As explained in the last two posts, we need a termination checker to ensure that LiquidHaskell is not tricked by divergent, lazy computations into telling lies. Happily, it turns out that with very little retrofitting, and a bit of jiu jitsu, we can use refinements themselves to prove termination!

38: module Termination where
39: 
40: import Prelude     hiding (sum)
41: import Data.Vector hiding (sum)

Lets first see how LiquidHaskell proves termination on simple recursive functions, and then later, we’ll see how to look at fancier cases.

Looping Over Vectors

Lets write a bunch of little functions that operate on 1-dimensional vectors

54: type Val = Int
55: type Vec = Vector Val

Next, lets write a simple recursive function that loops over to add up the first n elements of a vector:

62: sum     :: Vec -> Int -> Val
63: x1:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen x1))}
-> (GHC.Types.Int)sum (Data.Vector.Vector (GHC.Types.Int))a 0 = x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1  :  int))}0
64: sum a n = ({VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV == a) && ((vlen VV) >= 0)}a x1:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV < (vlen x1)) && (0 <= VV)}
-> (GHC.Types.Int)! ({VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen a))}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)) x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ x1:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen x1))}
-> (GHC.Types.Int)sum {VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV == a) && ((vlen VV) >= 0)}a ({VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen a))}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)

Proving Termination By Hand(waving)

Does sum terminate?

First off, it is apparent that if we call sum with a negative n then it will not terminate. Thus, we should only call sum with non-negative integers.

Fine, lets assume n is non-negative. Why then does it terminate?

Intuitively,

1. If n is 0 then it trivially returns with the value 0.

2. If n is non-zero, then we recurse but with a strictly smaller n …

3. … but ultimately hit 0 at which point it terminates.

Thus we can, somewhat more formally, prove termination by induction on n.

Base Case n == 0 The function clearly terminates for the base case input of 0.

Inductive Hypothesis Lets assume that sum terminates on all 0 <= k < n.

Inductive Step Prove that sum n only recursively invokes sum with values that satisfy the inductive hypothesis and hence, which terminate.

This reasoning suffices to convince ourselves that sum i terminates for every natural number i. That is, we have shown that sum terminates because a well-founded metric (i.e., the natural number i) is decreasing at each recursive call.

Proving Termination By Types

We can teach LiquidHaskell to prove termination by applying the same reasoning as above, by rephrasing it in terms of refinement types.

First, we specify that the input is restricted to the set of Natural numbers

109: {-@ sum :: a:Vec -> {v:Nat | v < (vlen a)} -> Val @-}

where recall that Nat is just the refinement type {v:Int | v >= 0}.

Second, we typecheck the body of sum under an environment that restricts sum to only be called on inputs less than n, i.e. using an environment:

• a :: Vec
• n :: Nat
• sum :: Vec -> n':{v:Nat | v < n} -> Val

This ensures that any (recursive) call in the body only calls sum with inputs smaller than the current parameter n. Since its body typechecks in this environment, i.e. sum is called with n-1 which is smaller than n and, in this case, a Nat, LiquidHaskell proves that sum terminates for all n.

For those keeping track at home, this is the technique of sized types, , expressed using refinements. Sized types themselves are an instance of the classical method of proving termination via well founded metrics that goes back, at least, to Turing.

Choosing the Correct Argument

The example above is quite straightforward, and you might well wonder if this method works well for ``real-world” programs. With a few generalizations and extensions, and by judiciously using the wealth of information captured in refinement types, the answer is an emphatic, yes!

Lets see one extension today.

We saw that liquidHaskell can happily check that some Natural number is decreasing at each iteration, but it uses a naïve heuristic to choose which one – for now, assume that it always chooses the first Int parameter.

As you might imagine, this is quite simpleminded.

Consider, a tail-recursive implementation of sum:

153: {-@ sum' :: a:Vec -> Val -> {v:Nat| v < (vlen a)} -> Val @-}
154: sum' :: Vec -> Val -> Int -> Val
155: x1:(Data.Vector.Vector (GHC.Types.Int))
-> (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen x1))}
-> (GHC.Types.Int)sum' (Data.Vector.Vector (GHC.Types.Int))a (GHC.Types.Int)acc 0 = {VV : (GHC.Types.Int) | (VV == acc)}acc x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV == a) && ((vlen VV) >= 0)}ax1:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV < (vlen x1)) && (0 <= VV)}
-> (GHC.Types.Int)!{VV : (GHC.Types.Int) | (VV == (0  :  int))}0 
156: sum' a acc n = x1:(Data.Vector.Vector (GHC.Types.Int))
-> (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen x1))}
-> (GHC.Types.Int)sum' {VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV == a) && ((vlen VV) >= 0)}a ({VV : (GHC.Types.Int) | (VV == acc)}acc x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (Data.Vector.Vector (GHC.Types.Int)) | (VV == a) && ((vlen VV) >= 0)}ax1:(Data.Vector.Vector (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV < (vlen x1)) && (0 <= VV)}
-> (GHC.Types.Int)!{VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen a))}n) ({VV : (GHC.Types.Int) | (VV >= 0) && (VV < (vlen a))}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)

Clearly, the proof fails as liquidHaskell wants to prove that the accumulator is a Natural number that decreases at each iteration, neither of which may be true.

The remedy is easy. We can point liquidHaskell to the correct argument n using a Decrease annotation:

164: {-@ Decrease sum' 3 @-}

which directs liquidHaskell to verify that the third argument (i.e., n) is decreasing. With this hint, liquidHaskell will happily verify that sum' is indeed a terminating function.

Thats all for now, next time we’ll see how the basic technique can be extended to a variety of real-world settings.

---