The Coq mailing list

[Louis Noizet <louis.noizet AT irisa.fr>]

Sorry for hitting send too fast !


Hi, I'm trying to implement some kind of non-deterministic λ-calculus.
Anyway, the terms are something like that

Inductive term :=
| var: string -> term
| func: var -> body -> term
with body :=
| choose: list body -> body
| ret: term -> body
| apply: var -> term -> body
| letin: var -> body -> body -> body

And now I'm trying to define the type of values.
So a functional value is a relation between values, because it takes a value 
and produces some number of values.

I would like to write something like that :

Inductive value : Type :=
| base: forall t: Type, t -> value
| func: (value -> value -> Prop) -> value.


Of course, this is not working because of non-positivity. 

The obvious solution would be to use closures, but we want to be able to 
externally define functions (directly in gallina, via a relation) without 
having to explicitly define a body for it.

I thought for sure somebody must have already had a similar issue.

By the way, we did a version using step-indexing, but it's not entirely 
satisfactory, because it makes the definition hard to use to make a proof.

Thanks in advance !

-- 
Louis

Attachment: pEpkey.asc
Description: application/pgp-keys