content: ---
  layout: post
  title: "Lexicographic Termination"
  date: 2013-12-15 16:12
  comments: true
  external-url:
  categories: termination, lexicographic ordering
  author: Niki Vazou
  published: true 
  demo: LexicographicTermination.hs
  ---
  
  [Previously][ref-termination] 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*.
  
  <!-- more -->
  
  <div class="hidden">
  
  \begin{code}
  module LexicographicTermination where
  
  import Language.Haskell.Liquid.Prelude (liquidError)
  \end{code}
  
  </div>
  
  Does Ackermann Function Terminate?
  ----------------------------------
  
  Consider the famous [Ackermann
  function](http://en.wikipedia.org/wiki/Ackermann_function)
  
  \begin{code}
  {-@ ack :: m:Nat -> n:Nat -> Nat @-}
  ack :: Int -> Int -> Int
  ack m n
      | m == 0          = n + 1
      | m > 0 && n == 0 = ack (m-1) 1
      | m > 0 && n >  0 = ack (m-1) (ack m (n-1))
      | otherwise       = liquidError "Bad arguments!!!"
  \end{code}
  
  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](htpp://en.wikipedia/wiki/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][ref-termination] 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][ref-termination]
  to specify which is the decreasing argument.
  Now, we will use it with more arguments to specify 
  our decreasing pair. So,
  
  \begin{code}
  {-@ Decrease ack 1 2 @-}
  \end{code}
  
  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][ref-termination],
  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*.
  
  \begin{code} So, `ack` will also typecheck against the signature:
  {-@ ack :: m:Nat -> n:Nat -> Nat / [m, n] @-}
  \end{code}
  
  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!
  
  [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/
  