coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "J. Ian Johnson" <ianj AT ccs.neu.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Strictly positive inductive types
- Date: Thu, 4 Sep 2014 13:24:13 -0400 (EDT)
Non-strictly positive types are definitely a natural occurrence. I give this
example everywhere when I'm frustrated with Coq's limitations, so I'll give
it again.
Closures. Closures are the pair of a lambda term and an explicit
substitution. A substitution is a finite function - a dictionary. You can't
define closures with an abstract dictionary due to the self-reference, even
though it's well-founded. You have to lock in a representation that will be a
pain to work with.
Inductive Closure : Set :=
clos : Lam -> dict Variable Closure -> Closure.
Say we decided to represent the finite function with just a function. This is
a positive but not strictly positive type.
Inductive Closure : Set :=
clos : Lam -> (Variable -> Closure) -> Closure.
More recently, I've been modeling a language for automatically abstracting
reduction semantics, where some values are allowed to be "external."
An external value is a pair of an external space descriptor (contains
functions implementing important operations like join, equality,
cardinality), and a value of the type the descriptor states is the type of
that space's values.
Operations for join, equality and cardinality all get the context of where
they're being called from, to make informed decisions, but this means a big
mutual recursive knot to tie, since states contain stores, which map to
values, of which external values are a member.
I'd prefer to define the descriptor as a dependent record, but I can't.
Inductive ExternalDescriptor : Set :=
ex_desc : forall t : Set, (* carrier type *)
(* join *) (State -> Store -> t -> t -> t) ->
(* equal *) (State -> Store -> t -> t -> EqRes) ->
(* cardinality *) (t -> AbsN) -> ExternalDescriptor
with
PreTerm : Set :=
...stuff...
| External : forall E : ExternalDescriptor, match E with ex_desc t _ _ _ => t
end -> PreTerm (* oops, can't do induction/non-recursion *)
with
TAbs_ty : Set :=
| TAbs : set PreTerm -> (* and some way to have a "dependent dictionary" of
external descriptors to values of the descriptor's carried type *) -> TAbs_ty
with
Term : Set :=
pre : PreTerm -> Term
| abs : TAbs_ty -> Term
with
EqRes : Set :=
Equal : set Refinement -> set (Term * Term) -> EqRes
| Disequal : set Refinement -> set (Term * Term) -> EqRes
| May : set (Term * Term) -> EqRes
| Both : set Refinement -> set Refinement -> set (Term * Term) -> EqRes
(* Term sets are to stop cyclic equality checking since terms can contain
pointers into the store. *)
(* Also, can't have "set"s here in Coq, even though it's well-founded *)
with Refinement := dict Address Term (* nope, not allowed *)
with Store := dict Address TAbs_ty (* nope *).
Just having an s-expression-like thing with sets or maps instead of lists is
just impossible in Coq. Also in OCaml because functors for maps or sets don't
make sense in a lot of cases.
I'm pretty sure Agda's termination checker would also barf at this type too,
but I haven't tried it.
-Ian
----- Original Message -----
From: "Randy Pollack"
<rpollack AT inf.ed.ac.uk>
To: "Coq-Club Club"
<coq-club AT inria.fr>
Sent: Thursday, September 4, 2014 12:45:25 PM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] Strictly positive inductive types
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?
>>>>
>>>>
>>>
>>
>
>
- Re: [Coq-Club] Strictly positive inductive types, Frédéric Blanqui, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Maxime Dénès, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Ralph Matthes, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Randy Pollack, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Ralph Matthes, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Randy Pollack, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Ralph Matthes, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Thorsten Altenkirch, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Frédéric Blanqui, 09/08/2014
- Re: [Coq-Club] Strictly positive inductive types, Andrés Sicard-Ramírez, 09/05/2014
- Re: [Coq-Club] Strictly positive inductive types, Daniel Schepler, 09/05/2014
- Re: [Coq-Club] Strictly positive inductive types, Andrés Sicard-Ramírez, 09/05/2014
- Re: [Coq-Club] Strictly positive inductive types, Daniel Schepler, 09/05/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Strictly positive inductive types, J. Ian Johnson, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Maxime Dénès, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, J. Ian Johnson, 09/04/2014
- Re: [Coq-Club] Strictly positive inductive types, Thorsten Altenkirch, 09/05/2014
- Re: [Coq-Club] Strictly positive inductive types, Dan Doel, 09/05/2014
- Re: [Coq-Club] Strictly positive inductive types, Thorsten Altenkirch, 09/05/2014
- Re: [Coq-Club] Strictly positive inductive types, Maxime Dénès, 09/04/2014
Archive powered by MHonArc 2.6.18.