Code is meant to be run...

      msort :: (Ord a) => [a] -> [a]
      msort []   = []
      msort xs   = let (xs1, xs2) = split xs in
                      merge (msort xs1) (msort xs2)
      
      split :: [a] -> ([a], [a]) 
      split (x:y:zs) = let (xs, ys) = split zs in 
                         (x:xs, y:ys) 
      split xs       = (xs, [])
      
      merge :: (Ord a) => [a] -> [a] -> [a]  
      merge xs []         = xs
      merge [] ys         = ys
      merge (x:xs) (y:ys)
        | x <= y           = x : merge xs (y:ys)
        | otherwise        = y : merge (x:xs) ys

Code is meant to be run...


Code is meant to be run...and finish!



                λ> :l msort.hs
                [1 of 1] Compiling Main             ( msort.hs, interpreted )
                Ok, modules loaded: Main.
                λ> msort []
                []
                λ> msort [1,3,2]


Avoiding Infinite Loops

Lets prove termination!


Example: Proving Termination of sum



sum :: Int -> Int sum 0 = 0 sum n = n + sum (n - 1)



Exercise: (Why) does this terminate?

Proving Termination

Proving Termination

Termination: A well founded metric decreases at each recursive call

Proving Termination

Termination: A well founded metric decreases at each recursive call

Metric gets strictly smaller

Metric has a lower bound

Proving Termination

Termination: A well founded metric decreases at each recursive call

Metric gets strictly smaller and has a lower-bound

e.g. 99 bottles, 98 bottles, ..., 0 bottles!

Example: Proving Termination of sum


sum' :: Int -> Int sum' 0 = 0 sum' n = n + sum (n - 1)

Default Metric

First Int parameter

Exercise: Always gets smaller, but what's the lower bound?

User Specified Termination Metrics


The first Int need not always be decreasing!

User Specified Termination Metrics


The first Int need not always be decreasing!

{-@ fastSum :: Int -> Int -> Int @-} fastSum total 0 = total fastSum total n = fastSum (total + n) (n - 1)

Exercise: Can you specify metric as an expression over the inputs?

User Specified Termination Metrics


Specify metric as an expression over the inputs

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

Exercise: What metric proves range terminates?

Proving Termination


Type Checker Verifies

A 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 0 n = n + 1 ack m 0 = ack (m - 1) 1 ack m n = 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 append terminate?

append :: [a] -> [a] -> [a] append [] ys = ys append (x:xs) ys = x : append xs ys

Recursive Calls on Smaller Lists

Default Metric: First parameter with associated size

User specified metrics on Data Types


Why 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. What is a suitable metric?

Termination Can be Tricky


Exercise: What's going on with this merge-sort? Can you fix it?

sort :: Ord a => [a] -> [a] sort [] = [] sort xs = let (ys, zs) = split xs in merge (sort ys) (sort zs) split :: [a] -> ([a], [a]) split (x:y:zs) = let (xs, ys) = split zs in (x:xs, y:ys) split xs = (xs, [])

Avoiding Infinite Loops


Type Check Termination

Some well founded metric decreases at each recursive call.

Avoiding Infinite Loops


Type Check Termination

Some well founded metric decreases at each recursive call.


First Int or sized parameter (default), or

Avoiding Infinite Loops


Type Check Termination

Some well founded metric decreases at each recursive call.


First Int or sized parameter (default), or

User specified (lexicographic) metric, or

Avoiding Infinite Loops


Type Check Termination

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 (non-terminating).

Avoiding Infinite Loops is Easy (in Practice)


Avoiding Infinite Loops is Easy (in Practice)


503 Recursive Functions

67% via default metrics vs 30% user given metrics

1 metric per 100 LOC

Avoiding Infinite Loops is Easy (in Practice)


503 Recursive Functions

67% via default metrics vs 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 type checker