It's all Geek to me?

Jacob Fugal lukfugl at
Wed Feb 21 12:55:27 MST 2007

On 2/21/07, Steve <smorrey at> wrote:
> But what the heck does it mean to "contain the lambda calculus properly"?

Distilled from,
the calculus is defined as:

  * A set of identifiers
  * A grammar over those identifiers for forming lambda expressions
  * A set of equivalence relations for determining if two lambda
expressions are "equal"

My interpretation of a language X "containing" the calculus would be that:

1) For any expression A in X, there is at least one lambda expression
A' that represents the same calculation as A. We'll call A' equivalent
to A.


2) For any two expressions A and B in X, the A and B are equivalent if
and only if A' and B' are equivalent for all (A', B') where A' is a
lambda expression to A and B' is a lambda expression equivalent to B.

In more informal language: "X contains the lambda calculus if
translating a program in X into the lambda calculus and then
manipulating the translated program according to the rules of the
lambda calculus will always leave the result of the program

Jacob Fugal

More information about the PLUG mailing list