The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Thu, 4 Sep 2014 14:04:17 +0100
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Strictly positive inductive types

Hello.

Le 11/08/2014 23:23, Maxime Dénès a écrit :

Coq does reject non strictly positive types, even if they are positive. Otherwise it would be inconsistent in general, as you could encode the argument given in [1].

Non-strictly positive types are not necessarily inconsistent. In Inductively defined types, COLOG'88, Thierry Coquand and Christine Paulin show that a particular "big" non-strictly positive type is inconsistent (section 3.1, page 59). I call it "big" for it has a constructor having a type argument that is not a parameter. The constructor has type ((X->Prop)->Prop)->X. However, "small" (e.g. replace Prop by bool) non-strictly positive types are harmless.

I was just about to ask wether this is obvious, but I realise that this is justified by the impredicative encoding of such types. That is while they don’t have exactly the same reduction rules we can exploit the encoding in the semantics. 

Is there any use of positive inductive types? I lack any intuition about such types. They seem to be a formalist invention.

Thorsten

Best regards,

Frédéric.

I don't know of any flag to disable this check but a patch should not be too hard to write. What's your use case?

Maxime.

[1] A new paradox in type theory, T. Coquand - Proceedings 9th Int. Congress of Logic, Methodology, 1991

On 08/11/2014 05:04 PM, Luke Maurer wrote:

AFAIK, Coq always accepts types that are positive but not strictly so. And it never accepts non-positive occurrences (unlike with Agda, Coq's termination checking is mandatory).

- Luke

On Aug 11, 2014, at 1:54 PM, <elilobo.v AT gmail.com> wrote:

How to force Coq to accept non-strictly positive inductive types? Is there a
flag like --no-positivity-check in Agda, to do it?

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.