0
size
returns positive valuesavg
head
and tail
are Safefoldr1
average
map
init
init'
insert
List
s ElementsList
max
type (I)max
type (II)max
type (III)max
typekeys
Map
eval
create
unsafeTake
unpack
chop
LiquidHaskell checks by default that all your functions terminate!
Why?
LiquidHaskell sometimes gives "unexpected" errors. Why is it complaining in the below factorial
definition?
Because, it cannot prove termination!
Indeed factorial (-42)
will diverge!
But, factorial
recursively calls itself with smaller arguments. Thus, it always terminates on non-negative inputs!
Q: Modify the specification of factorial
to prove termination.
That is great, because many times, to prove termination we need to know semantic invariants.
To prove gcd
terminating, we need to reason about the behavior of the mod
operator:
mod
to prove gcd
terminating!
To prove termination we need to prove that at each recursive call a well founded metric (i.e., one with a lower bound) strictly decreses.
Potential Metrics:
Range
's first argument is not decreasing.
Q: In the following type signature of range
replace 0
with the appropriate termination metric.
To prove termination we need to prove that at each recursive call a well founded metric (i.e., one with a lower bound) strictly decreses.
Potential Metrics:
Why does Ackermann Function terminate?
It does, but we need a termination (lexicographically descreaing) pair!
LiquidHaskell supports lexicographically decreasing tuples!
Q: In the following type signature of ack
replace 0
with the appropriate termination metrics.
To prove termination we need to prove that at each recursive call a well founded metric (i.e., one with a lower bound) strictly decreses.
Potential Metrics:
Recall the List
data type that came with a measure length
?
mapList
using the length
measure:
Wait! That was easy! LiquidHaskell is smarter than that!
If we teach liquidHaskell what is the size of a ADT, then it automatically uses it to prove termination!
To prove termination we need to prove that at each recursive call a well founded metric (i.e., one with a lower bound) strictly decreses.
Potential Metrics:
Build in lists come with a size len
, so at most recursive functions, termination metrics are not required.
Still there are functions that require more complicated termination metrics:
merge
:
To prove termination we need to prove that at each recursive call a well founded metric (i.e., one with a lower bound) strictly decreses.
Potential Metrics:
But, how do we prove mutual recursion? We just need to apply the same idea! Define one termination metric for each (mutually) recursive function:
isEven
and isOdd
are terminating.
Hint: You will need one more element in the termination metrics to state that isOdd
can freely call isEven
.
Thats all! We are ready to prove termination and functional corectness of more complicated functions, like the mutual recursive version of qsort
:
What about intentionaly non-termination?
Declare it!
Lazy
deactivates termination check for one function.
The flag "no-termination" deactivated termination check.
NIKI TODO: specify productive lists
Termination proofs are semantic, not syntactic.
To prove termination we need to prove that at each recursive call a well founded metric (i.e., one with a lower bound) strictly decreses.
Potential Metrics:
Next: Case Study
CHEAT AREA! mod :: a:Nat -> b:{v:Nat| 0 < v} -> {v:Nat | v < b}
qsort :: xs:[a] -> OList a / [len xs, 0] qpart :: x:a -> ys:_ -> l:_ -> r:_ -> _ / [len ys + len l + len r, len ys+1]
isEven :: n:Nat -> Bool / [n, 0] isOdd :: m:Nat -> Bool / [m, 1]