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

Distilled from http://en.wikipedia.org/wiki/Lambda_calculus#Formal_definition,
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.

and

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
unchanged."

Jacob Fugal

/*
PLUG: http://plug.org, #utah on irc.freenode.net
Unsubscribe: http://plug.org/mailman/options/plug
Don't fear the penguin.
*/

Reply via email to