[Agda] termination checking

[Peter Selinger]

Hi Andreas,

thanks for your reply. I think I understand your point. Record
constructors are matched lazily, and therefore could lead to infinite
loops, because a variable x of type Empty will expand to inn (inn (inn
...))  indefinitely.

However, this is unfortunate, because it means that there is no way to
make the "Inductive" argument irrelevant, even though it is, in fact,
irrelevant. Or to put it differently: the combination of features of
datatypes and record types seems to be such that it is impossible to
prove termination by structural induction on an irrelevant argument,
even in cases where this should be possible. 

I'll give a concrete example below.

First I should point out the the Fibonacci example of my last email
was a red herring. I was puzzled by the fact that the function
fibonacci-aux passes the termination checker; however, it does so
because the first (and not the second) argument is structurally
decreasing. Duh. Sorry for not having noticed this earlier.

Nevertheless, I will stick with the Fibonacci example, because it
illustrates the following point better than integer division.

Type-check this code:

----------------------------------------------------------------------
open import Data.Nat
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module TerminationExample where

-- Some true lemmas about natural numbers. Proofs omitted for brevity.
postulate
  lemma-refl : ∀ n -> n ≤ n
  lemma-suc : ∀ n -> n ≤ suc n
  lemma-lt-trans : ∀ {n m k} -> n < m -> m < k -> n < k
  lemma-elim : ∀ {m n} {C : Set} -> m < suc n -> (m < n -> C) -> (m ≡ n -> C) -> C

module Inductive-as-Record where

  -- A natural number is inductive if all smaller numbers are inductive.
  record Inductive (n : ℕ) : Set where
    inductive
    constructor cind
    field cind-field : ∀ {m} -> m < n -> Inductive m

module Inductive-as-Datatype where

  -- The same thing defined as a datatype.
  data Inductive : (n : ℕ) -> Set where
    cind : ∀ {n} -> (∀ {m} -> m < n -> Inductive m) -> Inductive n

open Inductive-as-Record   
-- or: open Inductive-as-Datatype
  
-- All natural numbers are inductive. We prove it here, because the
-- following examples don't work correctly when it is just a
-- postulate. The details of the proof do not matter.
lemma-inductive : ∀ n -> Inductive n
lemma-inductive zero = cind (λ ())
lemma-inductive (suc n) = cind (λ p → lemma-elim p case1 case2)
  where
  ih = lemma-inductive n

  inductive-less : ∀ {n m} -> m < n -> Inductive n -> Inductive m
  inductive-less p (cind h) = cind (λ q → h (lemma-lt-trans q p))

  case1 : ∀ {m} -> m < n -> Inductive m
  case1 q = inductive-less q ih

  case2 : ∀ {m} -> m ≡ n -> Inductive m
  case2 q = subst Inductive (sym q) ih

-- The Fibonacci sequence, defined by strong recursion.
fibonacci-aux : (n : ℕ) -> Inductive n -> ℕ
fibonacci-aux 0 (cind h) = 1
fibonacci-aux 1 (cind h) = 1
fibonacci-aux (suc (suc n)) (cind h) = fibonacci-aux n (h proof1) + fibonacci-aux (suc n) (h proof2)
  where
  proof1 : n < suc (suc n)
  proof1 = s≤s (lemma-suc n)

  proof2 : suc n < suc (suc n)
  proof2 = lemma-refl (suc (suc n))

fibonacci : (n : ℕ) -> ℕ
fibonacci n = fibonacci-aux n (lemma-inductive n)

-- This definition is sufficient to evaluate closed terms. For
-- example, pressing Ctrl-n here will evaluate to 89:
test1 = {! fibonacci 10 !}

-- However, partial evaluation of open terms is not possible. The
-- following evaluates to a closure with unevaluated proof
-- obligations. This makes sense, because (lemma-inductive n) does not
-- evaluate to canonical form when n is an open term.
test2 = λ n -> {! fibonacci (suc (suc n)) !}

-- We can solve this problem by making the Inductive argument
-- irrelevant:

