Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Weakening the negative occurrence restriction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Weakening the negative occurrence restriction


chronological Thread 
  • From: "Stefan Monnier" <monnier+lists.coq/news/ AT rum.cs.yale.edu>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Weakening the negative occurrence restriction
  • Date: 14 Oct 2002 16:30:39 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Newsgroups: lists.coq

A while back I un-brightly suggested:
>> I.e. move the positiveness restriction from the inductive definition
>> to the elimination construct.
>> Is there such a construct that is still strongly normalizing ?
>> Does it make any sense ?

To which Benjamin politely pointed out:
> Once you have negative occurences, you do not need any fixpoint
> construct anymore to loop.

So here's another proposal, hopefully less ridiculous:

In case there is a non-strictly positive occurrence, disallow case analysis.
I.e. only provide constructors but don't provide any elimination construct.

That should be enough to allow the definition of a typed lambda-calculus
in HOAS (i.e. with a negative occurrence) and its proof of soundness
as long as the proof only needs induction on the type derivation rather
than on the terms.

I'm sure I'm missing something obvious again, tho.


        Stefan




Archive powered by MhonArc 2.6.16.

Top of Page