The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

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 ?

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.