Termination {#termination} ========================== Dependent != Refinement -----------------------
**Dependent Types**
+
*Arbitrary terms* appear inside types
+
Termination ensures well-defined

**Refinement Types**
+
*Restricted refinements* appear in types
+
Termination *not* required ...
+
... except, alas, with *lazy* evaluation!
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) Recur On *Smaller* `Nat` ------------------------
**To ensure termination of** 
69: foo   :: Nat -> T
70: foo x =  body

**Check `body` Under Assumption** `foo :: {v:Nat | v < x} -> T`
*i.e.* require recursive calls have inputs *smaller* than `x`
Ex: Recur On *Smaller* `Nat` ---------------------------- 
93: {-@ fib  :: Nat -> Nat @-}
94: {VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0)}fib 0    = x1:(Int#) -> {x2 : (Int) | (x2 == (x1  :  int))}1
95: fib 1    = x1:(Int#) -> {x2 : (Int) | (x2 == (x1  :  int))}1
96: fib n    = {VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0)}fib ({x2 : (Int) | (x2 >= 0)}nx1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}-{x2 : (Int) | (x2 == (1  :  int))}1) x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+ {VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0)}fib ({x2 : (Int) | (x2 >= 0)}nx1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}-{x2 : (Int) | (x2 == (2  :  int))}2)

Terminates, as both `n-1` and `n-2` are `< n`

Demo:What if we drop the `fib 1` case?
Refinements Are Essential! -------------------------- 
115: {-@ gcd :: a:Nat -> {b:Nat | b < a} -> Int @-}
116: x1:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV >= 0) && (VV < x1)} -> (Int)gcd {VV : (Int) | (VV >= 0)}a 0 = {x3 : (Int) | (x3 == a) && (x3 >= 0)}a
117: gcd a b = x1:{VV : (Int) | (VV >= 0)}
-> {VV : (Int) | (VV >= 0) && (VV < x1)} -> (Int)gcd {x3 : (Int) | (x3 >= 0) && (x3 < a)}b ({x3 : (Int) | (x3 == a) && (x3 >= 0)}a x1:{x9 : (Int) | (x9 >= 0)}
-> x2:{x7 : (Int) | (x7 >= 0) && (0 < x7) && (x7 < x1)}
-> {x3 : (Int) | (x3 >= 0) && (x3 < x2)}`mod` {x3 : (Int) | (x3 >= 0) && (x3 < a)}b)

Need refinements to prove `(a mod b) < b` at *recursive* call! 

130: {-@ mod :: a:Nat 
131:         -> b:{v:Nat|(0 < v && v < a)} 
132:         -> {v:Nat| v < b}                 @-}
Recur On *Smaller* Inputs ------------------------- What of input types other than `Nat` ? 
142: foo   :: S -> T
143: foo x = body

**Reduce** to `Nat` case...

Recur On *Smaller* Inputs ------------------------- What of input types other than `Nat` ? 
160: foo   :: S -> T
161: foo x = body

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` ----------------------------- 
181: forall a b. (a -> b) -> (L a) -> (L b)map a -> bf N        = forall a. {x2 : (L a) | ((llen x2) == 0)}N
182: map f (C x xs) = (a -> bf {VV : a | (VV == x)}x) a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}`C` (forall a b. (a -> b) -> (L a) -> (L b)map a -> bf {x3 : (L a) | (x3 == xs) && (0 <= (llen x3))}xs)

Terminates using **default** measure `llen` 
191: {-@ data L [llen] a = N 
192:                     | C (x::a) (xs :: L a) @-}
193: {-@ measure llen :: L a -> Int
194:     llen (N)      = 0
195:     llen (C x xs) = 1 + (llen xs)   @-}
Recur On *Smaller* Inputs ------------------------- What of *smallness* spread across inputs? 
208: forall a. (Ord a) => (L a) -> (L a) -> (L a)merge (L a)xs@(x `C` xs') (L a)ys@(y `C` ys')
209:   | {VV : a | (VV == x)}x x1:a -> x2:a -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}< {VV : a | (VV == y)}y     = {VV : a | (VV == x)}x a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}`C` forall a. (Ord a) => (L a) -> (L a) -> (L a)merge {x3 : (L a) | (x3 == xs') && (0 <= (llen x3))}xs' {x5 : (L a) | (x5 == ys) && (x5 == (Termination.C y ys')) && ((llen x5) == (1 + (llen ys'))) && (0 <= (llen x5))}ys
210:   | otherwise = {VV : a | (VV == y)}y a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}`C` forall a. (Ord a) => (L a) -> (L a) -> (L a)merge {x5 : (L a) | (x5 == xs) && (x5 == (Termination.C x xs')) && ((llen x5) == (1 + (llen xs'))) && (0 <= (llen x5))}xs {x3 : (L a) | (x3 == ys') && (0 <= (llen x3))}ys'

Neither input decreases, but their *sum* does.
Recur On *Smaller* Inputs ------------------------- Neither input decreases, but their *sum* does. 
227: {-@ merge :: Ord a => xs:_ -> ys:_ -> _ 
228:           /  [(llen xs) + (llen ys)]     @-}

Synthesize *ghost* parameter equal to `[...]`

Reduces to single-parameter-decrease case.
Important Extensions -------------------- -
Mutual recursion
-
Lexicographic ordering...
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:* Decouple Invariants 5. **Lazy Evaluation:** Requires Termination 6. **Termination:** Via Refinements! 7.
**Evaluation**