The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Ralph Matthes wrote:
[...] the very idea of such a constructor is already found in Section
4.3.2 of Christine Paulin's habilitation thesis of 1996).

That's Chapter 4, Section 4.3.2 .

Since Ralph brought up plain system F, recall that

Definition lam: forall (X:Prop), ((X -> X)-> X) -> (X -> X -> X) -> X.

checks in system F.  I'm echoing Thorsten in pointing this out.
However, unlike strictly positive impredicative intersections, no
constructor is definable for the "constructor" (X -> X)-> X.

--Randy

On Thu, Sep 4, 2014 at 10:27 AM, Ralph Matthes 
<Ralph.Matthes AT irit.fr>
 wrote:
> Maybe there are only very few use cases since there is no support. In plain
> system F, there is no problem at all with positive but not strictly positive
> inductive types. I exploited this in my TLCA 2001 paper "Parigot's Second
> Order lambda-mu-Calculus and Inductive Types", with the inductive type #rho
> that has a constructor S of type ((#rho -> bot) -> bot) -> #rho (i.e.,
> elimination of double negation - as I understood later, the very idea of
> such a constructor is already found in Section 4.3.2 of Christine Paulin's
> habilitation thesis of 1996). In system F^omega, one can have positive
> inductive families that are not recognized as strictly positive in the Coq
> system. There, this is not a question of being twice on the left of an arrow
> but rather of nesting of type transformations. This has been studied in
> several papers, in particular profoundly in "Iteration and coiteration
> schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333(1-2):
> 3-66 (2005)" by Andreas Abel, Tarmo Uustalu and myself.
>
> I would be happy to see "natural" algorithmic examples involving
> non-strictly positive inductive types and families. As I wrote above, people
> might not be encouraged to search for them if tool support is missing.
>
> Best,    Ralph
>
>
> Le 04/09/2014 15:32, Maxime Dénès a écrit :
>
>> Hi,
>>
>> Indeed, that's what I meant by "in general".
>>
>> Note that Coq doesn't allow positive types that are not strictly positive
>> even when they are small, which probably makes it more conservative than it
>> could be. On the other hand, I don't know if there are many use cases that
>> are impacted.
>>
>> Best,
>>
>> Maxime.
>>
>> On 09/04/2014 09:04 AM, Frédéric Blanqui wrote:
>>>
>>> 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 <http://dx.doi.org/10.1007/3-540-52335-9_47>,
>>> 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.
>>>
>>> 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?
>>>>
>>>>
>>>
>>
>
>