The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

True, I had meant to say that the type was empty.
Generally, I think that think kind of definition should be okay, since the 
non-strictly positive occurrence is "treated positively" in the same way that 
the recursive structure of a closure might have a non-strictly positive 
occurrence for the type of the dictionary's values, but due to the treatment 
by the dictionary, this circularity must always bottom out.

concretely:
Inductive Value : Type :=
| closure : lambda-expr -> (dictionary Variable Value) -> Value

To make the metatheory work out, there need to be positivity annotations on 
type arguments, but I haven't given much thought into the deeper meaning of 
this (gotta graduate).

My high level feeling is that it should work, but it could make recursion 
very hard to prove terminating (though would make many programming patterns I 
use in daily life actually possible).

-Ian

----- Original Message -----
From: "gallais @ ensl.org" 
<guillaume.allais AT ens-lyon.org>
To: "J. Ian Johnson" 
<ianj AT ccs.neu.edu>
Cc: "Arthur Azevedo de Amorim" 
<arthur.aa AT gmail.com>,
 
coq-club AT inria.fr
Sent: Friday, October 5, 2012 11:10:49 AM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] Indices in mutual inductives

Well, this is just saying that B is empty. But it's usually ok to
define empty sets!

Inductive B : Set :=
  BIntro : B -> B.
Fixpoint omega (b : B) : False := match b with
  BIntro b' => omega b'
end.

--
gallais


On 5 October 2012 16:00, J. Ian Johnson 
<ianj AT ccs.neu.edu>
 wrote:
> Fixpoint omega (b : B) (a : A b) : False :=
>  match a with
>  | AIntro (BIntro b'' a') => omega b'' a'
>  end.
>
> ----- Original Message -----
> From: "Arthur Azevedo de Amorim" 
> <arthur.aa AT gmail.com>
> To: 
> coq-club AT inria.fr
> Sent: Friday, October 5, 2012 10:42:20 AM GMT -05:00 US/Canada Eastern
> Subject: [Coq-Club] Indices in mutual inductives
>
> Dear list,
>
> Coq rejects the following definition
>
> Inductive A : B -> Type :=
> | AIntro : forall b, A b
>
> with B : Type :=
> | BIntro : forall b (a : A b), B
> | Base : forall b, B.
>
> Is there any metatheoretical reason for this? Does anyone have an
> example showing that it would make the logic inconsistent?
>
> Thanks
>
> --
> Arthur Azevedo de Amorim