Lambda Calculus

Lambdascope

Lambdascope:
Another optimal implementation of the lambda-calculus

We have presented an implementation of the lambda-calculus
in the spirit of the calculational approach [...], and which
is fully in the traditions of calculi with explicit substitution
and of graph implementations of term rewriting. As far as
we know it is the first such calculus which is optimal in the sense of Levy. Moreover, as far as we know this is the
first optimal calculus featuring only a single scope delimiter
node instead of the usual two, croissants and brackets,
which by force eliminates the problems which are caused by
having more than one scope node [...]. The calculus
is simple, half a page suffices [...] to describe
it, and completely reduction-based (no semantic read-back
in the implementation). As a consequence it can be trivially
implemented in any (modern) programming language.

Remembering our discussion on atoms of PLs (such as scope and name), I decided this paper might be of interest.

Foundational Calculi for Programming Languages (intro)

Since pi calculus is a hot topic lately, Pierce's Foundational Calculi for Programming Languages might be of interest as an introduction. It very briefly introduces and justifies foundational calculi in general, spends about 10 pages on lambda calculus, then builds on that with another 7 pages on pi calculus.

A New Approach to Abstract Syntax with Variable Binding

Pitts and Gabbay, A New Approach to Abstract Syntax with Variable Binding, FAC 2001.

In the lambda calculus, the particular choice of variable names - even free variables - is irrelevant. Names serve two purposes:

  • as mnemonics to help human readers understand their role, and
  • to distinguish variables that are meant to be different and unify variables that are meant to be the same.

In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with capture-avoiding substitution, the Barendregt variable convention, gensym, and the like. These are all ways of getting around the fact that we've committed to a particular name when we really shouldn't have cared what the name was.

There are several standard ways to deal with this. Generating fresh names with gensym is awkward and forces the implementer to reimplement binding and substitution from scratch for each new object language; not to mention its violation of referential transparency. de Bruijn indices remove the variable names but are hard to read and understand. Higher-order abstract syntax implements binders in the object language as functions in the metalanguage, in order to reuse the built-in mechanisms of binding and substitution; but by mixing higher-order values in algebraic datatypes, structural induction is hard to recover.

This paper introduces a theory of fresh names that restores algebraic reasoning, referential transparency, and structural induction to algebraic datatypes with a HOAS-like notation for introducing binders into an abstract syntax. This is the set-theoretical basis for the authors' work on FreshML and FreshO'Caml, which we've discussed a little bit on LtU in the past.

Barbara Partee: Reflections of a Formal Semanticist as of Feb 2005

What follows will be a very subjective and personal view, as much my own history and development in the field and how things looked through my eyes as about the development of the field itself.

This essay is a longer version of the introductory essay in (Partee 2004). The introductory essay was first written in this long form in February 2003, but had to be cut down to about half the size to fit in the book...

This essay is about natural language semantics, but you'll find old friends here: lambdas, bindings, types, quantifiers etc. If you are lazy, go directly to footnote 25...

No surprise, really, if you follow the links we give here from time to time about TLGs and such.

The Church Project

http://types.bu.edu or http://www.church-project.org

The Church Project investigates the foundations, design principles and implementation techniques of programming languages and related systems. The overall goal is the development of software technology that performs better and is more reliable. The project is named in honor of Alonzo Church, the inventor of the lambda calculus.

Four major research efforts (supported by various funding bodies including EC, EPSRC, and NSF) are presently undertaken by project participants:

  • Compiling with Flow Types
  • Compositional Analysis
  • Programming with Dependent Types (DML) (Xanadu)
  • Linear Naming and Computation

We previously linked to a document on this site, but not the site itself.

The pi-Calculus in Direct Style

The pi-Calculus in Direct Style

We introduce a calculus which is a direct extension of both the
lambda and the pi calculi. We give a simple type system for it, that
encompasses both Curry's type inference for the lambda-calculus,
and Milner's sorting for the pi-calculus as particular cases of
typing. We observe that the various continuation passing style
transformations for lambda-terms, written in our calculus, actually
correspond to encodings already given by Milner and others
for evaluation strategies of lambda-terms into the pi-calculus. Furthermore,
the associated sortings correspond to well-known
double negation translations on types. Finally we provide an
adequate cps transform from our calculus to the pi-calculus.

This shows that the latter may be regarded as an "assembly
language", while our calculus seems to provide a better
programming
notation for higher-order concurrency.

a.k.a. Blue Calculus

Normal-order direct-style beta-evaluator with syntax-rules, and the repeated applications of call/cc

Oleg's presentation at the workshop in honor of Daniel Friedman is great fun as usual. The topic of repeated applications of call/cc has been mentioned on LtU previously, a few years ago. New this time: the full and correct beta-normalizer written as a direct-style syntax-rule. The normalizer implements calculus of explicit substitutions. The talk presents probably the shortest (and the fastest) normal-order beta-normalizer as a (stand-alone) Scheme macro. Another new feature is the discussion of self-applications of delimited continuation operators. The talk mentions incidentally that shift, control, shift0 and other, less-delimited control operators are the members of the same family: gshift/greset.

Hot stuff.

Call-by-Name, Call-by Value and the Lambda Calculus

Gordon Plotkin's Call-by-Name, Call-by-Value and the Lambda Calculus (Theoretical Computer Science , Vol. 1, pp. 125-159, 1975), is available online.

The fundamental point made in the paper should seem natural to most LtU readers: In order to reason about programming language semantics one should look for programming language/calculus pairs.

The paper contrasts CBN and CBV, and shows the differences between the Lambda Calculi appropriate for describing each of them.

Theoretical Pearl: Church numerals, twice!

Ralf Hinze. Theoretical Pearl: Church numerals, twice! Journal of Functional Programming, 2004. To appear.

This pearl explains Church numerals, twice. The first explanation links Church numerals to Peano numerals via the well-known encoding of data types in the polymorphic LC. This view suggests that Church numerals are folds in disguise. The second explanation, which is more elaborate, but also more insightful, derives Church numerals from first principles, that is, from an algebraic specification of addition and multiplication. Additionally, we illustrate the use of the parametricity theorem by proving exponentiation as reverse application correct.

A simple concept is used to demonstrate several interesting and useful techniques.

Reflections on reflection - Henk Barendregt

(Link)

Here's something to exercise both brain hemispheres. Henk Barendregt needs no introduction for many LtU readers - he literally wrote "the book" on the lambda calculus, and that only hints at the profound impact his work has had on lambda calculus and type theory.

The page linked above lists two overlapping papers, both about reflection:

Reflection plays in several ways a fundamental role for our existence. Among other places the phenomenon occurs in life, in language, in computing and in mathematical reasoning. A fifth place in which reflection occurs is our spiritual development. In all of these cases the effects of reflection are powerful, even downright dramatic. We should be aware of these effects and use them in a responsible way.

A prototype situation where reflection occurs is in the so called lambda calculus. This is a formal theory that is capable of describing algorithms, logical and mathematical proofs, but also itself.

As the first paragraph quoted above implies, the scope of these two papers extends far beyond the lambda calculus, into fields such as biology and meditation. Between the two papers, there's something for everyone:

"Reflection and its use, from science to meditation" is wide-ranging, covering reflection related to living cells, formal languages, mathematics, art, computers, and the human mind.

"Reflection and its use, with an emphasis on languages and lambda calculus", focuses specifically on reflection in formal languages, including combinatory logic and lambda calculus.

XML feed