# Termination Checking

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:

Q: Fill in the specification of mod to prove gcd terminating!
{-@ 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} -> Nat @-} 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!

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

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 :: xs:[a] -> ys:[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: Modify the termination metrics to prove that isEven and isOdd are terminating.
{-@ isEven :: n:Nat -> Bool / [n] @-} {-@ isOdd :: m:Nat -> Bool / [m] @-} isEven 0 = True isEven n = isOdd (n-1) isOdd m = not \$ isEven m

Hint: You will need one more element in the termination metrics to state that isOdd can freely call isEven.

## 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

## Desired Divergence

Declare it!

{-@ Lazy repeat @-} repeat x = x : repeat x

Lazy deactivates termination check for one function.

The flag "no-termination" deactivated termination check.

## 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

Next: Case Study