content: ---
  layout: post
  title: "Termination Checking"
  date: 2013-11-18 16:12
  comments: true
  external-url:
  categories: termination
  author: Niki Vazou
  published: false
  demo: Termination.hs
  ---
  
  If you used liquidHaskell lately, you may have noticed some type errors that
  just make no sense.
  Well, that is not a bug, but a ... **termination checker** failing to prove that
  your function terminates.
  
  In this post, we present how you can use liquidHaskell to prove termination on
  simple recursive functions and explain why termination is required for sound
  type checking.
  Of course liquidHaskell would be useless if it required that all your functions
  do terminate.
  Instead, it just requires that non-terminating functions return unrefined
  results.
  We will shortly explain how one can turn off termination checking while preserve
  sound type checking.
  
  <!-- more -->
  
  \begin{code}
  module Termination where
  
  import Prelude hiding (sum, (!!), repeat)
  import Data.List      (lookup)
  import Data.Maybe     (fromJust)
  
  import Language.Haskell.Liquid.Prelude (liquidAssert)
  \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. 
  Of course, we can never prove termination on non-terminating functions that
  naturally exist on haskell source code.
  So, we postpone 
  proving termination on more interesting functions
  and instead lets see how and when you can safely turn termination check off.
  
  Why is Termination Analysis Required
  -------------------------------------
  
  Consider a no-terminating function:
  
  \begin{code}
  {-@ foo :: Int -> {v:Int | false} @-}
  foo     :: Int -> Int
  foo n   = foo n
  \end{code}
  
  According to the *partial correctness property*
  the type signature for `foo` means that any
  value `foo` returns will satisfy the result refinement
  `false`. 
  Since `foo` never returns, 
  it can return *none* value, thus it trivially satisfies its
  type.
  
  Now, in an environment where `false` (i.e., `foo`'s result)
  exists, liquidHaskell can prove anything, 
  even the contradiction `0==1`:
  
  \begin{code}
  prop = liquidAssert ((\_ -> 0==1) (foo 0))
  \end{code}
  
  This is totally valid under *eager* evaluation, where
  to execute the assertion one should first compute the argument
  `foo 0` which never returns.
  But, it is not valid under haskell's *lazy* semantics
  where execution ignores the unused argument, and fails.
  
  From the above discussion we see that partial correctness is not enough to
  verify Haskell's lazy code.
  To restore soundness we require *total correctness*, or
  that each function terminates.
  This explains why termination checking is set as default to liquidHaskell (as is
  in many other verifiers, like Coq or Agda.)
  
  Turning off Termination Checking
  --------------------------------
  
  Of course, you cannot prove termination of functions like `repeat`
  
  \begin{code}
  {-@ repeat :: a -> [a] @-}
  repeat     :: a -> [a]
  repeat a   = a : repeat a
  \end{code}
  
  Instead, you can mark `repeat` as `Lazy` to disable termination for these
  functions:
  \begin{code}
  {-@ Lazy repeat @-}
  \end{code}
  
  But, be careful!
  By marking a function as `Lazy` *you* also guarantee that *the result type
  cannot contain inconsistencies*.
  In our previous example, liquidHaskell typechecked the unsafe `prop`, just
  because we marked `foo` (who's return type contains inconsistency) as `Lazy`
  \begin{code}
  {-@ Lazy foo @-}
  \end{code}
  
  Even though it is hard to decide if a type can contain inconsistencies,
  trivially *unrefined types* (or types refined to `true`) cannot ever be resolved
  to `false`.
  In other words, it is always safe to mark as `Lazy` functions with unrefined
  result.
  
  \begin{code} Finally, you have the option to totally disable termination checking, using the `no-termination` flag:
  {-@ LIQUID "--no-termination" @-}
  \end{code}
  
  Conclusion
  ----------
  
  In this post, 
  
  - We saw how to use liquidHaskell to prove termination of simple recursive
    functions, and
  
  - We learned why termination is required for sound type checking and when
    it is safe to deactivate it.
  
  Termination checking may sound a big demand,
  but soon we will see that liquidHaskell is powerful enough to prove
  termination on a great number of functions
  