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!

How do you prove this fellow will stop falling?

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,

If

`n`

is`0`

then it trivially returns with the value`0`

.If

`n`

is non-zero, then we recurse*but*with a strictly smaller`n`

…… 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 `Nat`

ural 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 `acc`

umulator is a `Nat`

ural number that decreases at each iteration, neither of which may be true.

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