fibonacci'-aux : (n : ℕ) -> .(Inductive n) -> ℕ
fibonacci'-aux 0 (cind h) = 1
fibonacci'-aux 1 (cind h) = 1
fibonacci'-aux (suc (suc n)) (cind h) = fibonacci'-aux n (h proof1) + fibonacci'-aux (suc n) (h proof2)
  where
  proof1 : n < suc (suc n)
  proof1 = s≤s (lemma-suc n)
   proof2 : suc n < suc (suc n)
  proof2 = lemma-refl (suc (suc n))

fibonacci' : (n : ℕ) -> ℕ
fibonacci' n = fibonacci'-aux n (lemma-inductive n)

-- Now both closed and open terms can be reduced:

-- Term in hole evaluates to: 89
test3 = {! fibonacci' 10 !}

-- Term in hole evaluates to: fibonacci'-aux n _ + fibonacci'-aux (suc n) _
test4 = λ n -> {! fibonacci' (suc (suc n)) !}

----------------------------------------------------------------------

Note that everything works as advertised, and especially, the
Inductive argument can be made irrelevant, as it should be.

However, now change "open Inductive-as-Record" to "open
Inductive-as-Datatype" and re-typecheck the example again. 

The function fibonacci'-aux now gives the error:
"Cannot pattern match cind h against irrelevant type".

So we are caught between a rock and a hard place:

* If we use records, then we can make the inductive argument
  irrelevant, but we cannot prove termination by structural recursion
  on it. (Here, the function passes termination checking anyway, but
  in the integer division example, it does not).

* If we use datatypes, then we can prove termination on the second
  argument, but we cannot make that argument irrelevant.

As far as I can see, there is no logical reason for not being able to
do both at the same time - it is just a nasty coincidence because each
of the record and datatype mechanisms lack certain features, both of
which we happen to need simultaneously here.

It seems to me that solving this problem would require a (minor)
language extension. There are several possible solutions:

* add a "no-eta" option to record definitions, to turn off eta.
  Then allow termination checking on the resulting record
  constructors. Alternatively, as suggested by Andreas, turn off eta
  for all inductive records, and permit termination checking on their
  constructors. 

* Or: give a special status to datatype constructors when the datatype
  has a unique constructor. Permit such constructors to be matched
  against irrelevant arguments. (One could also permit such unique
  constructors to be used in let-bindings, as is already permitted for
  record constructors).

Is there a solution to my problem that uses only existing language
features? I tried many combinations of irrelevance and structural
induction, but I did not manage to find a combination where I could
prove termination by structural induction on an irrelevant argument.

Thanks, -- Peter

Andreas Abel wrote:
> 
> Peter,
> 
> this is not a bug, this is intended behavior.  Record constructors do 
> not count as structural increase.  This is due to eta for records.
> 
> Consider the following example of an inductive record:
> 
> ---------------------------
> open import Common.Equality
> 
> record Empty : Set where
>    inductive
>    constructor inn
>    field out : Empty
> 
> {-# TERMINATING #-}
> loop : Empty → {A : Set} → A
> loop (inn e) = loop e
> 
> -- internally, the clause is represented as
> -- loop x = loop (out x)
> 
> postulate x : Empty
> 
> y : Empty
> y = loop x
> 
> test : x ≡ y
> test = refl
> -----------
> 
> loop needs to be rejected since in internal representation, the matching 
> on a record constructor on the lhs is replaced by projections on the 
> rhs.  (This internal representation serves to make matching against 
> record constructors lazy, which is the right thing if there is eta.)
> 
> Your example is similar.
> 
> However, there is indeed some inconsistency, as Agda turns off eta for 
> recursive records (to avoid looping).
> 
>    eta-Inductive : ∀ {n} (i : Inductive n) →
>      i ≡ cind (Inductive.cind-field i)
>    eta-Inductive i = refl
>    -- FAILS
> 
> You can force Agda to consider eta with pragma
> 
>    {-# ETA Inductive #-}
> 
> then eta-Inductive succeeds.
> 
> Maybe Agda should be more consequent and regard constructors of non-eta 
> records like constructors of data types.
> 
> Cheers,
> Andreas
> 
> On 18.12.2014 20:06, Peter Selinger wrote:
> > I have a question about termination checking. The following example
> > has been vexing me. I do not understand why the function
> > RecordExample.div-aux fails termination checking, while both
> > RecordExample.fibonacci and DataTypeExample.div-aux pass it.
> >
> > Agda version 2.4.2.2. Might this be a subtle bug in the termination
> > checker with respect to inductive records? Or is there something
> > obvious that I am missing.
> >
> > Any help appreciated! Thanks, -- Peter
> >
> > P.S.: although the example works if I use a datatype, I prefer using a
> > record, because then I can use the constructor in let-bindings, and
> > also when matching against irrelevant arguments. In the case of
> > datatypes, these two kinds of pattern matches are not allowed.
> >
> > ----------------------------------------------------------------------
> > open import Data.Nat
> > open import Relation.Nullary
> >
> > module TerminationExample where
> >
> > -- Some true lemmas about natural numbers. Proofs omitted for brevity.
> > postulate
> >    lemma-refl : ∀ n -> n ≤ n
> >    lemma-suc : ∀ n -> n ≤ suc n
> >    lemma-order : ∀ {n m} -> ¬ n ≤ m -> n > 0
> >    lemma-minus : ∀ n m -> n > 0 -> n ∸ suc m < n
> >
> > module RecordExample where
> >
> >    -- A natural number is inductive if all smaller numbers are inductive.
> >    record Inductive (n : ℕ) : Set where
> >      inductive
> >      constructor cind
> >      field cind-field : ∀ {m} -> m < n -> Inductive m
> >
> >    -- All natural numbers are inductive. Proof omitted for brevity.
> >    postulate
> >      lemma-inductive : ∀ n -> Inductive n
> >
> >    -- Auxiliary function for integer division. The termination checker
> >    -- fails but I don't know why.  The third argument is clearly
> >    -- decreasing:
> >    --
> >    -- h proof < cind h
> >
> >    {-# NON_TERMINATING #-}
> >    div-aux : (n : ℕ) -> ℕ -> Inductive n -> ℕ
> >    div-aux n zero (cind h) = zero
> >    div-aux n (suc m) (cind h) with n ≤? suc m
> >    div-aux n (suc m) (cind h) | yes p = zero
> >    div-aux n (suc m) (cind h) | no p = suc (div-aux (n ∸ suc m) (suc m) (h proof))
> >      where
> >      proof : n ∸ suc m < n
> >      proof = lemma-minus n m (lemma-order p)
> >
> >    -- Integer division.
> >    div : ℕ -> ℕ -> ℕ
> >    div n m = div-aux n m (lemma-inductive n)
> >
> >    -- However, it does not*always*  fail. Here is a situation that is a
> >    -- priori very similar, but termination checking succeeds without
> >    -- any problems.
> >    fibonacci-aux : (n : ℕ) -> Inductive n -> ℕ
> >    fibonacci-aux 0 (cind h) = 1
> >    fibonacci-aux 1 (cind h) = 1
> >    fibonacci-aux (suc (suc n)) (cind h) = fibonacci-aux n (h proof1) + fibonacci-aux (suc n) (h proof2)
> >      where
> >      proof1 : n < suc (suc n)
> >      proof1 = s≤s (lemma-suc n)
> >
> >      proof2 : suc n < suc (suc n)
> >      proof2 = lemma-refl (suc (suc n))
> >
> >
> > module DataTypeExample where
> >
> >    -- Redoing the same example using an inductive datatype instead of
> >    -- an inductive record.
> >
> >    data Inductive : (n : ℕ) -> Set where
> >      cind : ∀ {n} -> (∀ {m} -> m < n -> Inductive m) -> Inductive n
> >
> >    postulate
> >      lemma-inductive : ∀ n -> Inductive n
> >
> >    -- This time it works like a charm.
> >    div-aux : (n : ℕ) -> ℕ -> Inductive n -> ℕ
> >    div-aux n zero (cind h) = zero
> >    div-aux n (suc m) (cind h) with n ≤? suc m
> >    div-aux n (suc m) (cind h) | yes p = zero
> >    div-aux n (suc m) (cind h) | no p = suc (div-aux (n ∸ suc m) (suc m) (h proof))
> >      where
> >      proof : n ∸ suc m < n
> >      proof = lemma-minus n m (lemma-order p)
> >
> >    -- Integer division.
> >    div : ℕ -> ℕ -> ℕ
> >    div n m = div-aux n m (lemma-inductive n)
> > ----------------------------------------------------------------------
> 
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
> 
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>