2013-12-29-decreasing-expressions.lhs

---
layout: post
title: "Decreasing Expressions"
date: 2013-12-29 16:12
comments: true
external-url:
categories: termination, measures
author: Niki Vazou
published: false
demo: DecreasingExpressions.hs
---

So far we proved that many recursive functions terminate.
All the functions we used share a characteristic.
They had (a list of) arguments that were (lexicographically) decreasing.

What if no argument decreases?
Consider an argument `i` that increases up to a higher value `hi`.
As `i` increases the difference `hi - i` decreases and will eventually reach
`0`.
This difference "witnesses" termination.

Today we will describe 
the last mechanism liquidHaskell uses to prove termination:
*decreasing expressions*
that allow us to annotate functions with termination withnesses.

<!-- more -->

\begin{code}
module DecreasingExpressions where

range ::          Int -> Int -> [Int]
merge :: Ord a => [a] -> [a] -> [a]
\end{code}

Termination on Increasing Arguments
-----------------------------------

Consider a `range` function that takes two integers 
a `lo`wer and a `hi`gher and returns the list `[lo, lo+1, ..., hi-1]`

\begin{code}
range lo hi | lo < hi   = lo : range (lo + 1) hi
            | otherwise = []
\end{code}

Clearly the difference `hi - lo` is decreasing at each iteration and will
eventually reach `0`.
That is, `hi - lo` is a *well-founded metric* that decreases.
[Previously][ref-termination] we discussed that this is exactly what 
liquidHaksell needs to prove termination.

Sadly, liquidHaskell cannot synthesize this metric.
But provides a mechanism for the user to specify it.
With *decreasing expressions*, 
we can annotate the type of a recursive function
with the termination witness. Thus

\begin{code}
{-@ range :: lo:Int -> hi:Int -> [Int] / [(hi - lo)] @-}
\end{code}

makes liquidHaskell 
prove that `hi - lo` is a non-negative quantily that decreases at
each iteration, 

Termination on a Function of the Arguments
------------------------------------------

Lets illustrate the power of decreasing expressions with a more involved
example.

Consider the standard `merge` from the homonymous sorting function 

\begin{code}
merge (x:xs) (y:ys) 
  | x < y     = x : merge xs     (y:ys)
  | otherwise = y : merge (x:xs) ys
\end{code}

Does `merge` terminate?
Well it does because at each iteration the sum of the lengths of the two
arguments decreases. 
Using liquidHaskell's build in [measure][ref-measure] `len`
to get the length of a list, we can specify 
`(len xs) + (len ys)`
as the decreasing expression for `merge`

\begin{code}_
{-@ merge :: Ord a => xs:[a] -> ys:[a] -> [a] / [(len xs) + (len ys)] @-}
\end{code}


By the way, the power of liquidHaskell does not stop at proving `merge`
terminating. 
It extends to proving that given two sorted lists, `merge` will actually return
a sorted list!

[Some time ago][ref-slist], we represented Sorted Lists as
\begin{code}
{-@ type SL a = [a]<{\x v -> x <= v}> @-}
\end{code}

With this, all we need to prove that sortedness is preserved is to type `merge`
as
\begin{code}
{-@ merge :: Ord a => xs:(SL a) -> ys:(SL a) -> (SL a) 
           / [(len xs) + (len ys)]                                    @-}
\end{code}


Wrapping Up Termination Checking
--------------------------------

In the last couple of posts, we presented the mechanisms liquidHaskell uses to
prove termination

- We [started][ref-termination] with functions recursive on some natural namber
  `i` that served as a decreasing metric to prove termination.

- [Then][ref-lex], we used lexicographic ordering to prove termination on functions where
  the decreasing metric constists of a list of arguments.

- [After][ref-structures], we saw how to handle recursion on data structures: by proving the size of
  this structure is decreasing, and

- Today, we saw how to express more complicated decreasing metrics.

Obviously liquidHaskell does not solve the halting problem: there do exist
terminating functions that cannot be proven terminating.
Worse, there do exist some cases of non-terminating functions tha fool
liquidHaskell: 
for instance, you can trick the tool 
if you encode termination via [recursive types][ref-rec] or
[references][ref-ref].
We aim to soon address such corner cases.

We claim that the above mechanisms suffice to prove 
termination on numerous functions.
Even *mutually recursive* ones, as we shall soon see.



[ref-ref]:          https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/todo/Recursion1.hs
[ref-rec]:          http://en.wikipedia.org/wiki/Fixed-point_combinator#Example_of_encoding_via_recursive_types 
[ref-lies]:        /blog/2013/11/23/telling-lies.lhs/ 
[ref-bottom]:      /blog/2013/12/01/getting-to-the-bottom.lhs/
[ref-termination]: /blog/2013/12/08/termination-checking.lhs/
[ref-lex]:         /blog/2013/12/15/lexicographic-termination.lhs/
[ref-structures]:  /blog/2013/12/22/measuring-the-size-of-structures.lhs/
[ref-measure]:     /blog/2013/01/31/safely-catching-a-list-by-its-tail.lhs/
[ref-slist]:       /blog/2013/07/29/putting-things-in-order.lhs/