Refinement Types via SMT and Predicate Abstraction

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.

```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., `a`mod``` b``` 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!