Checking Termination
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
is0
then it trivially returns with the value0
. -
If
n
is non-zero, then we recurse but with a strictly smallern
... -
... 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.
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.