The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

If you add to the simply typed lambda-calculus a type Dynamic with an  
introduction rule analogous to your constructor plus a 'typecase'  
construct for eliminating Dynamics, you can write non-terminating  
programs.  But it's not clear to me whether injectivity gives you  
that much power.

    - Benjamin


On Jun 9, 2008, at 7:44 PM, Adam Chlipala wrote:
> Andrew McCreight wrote:
> > I could be wrong, but this looks very similar to a question that  
> > was asked a few years ago:
> >
> > http://coq.inria.fr/mailing-lists/coqclub/200201/msg00001.html
> >
> > In short, the answer was no.
>
> I think that post only says definitively that injectivity isn't a  
> theorem.  I'm interested in whether CIC + injectivity for Dyn is  
> consistent, which is a different question.  It looks like the  
> poster in the message you referenced wasn't sure of the answer to  
> that question.
>
> > On Mon, Jun 9, 2008 at 3:37 PM, Adam Chlipala <adamc AT hcoop.net  
> > <mailto:adamc AT hcoop.net>> wrote:
> >
> >     Does anyone know if it would be consistent with (impredicative
> >     Set) CIC to assert the injectivity of the [Dyn] constructor below
> >     as an axiom?
> >
> >     Inductive dynamic : Set :=
> >      | Dyn : forall T, T -> dynamic.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club