skip to main content
10.1145/2676726.2676976acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

A Meta Lambda Calculus with Cross-Level Computation

Published: 14 January 2015 Publication History

Abstract

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 meta-level variables.

References

[1]
M. Abadi, L. Cardelli, P.-L. Curien and J.-J. Lévy. 1991. Explicit substitutions. Journal of Functional Programming 1, 4, 375--416.
[2]
Daisuke Bekki. 2009. Monads and meta-lambda calculus. In New Frontiers in Artificial Intelligence (JSAI 2008), LNAI 5447, 193--208.
[3]
Daisuke Bekki and Kenichi Asai. 2010. Representing covert movements by delimited continuations. In New Frontiers in Artificial Intelligence (JSAI-isAI 2009), LNAI 6284, 161--180.
[4]
Mathieu Boespflug and Brigitte Pientka. 2011. Multi-level contextual type theory. In Proceedings of the 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011), EPTCS 71, 29--43.
[5]
N. G. de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 75, 5, 381--392.
[6]
Laurent Dami. 1998. A lambda-calculus for dynamic binding. Theoretical Computer Science 192, 2, 201--231.
[7]
Rowan Davies. 1996. A temporal-logic approach to binding-time analysis. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS '96), 184--195.
[8]
Gilles Dowek, Thérèse Hardin and Claude Kirchner. 2000. Higher order unification via explicit substitutions. Information and Computation 157, 183--235.
[9]
Murdoch J. Gabbay. 2005. A NEW calculus of contexts. In Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP '05), 94--105.
[10]
Murdoch J. Gabbay and Stéphane Lengrand. 2009. The lambda-context calculus (extended version). Information and Computation 207, 12, 1369--1400.
[11]
Murdoch J. Gabbay and Dominic P. Mulligan. 2009. Two-level lambda-calculus. Electronic Notes in Theoretical Computer Science 246, 107--129.
[12]
Masatomo Hashimoto and Atsushi Ohori. 2001. A typed context calculus. Theoretical Computer Science 266, 249--272.
[13]
Moe Masuko and Daisuke Bekki. 2011. Categorical semantics of meta-lambda calculus (in Japanese). In Informal Proceedings of the 13th JSSST Workshop on Programming and Programming Languages, 60--74.
[14]
Aleksandar Nanevski, Brigitte Pientka and Frank Pfenning. 2003. A modal foundation for meta-variables. In Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN '03), 1--6.
[15]
Aleksandar Nanevski, Frank Pfenning and Brigitte Pientka. 2008. Contextual modal type theory. ACM Transactions on Computational Logic 9, 3, Article 23, 49 pages.
[16]
Masahiko Sato, Takafumi Sakurai and Yukiyoshi Kameyama. 2002. A simply typed context calculus with first-class environments. Journal of Functional and Logic Programming 2002, 1--41.
[17]
Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama and Atsushi Igarashi. 2003. Calculi of meta-variables. In Computer Science Logic (CSL 2003), LNCS 2803, 484--497.
[18]
Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama and Atsushi Igarashi. 2008. Calculi of meta-variables. Frontiers of Computer Science in China 2, 1, 12--21.

Cited By

View all
  • (2019)BNF-Style Notation as It Is Actually UsedIntelligent Computer Mathematics10.1007/978-3-030-23250-4_13(187-204)Online publication date: 3-Jul-2019

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. dynamic binding
  2. lambda calculus
  3. metavariables
  4. textual substitution

Qualifiers

  • Research-article

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)6
  • Downloads (Last 6 weeks)1
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2019)BNF-Style Notation as It Is Actually UsedIntelligent Computer Mathematics10.1007/978-3-030-23250-4_13(187-204)Online publication date: 3-Jul-2019

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media