# Termination

## Refinements & Termination

Fortunately, we can ensure termination using refinements

## Main Idea

Recursive calls must be on smaller inputs

## Recur On Smaller`Nat`

To ensure termination of

```75: foo   :: Nat -> T
76: foo x =  body
```

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`

```99: {-@ fib  :: Nat -> Nat @-}
100: {v : Int | (v >= 0)} -> {v : Int | (v >= 0)}fib 0    = x1:Int# -> {x2 : Int | (x2 == (x1  :  int))}1
101: fib 1    = x1:Int# -> {x2 : Int | (x2 == (x1  :  int))}1
102: fib n    = {v : Int | (v >= 0)} -> {v : Int | (v >= 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))}+ {v : Int | (v >= 0)} -> {v : Int | (v >= 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` equation?

## Refinements Are Essential!

```121: {-@ gcd :: a:Nat -> {b:Nat | b < a} -> Int @-}
122: x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)} -> Intgcd {v : Int | (v >= 0)}a 0 = {x3 : Int | (x3 == a) && (x3 >= 0)}a
123: gcd a b = x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)} -> Intgcd {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!

```136: {-@ mod :: a:Nat
137:         -> b:{v:Nat|(0 < v && v < a)}
138:         -> {v:Nat| v < b}                 @-}
```

## Recur On Smaller Inputs

What of input types other than `Nat` ?

```148: foo   :: S -> T
149: foo x = body
```

Reduce to `Nat` case...

## Recur On Smaller Inputs

What of input types other than `Nat` ?

```166: foo   :: S -> T
167: 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`

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

```199: {-@ data L [llen] a = N
200:                     | C { x::a, xs :: L a} @-}
201:
202: {-@ measure llen :: L a -> Int
203:     llen (N)      = 0
204:     llen (C x xs) = 1 + (llen xs)   @-}
```

## Recur On Smaller Inputs

What of smallness spread across multiple inputs?

```217: forall a. (Ord a) => (L a) -> (L a) -> (L a)merge (L a)xs@(x `C` xs') (L a)ys@(y `C` ys')
218:   | {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 x1:a
-> x2:(L a)
-> {x4 : (L a) | ((llen x4) == (1 + (llen x2))) && ((x1 x4) == x1) && ((x2 x4) == x2)}`C` forall a. (Ord a) => (L a) -> (L a) -> (L a)merge {x3 : (L a) | (x3 == xs') && (0 <= (llen x3))}xs' {x7 : (L a) | (x7 == ys) && (x7 == (Termination.C y ys')) && ((ys' x7) == ys') && ((llen x7) == (1 + (llen ys'))) && ((y x7) == y) && (0 <= (llen x7))}ys
219:   | otherwise = {VV : a | (VV == y)}y x1:a
-> x2:(L a)
-> {x4 : (L a) | ((llen x4) == (1 + (llen x2))) && ((x1 x4) == x1) && ((x2 x4) == x2)}`C` forall a. (Ord a) => (L a) -> (L a) -> (L a)merge {x7 : (L a) | (x7 == xs) && (x7 == (Termination.C x xs')) && ((xs' x7) == xs') && ((llen x7) == (1 + (llen xs'))) && ((x x7) == x) && (0 <= (llen x7))}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.

```236: {-@ merge :: Ord a => xs:_ -> ys:_ -> _
237:           /  [(llen xs) + (llen ys)]     @-}
```

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?