2013-12-14-gcd.lhs

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

We've seen how, in the presence of [lazy evaluation][ref-lies], refinements
[require termination][ref-bottom]. [Next][ref-termination], we saw how 
LiquidHaskell can be used to prove termination. 

Today, lets see how **termination requires refinements**. 

That is, a crucial feature of LiquidHaskell's termination prover is that it is 
not syntactically driven, i.e. is not limited to say, structural recursion. 
Instead, it uses the wealth of information captured by refinements that are
at our disposal, in order to prove termination. 

This turns out to be crucial in practice.
As a quick toy example -- motivated by a question by [Elias][comment-elias] -- 
lets see how, unlike purely syntax-directed (structural) approaches, 
LiquidHaskell proves that recursive functions, such as Euclid's GCD 
algorithm, terminates.

<!-- more -->

<br>
<br>
<br>

<div class="row-fluid">
  <div class="span12 pagination-centered">
  <img src="http://faculty.etsu.edu/gardnerr/Geometry-History/Euclid_7-Raphael.jpg"
       alt="Euclid" width="300">
       <br>
       <br>
       <br>
       With LiquidHaskell, Euclid wouldn't have had to wave his hands.
       <br>
       <br>
       <br>
  </div>
</div>

\begin{code}
module GCD where

import Prelude hiding (gcd, mod)

mod :: Int -> Int -> Int
gcd :: Int -> Int -> Int
\end{code}

The [Euclidean algorithm][ref-euclidean] is one of the oldest numerical algorithms 
still in common use and calculates the the greatest common divisor (GCD) of two 
natural numbers `a` and `b`.

Assume that `a > b` and consider the following implementation of `gcd`

\begin{code}
{-@ gcd :: a:Nat -> b:{v:Nat | v < a} -> Int @-}
gcd a 0 = a
gcd a b = gcd b (a `mod` b)
\end{code}

From our previous post, to prove that `gcd` is terminating, it suffices to prove
that the first argument decreases as each recursive call.

By `gcd`'s type signature, `a < b` holds at each iteration, thus liquidHaskell 
will happily discharge the terminating condition.

The only condition left to prove is that `gcd`'s second argument, ie., `a `mod`
b` is less that `b`. 

This property follows from the behavior of the `mod` operator.

So, to prove `gcd` terminating, liquidHaskell needs a refined signature for 
`mod` that captures this behavior, i.e., that for any `a` and `b` the value 
`mod a b` is less than `b`. Fortunately, we can stipulate this via a refined
type:

\begin{code}
{-@ mod :: a:Nat -> b:{v:Nat| 0 < v} -> {v:Nat | v < b} @-}
mod a b
  | a < b = a
  | otherwise = mod (a - b) b
\end{code}

\begin{code}Euclid's original version of `gcd` is different
gcd' :: Int -> Int -> Int
gcd' a b | a == b = a
         | a >  b = gcd' (a - b) b 
         | a <  b = gcd' a (b - a) 
\end{code}

Though this version is simpler, turns out that LiquidHaskell needs 
a more sophisticated mechanism, called **lexicographic ordering**, to 
prove it terminates. Stay tuned!


[ref-euclidean]:    http://en.wikipedia.org/wiki/Euclidean_algorithm
[ref-termination]:  /blog/2013/12/09/checking-termination.lhs/ 
[ref-lies]:  /blog/2013/11/23/telling-lies.lhs/ 
[ref-bottom]: /blog/2013/12/01/getting-to-the-bottom.lhs/
[comment-elias]: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/12/09/checking-termination.lhs/#comment-1159606500