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?