Termination Checking


Why termination Checking?



By default, LH checks that functions terminate!

Most functions should terminate

For soundness w.r.t. laziness [ICFP 14]


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


Liquid Haskell Checks:

Some well founded metric decreases at each recursive call.


Default 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

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

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

Termination is Easy in Practice

Library LOC Specs Time
XMonad.StackSet 256 74 27s
Data.List 814 46 26s
Data.Set.Splay 149 27 27s
Data.Vector.Algorithms 1219 76 61s
Data.Map.Base 1396 125 68s
Data.Text 3128 305 231s
Data.Bytestring 3505 307 136s
Total 11512 977 574s

Termination is Easy in Practice


503 Recursive Functions

  • 67% via default metrics
  • 30% user given metrics
  • 1 metric per 100 LOC

20 functions not proven to terminate

  • 12 do not terminate (e.g. top-level IO loops)
  • 8 currently outside scope of LiquidHaskell

Recap


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

What properties can be expressed in the logic?


Decidable SMT Theories

  • Boolean Propositions
  • Linear Arithmetic
  • Uninterpreted functions


Next: Any Terminating Haskell Function

Refinement Reflection