0size returns positive valuesavghead and tail are Safefoldr1averagemapinitinit'insertLists ElementsListmax type (I)max type (II)max type (III)max typekeysMapevalcreateunsafeTakeunpackchop
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]