The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 07/10/2013 17:33, Pierre Boutillier a écrit :
> Hi
>
> Yes
> On 07/10/2013 16:57, Frédéric Blanqui wrote:
> > Generalized Iteration and Coiteration for Higher-Order Nested Datatypes
> > <http://www2.tcs.ifi.lmu.de/%7Eabel/fossacs03.pdf> Andreas Abel, Ralph
> > Matthes and Tarmo Uustalu.
> > /Foundations of Software Science and Computation Structures (FoSSaCS
> > 2003)/,  LNCS 2620
> > <http://www.springer.de/cgi/svcat/search_book.pl?isbn=3-540-00897-7>
> tells us that Michiel's example should be accepted.
>
> Yes (as far as I understand) the restriction on reccursive arguments are
> made because polymorphic types can postpone negative type occurence that
> must be rejected as you explain here :
> On 07/10/2013 16:57, Frédéric Blanqui wrote:
> > Hello.
> >
> > Thanks Pierre for your example but I do not really understand how it is
> > related to Michiel's problem.
> >
> > In your example, the problem does not seem to be related to polymorphism
> > only. Here, the polymorphism hides a negative type, namely
> > (instantiating P by I):
> >
> > Inductive I : Type := C: (I (*negative occurrence of I*) -> I) -> I.
> > (*rejected by Coq*)
> >
> > And, elimination on negative types is not normalizing [Mendler 86]. You
> > proposed:
> >
> > Fixpoint f i : A (*anything*) := match i with C x => f (x i) end.
> >
> > Then, taking i := C (fun i => i), you get: f i ->iota f ((fun i => i) i)
> > ->beta f i.
> >
> > More generally, with:
> >
> > Inductive I : Type := C: (I -> A (*anything*)) -> I. (*rejected by Coq*)
> >
> > Fixpoint p i := match i with C x => x end.
> >
> > and d := fun x => p x x, you get: d (C d) ->beta p (C d) (C d) ->iota d
> > (C d).
> I don't undestand your point in
> > Also, it is not clear to me why "polymorphic arguments of a constructors
> > must not be [admissible subterms]." Otherwise, we could not have records
> > with type fields in Coq. Take for instance:
> >
> > Inductive I (*: Type*) := C : forall A (*: Type*), B A (*anything*) -> I.
> >
> > Fixpoint p1 i := match i with C A _ => A end.
> >
> > Fixpoint p2 i := match i as i return p1 i with C _ b => b end.
> p1 and p2 are accepted, they are not really fixpoints by the way, they
> do not do recursive calls !
> Do you want to say that a term of skeleton "fix f (x : I) := E (f (p2
> x))" (with E a close term) should be accepted ?
Hello Pierre.

My point was, rather as a remark, that you do not need to define a 
recursive function to get non-termination. Simple, apparently innocuous 
projections like p above or below, may be enough, if your inductive type 
does not satisfy some conditions.

Best regards,

Frédéric.

> These 2 points are really interresting :
> > On the other hand, the definitions of p1 and p2 are rejected by Coq if I
> > is declared of sort Prop and A of sort Type. Indeed, in this case, the
> > calculus is not normalizing and not consistent [Coquand, LICS'86].
> >
> > Finally, note that positivity ensures termination and consistency when
> > constructor arguments are at the object level [Mendler] but not always
> > when they are at the type level [Coquand-Paulin, COLOG'88]:
> >
> > Inductive I : Prop := C : ((I->Prop)->Prop)->I.
> >
> > Allowing Fixpoint p i := match i with C x => x end, turns C into an
> > injection from (I->Prop)->Prop to I, but there cannot be any injection
> > from (A->Prop)->Prop to A, nor from A->Prop to A, whatever A is.
> >
> > Best regards,
> >
> > Frédéric.
> Pierre B.