The Coq mailing list

[Marino Miculan <miculan AT dimi.uniud.it>]

On 07/dic/05, at 06:30, Fabrice Lemercier wrote:

> Hello
>
> I want to encode lambda calculus is Coq in such a way that it uses  
> the variable binding mechanism of Coq.  But the following  
> definition is rejected by Coq because of the non strictly positive  
> occurrence of  Term  in  (Term -> Term) -> Term.
>
> Inductive Term : Set :=
>   abs : (Term -> Term) -> Term
> | app : Term -> Term -> Term.
>
> Is there a workaround?
>
> Fabrice

If you do not need  induction nor recursion, you can go for an "open"  
definition (a la LF):

Parameter Term : Set.
Parameter abs : (Term -> Term) -> Term.
Parameter app : Term -> Term -> Term.


Otherwise, if you want to exploit the inductive types of Coq, you  
have to use a separate type for variables, e.g. as follows:

Parameter Var:Set.

Inductive Term : Set :=
  var : Var -> Term
|  abs : (Var -> Term) -> Term
| app : Term -> Term -> Term.

Coercion var : Var >-> Term.


In this way, alpha-conversion comes for free, but substitution is not  
delegated to the metalanguage and must be encoded explicitly.

This technique is called "weak HOAS" (or second order abstract  
syntax); also, the development of metatheoretic results about systems  
encoded in this way is facilitated by the so-called "theory of  
contexts", that is some basic principles about Var and terms of type  
(Var->Term) which can be added to the signature as Axioms.

See the following papers for full details:

Marino Miculan, Developing (Meta)Theory of lambda-calculus in the  
Theory of Contexts.
In Proceedings of the Workshop on MEchanized Reasoning about  
Languages with variable bINding (MERLIN 2001). ENTCS 58.1, Elsevier,  
2001.

Furio Honsell, Marino Miculan, Ivan Scagnetto, An axiomatic approach  
to metareasoning on systems in higher-order abstract syntax.
In Proceedings of ICALP'01, Number 2076 in Lecture Notes in Computer  
Science, pages 963-978, 2001.

Furio Honsell, Marino Miculan, Ivan Scagnetto, Translating  
Specifications from Nominal Logic to CIC with the Theory of Contexts.
In R. Pollack, editor, Proceedings of MERLIN'05. ACM DL, 2005.


-marino


--
  Marino Miculan - Department of Mathematics and Computer Science
University of Udine  - via delle Scienze 206, 33100 Udine - Italy
vox: +39-043255-8486 - fax: +39-043255-8499 - mob: +39-3292606452
mail:miculan at dimi uniud it  http://www.dimi.uniud.it/~miculan/