Termination Checking


Why termination Checking?



By default, LH checks that functions terminate!

Most functions should terminate.


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

... is difficult (Halting Problem = NP-Complete).

Halting Problem

Proving Termination


Two main ways to prove termnination:

Syntactic: Recursive calls only happen on smaller inputs.

Semantic: (Finite Chains) A value is descreasing at each resursive call.


This value (called well founded metric) cannot get negative!

Proving Termination

Liquid Haskell Checks:

Some well founded metric decreases at each recursive call.


Heuristic Metric:

The first Int parameter.

Example: Termination of fib



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



Automatically Proved Terminating

User Specified Termination Metrics


The first Int need not always be decreasing!

{-@ replicate :: Int -> Int -> [Int] @-} replicate _ n | n <= 0 = [] replicate x n = x : replicate x (n - 1)

Specify metric as an expression over the inputs

User Specified Termination Metrics


The first Int need not always be decreasing!

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

Excercise: Fill in metric that proves range terminates.

Proving Termination


Liquid Haskell Checks:

Some well founded metric decreases at each recursive call.


Either first Int parameter (default)

or

User specified metric

Lexicographic Termination

Why does Ackermann Function terminate?

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

First argument m decreases or second argument n decreases.

Specify lexicographically ordered sequence of termination metrics [m, n]

How About Data Types?


Why does map terminate?

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

Recursive Calls on Smaller Lists.

Use first parameter with associated size

... as default metric.

User specified metrics on ADTs


What does merge terminate?

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

Q: The default is insufficient here; can you fill in a suitable metric?

Mutually Recursive Functions

Same idea generalizes to mutual recursion.

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

Q: Can you find the correct metric?

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

Diverging Functions


Some functions do not terminate!

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

lazy annotation deactivates termination checking.

Proving Termination


Liquid Haskell Checks

Some well founded metric decreases at each recursive call.

First Int or sized parameter (default), or

User specified lexicographic metric, or

The function is marked lazy.

Recap


Refinements: Types + Predicates
Specification: Refined Input/Output Types
Verification: SMT-based Predicate Subtyping
Measures: Specify Properties of Data
Termination: Well-founded Metrics

Thank You!


https://github.com/ucsd-progsys/liquidhaskell


http://www.refinement-types.org


online demo @ http://goto.ucsd.edu/liquidhaskell