A Simpler Lambda Calculus

被引：2

作者：

Jay, Barry ^{[1
]}

机构：

[1] Univ Technol Sydney, Ctr Artificial Intelligence, Sydney, NSW, Australia

来源：

PROCEEDINGS OF THE 2019 ACM SIGPLAN WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM '19) | 2019年

关键词：

lambda calculus; closures; closure calculus; EXPLICIT SUBSTITUTIONS;

D O I：

10.1145/3294032.3294085

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Closure calculus is simpler than pure lambda-calculus as it does not mention free variables or index manipulation, variable renaming, implicit substitution, or any other meta-theory. Further, all programs, even recursive ones, can be expressed as normal forms. Third, there are reduction-preserving translations to calculi built from combinations of operators, in the style of combinatory logic. These improvements are achieved without sacrificing three fundamental properties of lambda-calculus, being a confluent rewriting system, supporting the Turing computable numerical functions, and supporting simple typing.

引用

页码：1 / 9

页数：9

共 23 条

[1]

ABADI M, 1990, CONFERENCE RECORD OF THE SEVENTEENTH ANNUAL ACM SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, P31, DOI 10.1145/96709.96712

[2]

[Anonymous], 1972, Proceedings of the ACM Annual Conference - Volume 2. ACM'72, DOI [DOI 10.1023/A:1010027404223, DOI 10.1145/800194.805852]

[3]

Barendregt H., 1991, J. Funct. Program, V1, P229

[4]

Barendregt H.P., 1984, The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics, V103

[5] Jones-Optimal Partial Evaluation by Specialization-Safe Normalization [J].

Brown, Matt ;

Palsberg, Jens .

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (POPL)

[6] Typed Self-Evaluation via Intensional Type Functions [J].

Brown, Matt ;

Palsberg, Jens .

ACM SIGPLAN NOTICES, 2017, 52 (01) :415-428

[7]

Curry H.B., 1972, COMBINATORY LOGIC, VII.

[8] Closed reduction:: explicit substitutions without α-conversion [J].

Fernández, M ;

Mackie, I ;

Sinot, FR .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2005, 15 (02) :343-381

[9]

Hindley J. R., 2008, Lambda-Calculus and Combinators: An Introduction

[10]

Hindley Roger., 1986, Introduction to Combinators and Lambda-Calculus

← 1 2 3 →