[Agda] termination checking

[Andreas Abel]

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/