Termination Checking
























Why Checking Termination?

LiquidHaskell checks by default that all your functions terminate!

Why?














Termination of Factorial

LiquidHaskell sometimes gives "unexpected" errors. Why is it complaining in the below factorial definition?

factorial :: Int -> Int factorial 0 = 1 factorial n = n * factorial (n-1)

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.

Hint: You may need to use the type of Natural numbers.
{-@ type Nat = {v:Int | 0 <= v } @-}









Termination proofs are semantic!

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:

{-@ gcd :: a:Nat -> b:{v:Nat | v < a} -> Int @-} gcd a 0 = a gcd a b = gcd b (a `mod` b) {-@ mod :: a:Nat -> b:{v:Nat| 0 < v} -> {v:Nat | v < b} @-} mod a b | a < b = a | otherwise = mod (a - b) b























Proving Termination I

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:

  • first integer argument














User specified Termination Metrics

Range's first argument is not decreasing.

range :: Int -> Int -> [Int] range lo hi | lo < hi = lo : range (lo+1) hi | otherwise = []
Q: In the following type signature of range replace 0 with the appropriate termination metric.
{-@ range :: lo:Int -> hi:Int -> [Int] / [0]@-}














Proving Termination IΙ

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:

  • user specified metrics
  • first integer argument












Lexicograohic Termination

Why does Ackermann Function terminate?

ack :: Int -> Int -> Int ack m n | m == 0 = n + 1 | n == 0 = ack (m-1) 1 | otherwise = ack (m-1) (ack m (n-1))

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.
{-@ ack :: m:Int -> n:Int -> Int / [0, 0]@-}









Proving Termination IΙ

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:

  • user specified lexicographic metrics
  • first integer argument

















Structural Recursion on ADTs

Recall the List data type that came with a measure length?

data List a = Emp -- Nil | (:::) a (List a) -- Cons





Q: Prove termination of mapList using the length measure:
{-@ mapList :: (a -> b) -> xs:List a -> List b / [0]@-} mapList f Emp = Emp mapList f (x:::xs) = f x ::: mapList f xs
















Relate ADTs with their size

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!

{-@ data List [length] @-}









Proving Termination IΙ

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:

  • user specified lexicographic metrics
  • first integer or "sized" argument



















Build In Lists

Build in lists come with a size len, so at most recursive functions, termination metrics are not required.







map :: (a -> b) -> [a] -> [b] map _ [] = [] map f (x:xs) = f x : map f xs













More termination metrics

Still there are functions that require more complicated termination metrics:







Q: Prove termination of merge:
merge :: Ord a => [a] -> [a] -> [a] merge [] [] = [] merge (x:xs) (y:ys) | x < y = x : merge xs (y:ys) | otherwise = y : merge (x:xs) ys













Proving 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:

  • user specified lexicographic metrics
  • first integer or "sized" argument



















Mutual Recursion

But, how do we prove mutual recursion? We just need to apply the same idea! Define one termination metric for each (mutually) recursive function:


Q: Prove that isEven and isOdd are terminating.
isEven :: Int -> Bool {-@ isEven :: n:Nat -> Bool / [0, 0] @-} {-@ isOdd :: m:Nat -> Bool / [0, 0] @-} isEven 0 = True isEven n = isOdd (n-1) isOdd m = not $ isEven m























Putting it all together!

Thats all! We are ready to prove termination and functional corectness of more complicated functions, like the mutual recursive version of qsort:

{-@ type OList a = [a]<{\x v -> x <= v}> @-} {-@ qsort :: xs:[a] -> OList a / [len xs, 0] @-} {-@ qpart :: x:_ -> ys:_ -> l:_ -> r:_ -> _ / [len ys + len l + len r, len ys+1] @-} qsort :: Ord a => [a] -> [a] qsort (x:xs) = qpart x xs [] [] qsort [] = [] qpart :: Ord a => a -> [a] -> [a] -> [a] -> [a] qpart x (y:ys) l r | x > y = qpart x ys (y:l) r | otherwise = qpart x ys l (y:r) qpart x [] l r = append x (qsort l) (qsort r) append x [] rs = x:rs append x (l:ls) rs = l:append x ls rs


























Recap

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:

  • user specified lexicographic metrics
  • first integer or "sized" argument