Termination {#termination} ========================== Refinements & Termination -------------------------
Fortunately, we can ensure termination **using refinements**
Main Idea --------- Recursive calls must be on **smaller** inputs
+ [Turing](http://classes.soe.ucsc.edu/cmps210/Winter11/Papers/turing-1936.pdf) + [Sized Types](http://dl.acm.org/citation.cfm?id=240882) + [DML](http://dl.acm.org/citation.cfm?id=609232) + [Size Change Principle](http://dl.acm.org/citation.cfm?id=360210) Recur On *Smaller* `Nat` ------------------------
**To ensure termination of** \begin{spec}
foo :: Nat -> T foo x = body \end{spec}

**Check `body` Under Assumption** `foo :: {v:Nat | v < x} -> T`
*i.e.* require recursive calls have `Nat` inputs *smaller than* `x`
Ex: Recur On *Smaller* `Nat` ---------------------------- \begin{code} {-@ fib :: Nat -> Nat @-} fib 0 = 1 fib 1 = 1 fib n = fib (n-1) + fib (n-2) \end{code}
Terminates, as both `n-1` and `n-2` are `< n`

Demo:   What if we drop the `fib 1` equation?
Refinements Are Essential! -------------------------- \begin{code} {-@ gcd :: a:Nat -> {b:Nat | b < a} -> Int @-} gcd a 0 = a gcd a b = gcd b (a `mod` b) \end{code}
Need refinements to prove `(a mod b) < b` at *recursive* call!

\begin{code} {-@ mod :: a:Nat -> b:{v:Nat|(0 < v && v < a)} -> {v:Nat| v < b} @-} \end{code}
Recur On *Smaller* Inputs ------------------------- What of input types other than `Nat` ? \begin{spec}
foo :: S -> T foo x = body \end{spec}
**Reduce** to `Nat` case...

Recur On *Smaller* Inputs ------------------------- What of input types other than `Nat` ? \begin{spec}
foo :: S -> T foo x = body \end{spec}
Specify a **default measure** `mS :: S -> Int`
**Check `body` Under Assumption** `foo :: {v:s | 0 <= (mS v) < (mS x)} -> T`
Ex: Recur on *smaller* `List` ----------------------------- \begin{code} map f N = N map f (C x xs) = (f x) `C` (map f xs) \end{code}
Terminates using **default** measure `llen`
\begin{code} {-@ data L [llen] a = N | C { x::a, xs :: L a} @-} {-@ measure llen :: L a -> Int llen (N) = 0 llen (C x xs) = 1 + (llen xs) @-} \end{code}
Recur On *Smaller* Inputs ------------------------- What of smallness spread across **multiple inputs**?
\begin{code} merge xs@(x `C` xs') ys@(y `C` ys') | x < y = x `C` merge xs' ys | otherwise = y `C` merge xs ys' \end{code}
Neither input decreases, but their **sum** does.
Recur On *Smaller* Inputs ------------------------- Neither input decreases, but their **sum** does.
\begin{code} {-@ merge :: Ord a => xs:_ -> ys:_ -> _ / [(llen xs) + (llen ys)] @-} \end{code}
Synthesize **ghost** parameter equal to `[...]`

... thereby reducing to decreasing **single parameter** case.
Important Extensions --------------------
**Mutual** recursion

**Lexicographic** ordering

Fit easily into our framework ...
Recap ----- Main idea: Recursive calls on **smaller** inputs
Use refinements to **check** smaller

Use refinements to **establish** smaller
A Curious Circularity ---------------------
Refinements require termination ...

... Termination requires refinements!

Meta-theory is tricky, but all ends well.
Recap ----- 1. Refinements: Types + Predicates 2. Subtyping: SMT Implication 3. Measures: Strengthened Constructors 4. Abstract: Refinements over functions and data 5. Lazy Evaluation: Requires Termination 6. **Termination:** via Refinements! 7.
**Evaluation:** How good is this in practice?


[[continue...]](11_Evaluation.lhs.slides.html)