The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 23/10/2012 13:12, AUGER Cédric wrote:
> Some restriction of the positivity condition is required to ensure 
> soundness.

Indeed.

> But Coq positivity restriction is too strong and should allow more
> terms.

I imagine this problem to be dual of the guardedness of fixpoints, so
there is plenty of room for extension. But I'm way lower-level in this
kind of consideration.

> What exactly would your patch do?

This would be trivial and very syntactical, thus not a deep modification
of the current implementation.

The patch would just add the following rule to the strict positivity
condition checker :

« If M is occuring stricly positively in N, then it also occurs stricly
positively in match P with ... | p => N | ... end ».

This seems legal, because it's already the case with the lambda
abstraction, which is (from the linear logic point of view) just a
special case of pattern-matching.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature