The Coq mailing list

["Stefan Monnier" <monnier+lists.coq/news/ AT rum.cs.yale.edu>]

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