The Coq mailing list

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

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).

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.

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].

The fact that a type parameter (the one of list in Michiel's example) is instanciated by a constant or something else is not a problem either. See for instance:

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes Andreas Abel, Ralph Matthes and Tarmo Uustalu.
Foundations of Software Science and Computation Structures (FoSSaCS 2003),  LNCS 2620

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.

Le 05/10/2013 16:45, Pierre Boutillier a écrit :

(1) Is there a theoretical reason it shouldn't? 

No

Something I'm just not seeing?

Well yes, but it is normal that you don't see it :-)

All arguments of constructors are NOT admissible subterms, polymorphic arguments of a constructors must not be !
See the example

Inductive I : Type := C: (forall (P : Type), P->P) -> I.

Definition Paradox : False :=
(fix ni (i :I):False := match i with | C f => ni (f i) end)
(C (fun (P :Type) (x :P)  => x)).

to understand why !

Coq registers "admissible for recursive calls" arguments of a constructor at definition time. Consequently, as the first argument of cons in 

Inductive list (A : Type) : Type := nil : list A | cons : A -> list A -> list A.

has an unknown type "A". it will never be OK to use it (or one of its subterm) as a subterm of the recursive argument ! (Yes, Coq should make the check at usage time. Everything would be fine and your trouble as the one of every Coq user before you would be solved)

There is sometime a work-around. In "match x with | cons a _ => ... | _ => ... end", if 'x' is the recursive argument, we have just seen why sadly 'a' will never be recognize as a subterm but if 'x' is a subterm already then 'a' will be one.

As a consequence, inner fixpoints (has the fold hidden in Robbert solution) sometime saves you … (the argument of inner is a subterm)

Pierre B.

Le 5 oct. 2013 à 15:57, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> a écrit :

On 10/05/2013 03:51 PM, Michiel Helvensteijn wrote:

(2) What is the recommended way of solving this? In my search I've
found some descriptions that might be related, but I'd really
appreciate a simple example.

The following alternative definition does through:

Fixpoint my_sum' (l: NatTree) : nat :=
 match l with
 | leaf n => n
 | inner l => fold_right plus 0 (map my_sum' l)
 end.
Definition my_sum (l : list NatTree) : nat :=
 fold_right plus 0 (map my_sum' l).