Termination

Refinements & Termination

Main Idea

Recursive calls must be on smaller inputs

• Turing
• Sized Types
• DML
• Size Change Principle

Recur On Smaller Nat

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

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)

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)

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

Recur On Smaller Inputs

What of input types other than Nat ?

166: foo   :: S -> T
167: foo x = body

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'

Recur On Smaller Inputs

Neither input decreases, but their sum does.

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

Important Extensions

Recap

Main idea: Recursive calls on smaller inputs

A Curious Circularity

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?