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

As explained in the [last][ref-lies] [two][ref-bottom] 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!

<!-- more -->

<div class="row-fluid">
   <div class="span12 pagination-centered">
       <img src="http://img.dailymail.co.uk/i/pix/2007/06_01/TombstoneSWNS_468x526.jpg"
       alt="Falling Down" width="300">
       <br>
       <br>
       <br>
       How do you prove this fellow will <b>stop falling?</b>
       <br>
       <br>
       <br>
   </div>
</div>



\begin{code}
module Termination where

import Prelude     hiding (sum)
import Data.Vector hiding (sum)
\end{code}

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

\begin{code}
type Val = Int
type Vec = Vector Val
\end{code}

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

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

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 `Nat`ural numbers

\begin{code}
{-@ sum :: a:Vec -> {v:Nat | v < (vlen a)} -> Val @-}
\end{code}

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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.124.5589), 
, 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](http://www.turingarchive.org/viewer/?id=462&title=01b).

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&#239;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`:

\begin{code}
{-@ sum' :: a:Vec -> Val -> {v:Nat| v < (vlen a)} -> Val @-}
sum' :: Vec -> Val -> Int -> Val
sum' a acc 0 = acc + a!0 
sum' a acc n = sum' a (acc + a!n) (n-1)
\end{code}

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.

\begin{code}The remedy is easy. We can point liquidHaskell to the correct argument `n` using a `Decrease` annotation: 
{-@ Decrease sum' 3 @-}
\end{code}
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.

[ref-lies]:  /blog/2013/11/23/telling-lies.lhs/ 
[ref-bottom]: /blog/2013/12/01/getting-to-the-bottom.lhs/