Termination Checking

Why?

Example: Termination of fib

{-@ fib :: i:Int -> Int @-} fib i | i == 0 = 0 | i == 1 = 1 | otherwise = fib (i-1) + fib (i-2)

Q: Why is there an error?

Proving Termination I

Liquid Haskell checks a well founded metric decreases at each recursive call.

Well founded metrics:

• the first integer argument.

User specified Termination Metrics

The first integer is not always decreasing!

{-@ range :: lo:Int -> hi:Int -> [Int] / [0] @-} range lo hi | lo < hi = lo : range (lo+1) hi | otherwise = []

Q: Replace 0 with the decreasing metric!

Proving Termination

Liquid Haskell checks a well founded metric decreases at each recursive call.

Well founded metrics:

• user specified metrics, or
• the first integer argument.

Lexicographic Termination

Why does Ackermann Function terminate?

{-@ ack :: m:Int -> n:Int -> Int / [0, 0] @-} ack m n | m == 0 = n + 1 | n == 0 = ack (m-1) 1 | otherwise = ack (m-1) (ack m (n-1))

Q: Replace 0 with the decreasing metrics!

Map ADTs to integers using measures!

{-@ map :: (a -> b) -> xs:[a] -> [b] / [len xs] @-} map _ [] = [] map f (x:xs) = f x : map f xs

It will use len as the default metric to check x:[a] decreasing.

{-@ merge :: xs:[a] -> ys:[a] -> [a] / [0] @-} merge xs [] = xs merge [] ys = ys merge (x:xs) (y:ys) | x < y = x:(merge xs (y:ys)) | otherwise = y:(merge ys (x:xs))

Does merge terminate?

Mutual Recursive Functions

Same idea generalizes to mutual recursion.

{-@ isEven :: n:Nat -> Bool / [n, 0] @-} {-@ isOdd :: m:Nat -> Bool / [m, 0] @-} isEven 0 = True isEven n = isOdd (n-1) isOdd m = not \$ isEven m

Can you find the correct metric?

Liquid Haskell does not even attempt to guess it...

Diverging Functions

Lazy annotation deactivates termination checking.

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

Proving Termination

For non Lazy specified functions,

Liquid Haskell checks a well founded metric decreases at each recursive call.

Well founded metrics:

• user specified lexocographic metrics,
• the first integer or "sized" argument.

Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Specify Properties of Data
4. Termination: Use Logic to Prove Termination

Next: Refinement Reflection : Allow terminating functions in the logic!