Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423734 | Electronic Notes in Theoretical Computer Science | 2008 | 17 Pages |
Abstract
We present a simple but expressive lambda-calculus whose syntax is populated by variables which behave like meta-variables. It can express both capture-avoiding and capturing substitution (instantiation). To do this requires several innovations, including a key insight in the confluence proof and a set of reduction rules which manages the complexity of a calculus of contexts over the ‘vanilla’ lambda-calculus in a very simple and modular way. This calculus remains extremely close in look and feel to a standard lambda-calculus with explicit substitutions, and good properties of the lambda-calculus are preserved.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics