Termination Checking



















Why termination Checking?



LiquidHaskell checks by default that all your functions terminate!

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!















How about data types?

Map ADTs to integers using measures!

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



But Liquid Haskell knows that!


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















User specified metrics on ADTs


{-@ 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?


Liquid Haskell cannot know that!















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


What properties can be expressed in the logic?

  • Linear Arithmetic, Booleans, Uninterpreted Functions, ... (SMT logic)

  • Terminating Haskell functions.


Next: Refinement Reflection