basic_termination.lhs

---
layout: post
title: "Termination Checking"
date: 2013-11-18 16:12
comments: true
external-url:
categories: termination
author: Niki Vazou
published: false 
demo: TerminationBasic.hs
---

As explained in the [last](LINK) [two](LINK) posts, we need a termination
checker to ensure that LiquidHaskell is not tricked by divergent, lazy
computations into telling lies. Well, proving termination is not easy, but
happily, it turns out that with very little retrofitting, we can use 
refinements to prove termination.

In this post, lets see how LiquidHaskell proves termination on simple 
recursive functions, and then later, we'll see how to look at fancier 
cases.

<!-- more -->

\begin{code}
module Termination where

import Prelude hiding (sum, (!!))
import Data.List      (lookup)
\end{code}

Termination Check with Refinement Types
---------------------------------------

Consider a `Vec`tor that maps `Int`egers to `Val`ues:

\begin{code}
type Val   = Int
data Vec   = V [(Int, Val)]

(!!)       :: Vec -> Int -> Val
(V a) !! i = case i `lookup` a of {Just v -> v; _ -> 0}
\end{code}

Let `sum a i` add the `i` first elements of the vector `a`:

\begin{code}
sum     :: Vec -> Int -> Val
sum a 0 = 0
sum a i = (a !! (i-1)) + sum a (i-1)
\end{code}

Does `sum` terminate?
We observe that if `i` is not `0` then `sum i` will call `sum (i-1)`, otherwise
it will return.
This reasoning suffices to convince ourselves that `sum i` terminates for every
natural number `i`.
Formally, we shown that `sum` terminates because a *well-founded metric* (i.e., the
natural number `i`) is decreasing at each iteration.
Thus, to ensure termination it suffices to restrict `i` on Natural numbers,
which we can do with a liquid-type signature.
\begin{code}
{-@ sum :: Vec -> Nat -> Val @-}
\end{code}

LiquidHaskell will apply the same reasoning to prove `sum`
terminates:
Conventionally, to typecheck `sum` we would check the body assuming an
environment

`a:Vec`, `i:Nat`, `sum:Vec -> Nat -> Val`

Instead, we *weaken* the environment to 

`a:Vec`, `i:Nat`, `sum:Vec -> {v:Nat| v < i} -> Val`

Now, the type of `sum` stipulates that it *only* be recursively called with
`Nat` (so well-founded) values that are *strictly less than* the current parameter `i`. 
Since its body typechecks in this environment, `sum` terminates for
every `i` on `Nat`s.

Choosing the correct argument
-----------------------------

We saw that liquidHaskell can happily check that a Natural number is decreasing
at each iteration; but it uses a na&#239;ve heuristic to choose which one. 
For this post we can assume that it always chooses *the first* Integer. 

So, a tail-recursive implementation of `sum`:
\begin{code}
{-@ sum' :: Vec -> Val -> Nat -> Val @-}
sum' :: Vec -> Val -> Int -> Val
sum' a acc 0 = acc + a!!0 
sum' a acc i = sum' a (acc + a!!i) (i-1)
\end{code}

will fail, as liquidHaskell wants to prove that the `acc`umulator is the `Nat`ural
number that
decreases at each iteration.

\begin{code}The remedy is simple. We can direct liquidHaskell to the correct argument `i` using a `Decrease` annotation: 
{-@ Decrease sum' 3 @-}
\end{code}
which directs liquidHaskell to check whether the *third*
argument (i.e., `i`) is decreasing.
With this hint, liquidHaskell will happily verify that `sum'` is indeed a
terminating function.


Lexicographic Termination
-------------------------

Lets complicate the things a little bit.
To do so, lets compute the `sum` of a 2D `Vec`tor:

\begin{code}
data Vec2D    = V2D [((Int, Int), Val)]

(!!!)         :: Vec2D -> (Int,Int) -> Val
(V2D a) !!! i = case i `lookup` a of {Just v -> v; _ -> 0}
\end{code}

Now we write a `sum2D a n m` function that computes the sum of the first 
`(n+1)(m+1)` elements of `a`

\begin{code}
{-@ sum2D :: Vec2D -> Nat -> Nat -> Val @-}
sum2D :: Vec2D -> Int -> Int -> Val
sum2D a n m = go n m
  where 
       {-@ Decrease go 1 2 @-}
        go 0 0             = 0
        go i j | j == 0    =  a!!!(i, 0) + go (i-1) m
               | otherwise =  a!!!(i, j) + go i (j-1)
\end{code}

Here there is no decreasing argument, 
if `j>0`, `j` decreases (line `139`), otherwise `i` decreases (line `138`).
Though, liquidHaskell succeed in verifying that `sum2D` terminates and the reason
is our `Decrease go 1 2` annotation.
This annotation informs the tool that the decreasing measure is the
*lexicographically ordered* pair `[i,j]`. 
LiquidHaskell will verify that this pair is indeed decreasing: at each
iteration either `i` decreases (line `138`) or `i` remains the same and `j`
decreases (line `139`).

\begin{code}An alternative annotation to express the above decreasing measure is:
       {-@ go :: i:Nat -> j:Nat -> Val / [i, j] @-}
\end{code}
where after the type signature for `go` we write the list of lexicographic
decreasing *expressions*.
This mechanism, as we shall see, allows us to prove termination in functions
where the decreasing measure in a *function* of the arguments.

Decreasing expressions
----------------------
Back to our `1D` Vector, 
we now define a function `sumFromTo a lo hi` that sums the elements form `a!!lo`
to `a!!hi`:

\begin{code}
{-@ sumFromTo :: Vec -> lo:Nat -> hi:{v:Nat|v>=lo} -> Val @-}
sumFromTo :: Vec -> Int -> Int ->  Val
sumFromTo a lo hi = go lo hi
  where 
       {-@ go :: lo:Nat -> hi:{v:Nat|v>=lo} -> Val / [hi-lo] @-}
        go lo hi | lo == hi  =  a!!lo
                 | otherwise =  a!!lo + go (lo+1) hi
\end{code}

No argument is decreasing in this function, 
but still it does terminate, as at each iteration `lo` is increased and
execution will terminate when `lo` reaches `hi`.
Here the decreasing measure is the expression `hi-lo`.
LiquidHaskell has no way to generate such a measure, but,
if the user generates it, i.e., by annotating `go`'s signature,
liquidHaskell will happily check that `lo-hi` is indeed a well-founded measure (as it is
a natural number) that decreases at each iteration.


Powered with decreasing expressions and the `Decrease` hint,
we can prove termination on a great number of functions 
ranging from 
ones defined on recursive data structures
to mutual recursive ones. 
We shall soon see how to prove termination on more complicated functions, why
is termination analysis required by liquidHaskell and when is it safe to
deactivate it.

\begin{code}Until then, bear in mind that you can disable termination checking using the `no-termination` flag:
{-@ LIQUID "--no-termination" @-}
\end{code}