Avoiding Infinite Loops

Example: Proving Termination of sum



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



Q: (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 and 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, ...

Example: Proving Termination of sum


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

Default Metric

First Int parameter

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)

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 = []

Q: What metric proves range terminates?

Proving Termination


Liquid Haskell Checks

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

Q: The default is insufficient. What is a suitable metric?

Termination Can be Tricky


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

sort :: Ord a => [a] -> [a] sort [] = [] sort xs = merge (sort ys) (sort zs) where (ys, zs) = split xs

Avoiding Infinite Loops


Liquid Haskell Checks Termination

Some well founded metric decreases at each recursive call.

Avoiding Infinite Loops


Liquid Haskell Checks Termination

Some well founded metric decreases at each recursive call.


First Int or sized parameter (default), or

Avoiding Infinite Loops


Liquid Haskell Checks 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


Liquid Haskell Checks 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.

Avoiding Infinite Loops is Easy (in Practice)


Avoiding Infinite Loops 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

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 LiquidHaskell