0
size
returns positive valuesavg
head
and tail
are Safefoldr1
average
map
init
init'
insert
List
s ElementsList
keys
Map
eval
create
unsafeTake
unpack
chop
head
and tail
are Safefoldr1
average
map
init
init'
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:
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.
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 ofack
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.
Thats all! We are ready to prove termination and functional corectness of more complicated functions, like the mutual recursive version of qsort
:
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:
CHEAT AREA!
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]