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.
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!