A Meta Lambda Calculus with Cross-Level Computation

作者：Tobisawa Kazunori^*

来源：ACM Sigplan Notices, 2015, 50(1): 383-393.

DOI：10.1145/2676726.2676976

• lambda calculus
• metavariables
• textual substitution
• dynamic binding

We propose meta lambda calculus lambda* as a basic model of textual substitution via metavariables. The most important feature of the calculus is that every beta-redex can be reduced regardless of whether the beta-redex contains meta-level variables or not. Such a meta lambda calculus has never been achieved before due to difficulty to manage binding structure consistently with alpha-renaming in the presence of meta-level variables. We overcome the difficulty by introducing a new mechanism to deal with substitution and binding structure in a systematic way without the notion of free variables and alpha-renaming.
Calculus lambda* enables us to investigate cross-level terms that include a certain type of level mismatch. Cross-level terms have been regarded as meaningless terms and left out of consideration thus far. We find that some cross-level terms behave as quotes and 'eval' command in programming languages. With these terms, we show a procedural language as an application of the calculus, which sheds new light on the notions of stores and recursion via metalevel variables.

• 出版日期2015-1