[Agda] Positivity checker

[Ulf Norell]

On Tue, Dec 9, 2008 at 12:56 PM, Peter Dybjer <peterd at chalmers.se> wrote:

>
> On Dec 8, 2008, at 10:10 AM, Nils Anders Danielsson wrote:
>
>>
>>> The reason why this data type is ok, is because it is isomorphic to the
>>> corresponding family defined by induction on n.
>>> But what is the induction principle? Except induction on n?
>>>
>>
>> Do you suggest that one could inadvertently introduce new (stronger)
>> induction principles by accepting this type (or similar types)?
>>
>
> It depends on what the termination checker would do when pattern matching
> on this data type. But my feeling is that there is no natural induction
> principle associated with this type, except induction on n.


The termination checker accepts functions of the form

foo base = ...
foo (step f) = ... foo (f d) ...

for arbitrary d's. It doesn't care that d happens to have the same type has
the argument we're recursing over. Formulating that as an induction
principle you end up with

elim-D : (P : {n : Nat} -> D n -> Set) ->
         P base ->
         ({n : Nat}{f : D n -> D n} ->
           ((d : D n) -> P (f d)) -> P (step f)) ->
         {n : Nat}(d : D n) -> P d

which is easily proved by induction on n:

data Base   : Set where base : Base
data Step A : Set where step : (A -> A) -> Step A

D : Nat -> Set
D zero    = Base
D (suc n) = Step (D n)

elim-D : (P : {n : Nat} -> D n -> Set) ->
         P base ->
         ({n : Nat}{f : D n -> D n} ->
           ((d : D n) -> P (f d)) -> P (step f)) ->
         {n : Nat}(d : D n) -> P d
elim-D P b s {zero }  base    = b
elim-D P b s {suc n} (step f) =
  s \d -> elim-D P b s (f d)

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081209/aa04e641/attachment.html