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

[Gabriel Scherer]

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

What does this mean in term of sized types? In the naive
interpretation where size types are just another syntax for naturals
(or ordinals) that the termination-checker understands primitively,
sizes are irrelevant *and* they pass for the decreasing argument of
the recursive definition.
In sized definitions, the recursive functions actually recurses over
an inductive that is indexed with the size. Then the question becomes
whether this is still sound when the size-indexed inductive is
irrelevant.

On Fri, Dec 19, 2014 at 3:40 PM, Andreas Abel <abela at chalmers.se> wrote:
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda