Irrelevant termination measure [Re: [Agda] termination checking]

[Andreas Abel]

Hi Peter,

thanks for your message.  Again, I have to disappoint you a bit, but can 
offer a workaround.

First, the bad news.  As irrelevance is definitional, termination via an 
irrelevant argument cannot be supported by the usual term model of 
dependent types:

If  x : Inductive n  appears in an irrelevant position, then we are 
allowed to replace it by any value of the same type, in particular with

   cind (cind-field x) : Inductive n

where cind-field is the inverse to cind, which is also definable for the 
data-version of Inductive.

This means that strong normalization is broken in the term model if you 
allow recursion on Inductive.

I don't know whether there are better models that can prove strong 
normalization in the presence of recursion on irrelevant arguments.

The good news is that there is a backdoor that makes your data-version 
of Inductive go through with irrelevant matching.

   {-# OPTIONS --experimental-irrelevance #-}

allows you to match irrelevantly on single-constructor data types.  Be 
warned that you are entering the wild if you use this option.  No models 
to back you up.  ;-)

Cheers,
Andreas

On 19.12.2014 03:12, Peter Selinger wrote:
> 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  <><      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/