Termination Requires Refinements

We've seen how, in the presence of lazy evaluation, refinements require termination. Next, we saw how LiquidHaskell can be used to prove termination.

Today, lets see how termination requires refinements.

That is, a crucial feature of LiquidHaskell's termination prover is that it is not syntactically driven, i.e. is not limited to say, structural recursion. Instead, it uses the wealth of information captured by refinements that are at our disposal, in order to prove termination.

This turns out to be crucial in practice. As a quick toy example -- motivated by a question by Elias -- lets see how, unlike purely syntax-directed (structural) approaches, LiquidHaskell proves that recursive functions, such as Euclid's GCD algorithm, terminates.




Euclid


With LiquidHaskell, Euclid wouldn't have had to wave his hands.


51: module GCD where
52: 
53: import Prelude hiding (gcd, mod)
54: 
55: mod :: Int -> Int -> Int
56: gcd :: Int -> Int -> Int

The Euclidean algorithm is one of the oldest numerical algorithms still in common use and calculates the the greatest common divisor (GCD) of two natural numbers a and b.

Assume that a > b and consider the following implementation of gcd

66: {-@ gcd :: a:Nat -> b:{v:Nat | v < a} -> Int @-}
67: x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x1)}
-> (GHC.Types.Int)gcd {VV : (GHC.Types.Int) | (VV >= 0)}a 0 = {VV : (GHC.Types.Int) | (VV == a) && (VV >= 0)}a
68: gcd a b = x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x1)}
-> (GHC.Types.Int)gcd {VV : (GHC.Types.Int) | (VV >= 0) && (VV < a)}b ({VV : (GHC.Types.Int) | (VV == a) && (VV >= 0)}a {VV : (GHC.Types.Int) | (VV >= 0)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (0 < VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x2)}`mod` {VV : (GHC.Types.Int) | (VV >= 0) && (VV < a)}b)

From our previous post, to prove that gcd is terminating, it suffices to prove that the first argument decreases as each recursive call.

By gcd's type signature, a < b holds at each iteration, thus liquidHaskell will happily discharge the terminating condition.

The only condition left to prove is that gcd's second argument, ie., amodb is less that b.

This property follows from the behavior of the mod operator.

So, to prove gcd terminating, liquidHaskell needs a refined signature for mod that captures this behavior, i.e., that for any a and b the value mod a b is less than b. Fortunately, we can stipulate this via a refined type:

88: {-@ mod :: a:Nat -> b:{v:Nat| 0 < v} -> {v:Nat | v < b} @-}
89: {VV : (GHC.Types.Int) | (VV >= 0)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (0 < VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x2)}mod {VV : (GHC.Types.Int) | (VV >= 0)}a {VV : (GHC.Types.Int) | (VV >= 0) && (0 < VV)}b
90:   | {VV : (GHC.Types.Int) | (VV == a) && (VV >= 0)}a x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 < x2))}< {VV : (GHC.Types.Int) | (VV == b) && (VV >= 0) && (0 < VV)}b = {VV : (GHC.Types.Int) | (VV == a) && (VV >= 0)}a
91:   | otherwise = {VV : (GHC.Types.Int) | (VV >= 0)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (0 < VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x2)}mod ({VV : (GHC.Types.Int) | (VV == a) && (VV >= 0)}a x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- {VV : (GHC.Types.Int) | (VV == b) && (VV >= 0) && (0 < VV)}b) {VV : (GHC.Types.Int) | (VV == b) && (VV >= 0) && (0 < VV)}b

Euclid's original version of gcd is different

95: gcd' :: Int -> Int -> Int
96: gcd' a b | a == b = a
97:          | a >  b = gcd' (a - b) b 
98:          | a <  b = gcd' a (b - a) 

Though this version is simpler, turns out that LiquidHaskell needs a more sophisticated mechanism, called lexicographic ordering, to prove it terminates. Stay tuned!

Niki Vazou
2013-12-14 16:12