[Agda] Positivity checker

[Peter Dybjer]

This induction principle is fine, but does not naturally reflects the  
generation of all elements. I doubt that its existence helps  
justifying the interest in accepting D n as a data type.

Peter

On Dec 9, 2008, at 1:55 PM, Ulf Norell wrote:

>
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081210/d826a5eb/attachment-0001.html