Previously we saw how refinements can be used to prove termination and we promised to extend our termination checker to handle “real-word” programs.

Keeping our promise, today we shall see a trick that allows liquidHaskell to prove termination on more recursive functions, namely lexicographic termination.

24: module LexicographicTermination where
25: 
26: import Language.Haskell.Liquid.Prelude (liquidError)

Does Ackermann Function Terminate?

Consider the famous Ackermann function

38: {-@ ack :: m:Nat -> n:Nat -> Nat @-}
39: ack :: Int -> Int -> Int
40: {v : Int | (v >= 0)}
-> {v : Int | (v >= 0)} -> {v : Int | (v >= 0)}ack {v : Int | (v >= 0)}m {v : Int | (v >= 0)}n
41:     | {x3 : Int | (x3 == m) && (x3 >= 0)}m x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 == x2))}== {x2 : Int | (x2 == (0  :  int))}0          = {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ {x2 : Int | (x2 == (1  :  int))}1
42:     | {x3 : Int | (x3 == m) && (x3 >= 0)}m x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 > x2))}> {x2 : Int | (x2 == (0  :  int))}0 x1:Bool
-> x2:Bool
-> {x2 : Bool | (((Prop x2)) <=> (((Prop x1)) && ((Prop x2))))}&& {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 == x2))}== {x2 : Int | (x2 == (0  :  int))}0 = {v : Int | (v >= 0)}
-> {v : Int | (v >= 0)} -> {v : Int | (v >= 0)}ack ({x3 : Int | (x3 == m) && (x3 >= 0)}mx1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}-{x2 : Int | (x2 == (1  :  int))}1) {x2 : Int | (x2 == (1  :  int))}1
43:     | {x3 : Int | (x3 == m) && (x3 >= 0)}m x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 > x2))}> {x2 : Int | (x2 == (0  :  int))}0 x1:Bool
-> x2:Bool
-> {x2 : Bool | (((Prop x2)) <=> (((Prop x1)) && ((Prop x2))))}&& {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 > x2))}>  {x2 : Int | (x2 == (0  :  int))}0 = {v : Int | (v >= 0)}
-> {v : Int | (v >= 0)} -> {v : Int | (v >= 0)}ack ({x3 : Int | (x3 == m) && (x3 >= 0)}mx1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}-{x2 : Int | (x2 == (1  :  int))}1) ({v : Int | (v >= 0)}
-> {v : Int | (v >= 0)} -> {v : Int | (v >= 0)}ack {x3 : Int | (x3 == m) && (x3 >= 0)}m ({x3 : Int | (x3 == n) && (x3 >= 0)}nx1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}-{x2 : Int | (x2 == (1  :  int))}1))
44:     | otherwise       = {x2 : [Char] | false} -> {x1 : Int | false}liquidError {x2 : [Char] | ((len x2) >= 0)}"Bad arguments!!!"

Does ack terminate?

At each iteration

1. Either m decreases,

2. or m remains the same and n decreases.

Each time that n reaches 0, m decreases, so m will eventaully reach 0 and ack will terminate.

Expressed more technically the pair (m, n) decreases in the lexicographic order on pairs, which is a well-ordering, ie., we cannot go down infinitely many times.

Express Termination Metric

Great! The pair (m, n) is a well-founded metric on the Ackermann function that decreases. From the previous post a well-founded metric is all liquidHaskell needs to prove termination. So, we should feed the tool with this information.

Remember the Decrease token? We used it previously to specify which is the decreasing argument. Now, we will use it with more arguments to specify our decreasing pair. So,

78: {-@ Decrease ack 1 2 @-}

says that the decreasing metric is the pair of the first and the second arguments, ie., the pair (m, n).

Finally, we will see how liquidHaskell uses this annotation to prove termination.

Proving Termination By Types

Following once more our previous post, liquidHaskell typechecks the body of ack under an environment that restricts ack to only be called on inputs less than (m,n). This time “less than” referes not to ordering on natural numbers, but to lexicographic ordering , i.e., using an environment:

• m :: Nat
• n :: Nat
• ack :: m':Nat -> n':{v:Nat | m' < m || (m' = m && v < n)} -> Nat

This ensures that any (recursive) call in the body only calls ack with inputs smaller than the current parameter (m, n). Since its body typechecks in this environment, i.e. ack is called with smaller parameters, LiquidHaskell proves that ack terminates.

Someone may find the Decrease token annoying: if we insert another argument we should also update the decrease information. LiquidHaskell supports an alternative notation, which lets you annotate the type signature with a list of decreasing expressions.

So, ack will also typecheck against the signature:

116: {-@ ack :: m:Nat -> n:Nat -> Nat / [m, n] @-}

But what is the syntax of the decreasing expressions? Are they restricted to function parameters? No, but that is the subject of a next post!