Misplaced Pages

Revision as of 14:48, 27 March 2014

A "let expression" associates a function with a restricted ]. Let expressions may be defined from Mathematics of for computer science.

The let expression may be considered as a lambda abstraction applied to a value. A let expression may also be considered as a conjunction of expressions, within an existential quantifier which restricts the scope of the variable.

The let expression is present in many functional languages to allow the local definition of expression, for use in defining another expression. The let-expression is present in many functional languages in two forms; let or "letrec". Letrec is an extension of the let expression which uses the Fixed-point combinator to implement recursion.

History

Dana Scotts LCF language was a stage in the evolution of lambda calculus into modern functional languages. This language introduce the let expression, which has appeared in most functional languages since that time.

The languages Miranda, ML, and more recently Haskel have evolved based on LCF.

State-full imperative languages such as and Pascal essentially implement a let expression, to implement restricted scope of functions, in block structures.

Definition

A lambda abstraction represents a function without a name. This is source of the inconsistency in the definition of a lambda abstraction. However lambda abstractions may be composed to represent a function with a name. In this form the inconsistency is removed. The lambda term,

${\displaystyle (\lambda f.z)\ (\lambda x.y)}$

is equivalent to defining the function ${\displaystyle f}$ by ${\displaystyle f\ x=y}$ in the expression ${\displaystyle z}$, which may be written as the let expression;

${\displaystyle \operatorname {let} f\ x=y\operatorname {in} z}$

The let expression is understandable as a natural language expression. Used in Dana Scotts LCF language the let expression represents the substitution of a variable for a value. The substitution rule describes the implications of equality as substitution. The let expression is the conjunction of two expressions, with the substitution rule from one expression applied to the other.

Let definition

The let expression is the conjunction of expressions. In functional languages the let expression is also used to limit scope. In mathematics scope is described by quantifiers. The let expression is a conjunction within an existential quantifier.

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

The meaning of the let expression allows the substitution to be applied to another expression. This substitution may be applied within a restricted scope, to a sub expression. The natural use of the let expression is in application to a restricted scope. These results may be derived to describe how the scope may be restricted;

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\to \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)}$

${\displaystyle x\in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\to \operatorname {let} x:G\operatorname {in} E\ F=(\operatorname {let} x:G\operatorname {in} E)\ F}$

${\displaystyle x\not \in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\to \operatorname {let} x:G\operatorname {in} E\ F=E\ F}$

From this definition the following standard definition of a let expression, as used in a functional language may be derived.

${\displaystyle x\not \in \operatorname {FV} (y)\to (\operatorname {let} x:x=y\operatorname {in} z)=z=\lambda x.z\ y}$

To derive this result, first assume,

${\displaystyle x\not \in \operatorname {FV} (L)}$

then

${\displaystyle L\ (\operatorname {let} x:x=y\operatorname {in} z)}$

${\displaystyle \iff (\operatorname {let} x:x=y\operatorname {in} L\ z)}$

${\displaystyle \iff x=y\land L\ z}$

Using the rule of substitution,

${\displaystyle \iff x=y\land (L\ z)}$

${\displaystyle \iff x=y\land (L\ z)}$

${\displaystyle \iff x=y\land L\ z}$

${\displaystyle \implies L\ z}$

so for all L,

${\displaystyle L\operatorname {let} x:x=y\operatorname {in} z\implies L\ z}$

Let ${\displaystyle L\ X=(X=K)}$ where K is a new variable. then,

${\displaystyle (\operatorname {let} x:x=y\operatorname {in} z)=K\implies z=K}$

So,

${\displaystyle \operatorname {let} x:x=y\operatorname {in} z=z}$

But from the mathematical interpretation of a beta reduction,

${\displaystyle \lambda x.z\ y=z}$

Here if y is a function of a variable x, it is not the same x as in z. Alpha renaming may be applied. So we must have,

${\displaystyle x\not \in \operatorname {FV} (y)}$

so,

${\displaystyle x\not \in \operatorname {FV} (y)\to \operatorname {let} x:x=y\operatorname {in} z=\lambda x.z\ y}$

This result is represented in a functional language in an abbreviated form, where the meaning is unambiguous;

${\displaystyle x\not \in \operatorname {FV} (y)\to (\operatorname {let} x=y\operatorname {in} z)=z=\lambda x.z\ y}$

Here the variable x is implicitly recognised as both part of the equation defining x, and the variable in the existential quantifier.

Joining let expressions

Let expressions may be defined with multiple variables,

${\displaystyle (\exists v...\exists w\exists xE\land F)\iff \operatorname {let} v,...,w,x:E\operatorname {in} F}$

then it can be derived,

${\displaystyle x\not \in FV(E)\to (\exists v...\exists w\exists xE\land F)\iff (\exists v...\exists w(E\land \exists xF))}$

so,

${\displaystyle x\not \in FV(E)\to (\operatorname {let} v,...,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,...,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)}$

Conversion between lambda calculus and let expressions

The following rules describe the equivalence of lambda and let expressions,

Name	Law
Eta-reduction equivalence	${\displaystyle f\ x=y\equiv f=\lambda x.y}$
Let-Lambda equivalence	${\displaystyle f\not \in FV(E)\to (\operatorname {let} f:f=E\operatorname {in} L\equiv (\lambda f.L)\ E)}$ (where f is a variable name).
Let combination	${\displaystyle w\not \in FV(E)\to (\operatorname {let} v,w:E\land F\operatorname {in} L\equiv \operatorname {let} v:E\operatorname {in} \operatorname {let} w:F\operatorname {in} L)}$ (where f is a variable name).

Meta-functions will be given that describe the conversion between lambda and let expressions. A meta-function is a function that takes a program as a parameter. The program is data for the meta-program. The program and the meta program are at different meta-levels.

The following conventions will be used to distinguish program from the meta program,

• Square brackets will be used to represent function application in the meta program.
• Capital letters will be used for variables in the meta program. Lower case letters represent variables in the program.
• ${\displaystyle \equiv }$ will be used for equals in the meta program.
• ${\displaystyle \_}$ represents a dummy variable, or an unknown value.

For simplicity the first rule given that matches will be applied. The rules also assume that the lambda expressions have been pre-processed so that each lambda abstraction has a unique name.

The substitution operator is used extensively. The expression ${\displaystyle L}$ means substitute every occurrence of G in L by S and return the expression. The definition used is extended to cover the substitution of expressions, from the definition given on the Lambda calculus page. The matching of expressions should compare expressions for alpha equivalence (renaming of variables).

Conversion from lambda to let expressions

The following rules describe how to convert from a Lambda expression to a let expression, without altering the structure.

1. ${\displaystyle \operatorname {de-lambda} \equiv V}$
2. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} \ \operatorname {de-lambda} }$
3. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} }$
4. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {de-lambda} =\operatorname {de-lambda} }$
5. ${\displaystyle \operatorname {de-lambda} \equiv \operatorname {let-combine} \operatorname {in} E]}$
6. ${\displaystyle V\not \in \operatorname {FV} \to \operatorname {de-lambda} \equiv \operatorname {let-combine} \operatorname {in} V]}$
7. ${\displaystyle V\neq W\to \operatorname {let-combine} \equiv \operatorname {let} V,W:E\land F\operatorname {in} G}$
8. ${\displaystyle \operatorname {let-combine} \equiv \operatorname {let} V:E\operatorname {in} F}$

Rule 6 creates a unique variable V, as a name for the function.

Example

For example the Y combinator,

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

is converted to,

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p}$

Rule	Lambda Expression
6	${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle V\not \in \operatorname {FV} \to \operatorname {de-lambda} }$ ${\displaystyle V=p,F=f,E=\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)}$ ${\displaystyle \operatorname {let-combine} \operatorname {in} V]}$
4	${\displaystyle \operatorname {let-combine} \operatorname {in} p]}$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle E=p\ f,F=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {de-lambda} =\operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} =\operatorname {de-lambda} }$ ${\displaystyle \operatorname {let-combine} =\operatorname {de-lambda} \operatorname {in} p]}$
5	${\displaystyle \operatorname {let-combine} =\operatorname {de-lambda} \operatorname {in} p]}$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle F=x,E=f\ (x\ x),L=(\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {let-combine} \operatorname {in} E]}$ ${\displaystyle \operatorname {let-combine} \operatorname {in} f\ (x\ x)]}$
3	${\displaystyle \operatorname {let-combine} =\operatorname {let-combine} \operatorname {in} f\ (x\ x)]\operatorname {in} p]}$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle F=x,P=x,E=f\ (x\ x)}$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} }$
9	${\displaystyle \operatorname {let-combine} =\operatorname {let-combine} \operatorname {in} f\ (x\ x)]\operatorname {in} p]}$ ${\displaystyle \operatorname {let-combine} \operatorname {in} f\ (x\ x)]}$ ${\displaystyle \operatorname {let-combine} }$ ${\displaystyle Y=\operatorname {let} x:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)}$ ${\displaystyle Y}$ ${\displaystyle \operatorname {let} x:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)}$
9	${\displaystyle \operatorname {let-combine} =\operatorname {let} x:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)\operatorname {in} p]}$ ${\displaystyle \operatorname {let-combine} }$ ${\displaystyle Y=\operatorname {let} p:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)]\operatorname {in} p}$ ${\displaystyle Y}$ ${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)\operatorname {in} p}$
4	${\displaystyle \operatorname {let} p:\operatorname {de-lambda} =\operatorname {let} x:\operatorname {de-lambda} \operatorname {in} f\ (x\ x)\operatorname {in} p}$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle E=x\ x,F=f\ (x\ x)}$ ${\displaystyle \operatorname {de-lambda} =\operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} =\operatorname {de-lambda} }$
2	${\displaystyle \operatorname {let} p:\operatorname {de-lambda} =\operatorname {let} x:\operatorname {de-lambda} =\operatorname {de-lambda} \operatorname {in} f\ (x\ x)\operatorname {in} p}$ ${\displaystyle \operatorname {de-lambda} ,\operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} ,\operatorname {de-lambda} ,\operatorname {de-lambda} ,}$ ${\displaystyle M_{1}=p,N_{1}=f,M_{2}=x,N_{2}=x,M_{3}=f,N_{3}=x\ x}$ ${\displaystyle \operatorname {de-lambda} \ \operatorname {de-lambda} ,\operatorname {de-lambda} \ \operatorname {de-lambda} ,\operatorname {de-lambda} \ \operatorname {de-lambda} }$ ${\displaystyle \operatorname {de-lambda} \ \operatorname {de-lambda} ,\operatorname {de-lambda} \ \operatorname {de-lambda} ,\operatorname {de-lambda} \ \operatorname {de-lambda} \ \operatorname {de-lambda} }$
1	${\displaystyle \operatorname {let} p:\operatorname {de-lambda} \ \operatorname {de-lambda} =\operatorname {let} x:\operatorname {de-lambda} \ \operatorname {de-lambda} =\operatorname {de-lambda} \ (\operatorname {de-lambda} \ \operatorname {de-lambda} )\operatorname {in} f\ (x\ x)]\operatorname {in} p}$ ${\displaystyle \operatorname {de-lambda} }$ ${\displaystyle V}$
	${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ x=f\ (x\ x)\operatorname {in} f\ (x\ x)]\operatorname {in} p}$

Conversion from let to lambda expressions

These rule reverse the conversion described above. They convert from a let expression to a Lambda expression, without altering the structure. Not all let expressions may be converted using these rules. The rules assume that the expressions are already arranged as if they had been generated by de-lambda.

1. ${\displaystyle \operatorname {get-lambda} =\operatorname {get-lambda} }$
2. ${\displaystyle \operatorname {get-lambda} =\operatorname {de-let} }$
3. ${\displaystyle \operatorname {de-let} \equiv \lambda V.\operatorname {de-let} }$
4. ${\displaystyle \operatorname {de-let} \equiv \operatorname {de-let} \ \operatorname {de-let} }$
5. ${\displaystyle \operatorname {de-let} \equiv V}$
6. ${\displaystyle V\not \in FV]\to \operatorname {de-let} \equiv \operatorname {get-lambda} }$
7. ${\displaystyle V\not \in FV]\to \operatorname {de-let} \equiv (\lambda V.\operatorname {de-let} )\ \operatorname {get-lambda} }$
8. ${\displaystyle W\not \in \operatorname {FV} ]\to \operatorname {de-let} \equiv \operatorname {de-let} }$
9. ${\displaystyle V\in \operatorname {FV} ]\to \operatorname {de-let} \equiv \operatorname {de-let} \operatorname {in} L]}$
10. ${\displaystyle W\in \operatorname {FV} ]\to \operatorname {de-let} \equiv \operatorname {de-let} \operatorname {in} \operatorname {let} W:F\operatorname {in} L]}$

There is no exact structural equivalent in lambda calculus for let expressions that have free variables that are used recursively. In this case some addition of parameters is required. The last two rules add these parameters.

Examples

For example the let expression obtained from the Y combinator,

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p}$

is converted to,

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))}$

Rule	Lambda Expression
6	${\displaystyle \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle V=p,E=p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)}$ ${\displaystyle \operatorname {get-lambda} }$
1	${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle F=p,G=p,V=f,E=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)}$ ${\displaystyle \operatorname {get-lambda} }$
2	${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle F=p,E=\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)}$ ${\displaystyle \operatorname {de-let} }$
3	${\displaystyle \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle V=f,E=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)}$ ${\displaystyle \lambda V.\operatorname {de-let} }$
7	${\displaystyle \lambda f.\operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle V\not \in FV]\to \operatorname {de-let} }$ ${\displaystyle V=x,E=x\ q=f\ (q\ q),L=f\ (x\ x)}$ ${\displaystyle (\lambda V.\operatorname {de-let} )\ \operatorname {get-lambda} }$
4	${\displaystyle (\lambda x.\operatorname {de-let} )\ \operatorname {get-lambda} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle M=f,N=(x\ x)}$ ${\displaystyle \operatorname {de-let} \ \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} \ \operatorname {de-let} }$
4	${\displaystyle (\lambda x.\operatorname {de-let} \ \operatorname {de-let} )\ \operatorname {get-lambda} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle M=x,N=x}$ ${\displaystyle \operatorname {de-let} \ \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} \ \operatorname {de-let} }$
5	${\displaystyle (\lambda x.\operatorname {de-let} \ (\operatorname {de-let} \ \operatorname {de-let} ))\ \operatorname {get-lambda} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle V}$
1	${\displaystyle (\lambda x.f\ (x\ x))\ \operatorname {get-lambda} }$ ${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle F=x,G=x,V=q,E=f\ (q\ q)}$ ${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle \operatorname {get-lambda} }$
2	${\displaystyle (\lambda x.f\ (x\ x))\ \operatorname {get-lambda} }$ ${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle \operatorname {get-lambda} }$ ${\displaystyle F=x,E=\lambda q.f\ (q\ q)}$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$
3	${\displaystyle (\lambda x.f\ (x\ x))\ \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle V=q,E=f\ (q\ q)}$ ${\displaystyle \lambda V.\operatorname {de-let} }$ ${\displaystyle \lambda q.\operatorname {de-let} }$
4	${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda q.\operatorname {de-let} )}$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle M_{1}=f,N_{1}=q\ q}$ ${\displaystyle \operatorname {de-let} \ \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} \ \operatorname {de-let} }$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle M_{2}=q,N_{2}=q}$ ${\displaystyle \operatorname {de-let} \ \operatorname {de-let} }$
5	${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda q.\operatorname {de-let} \ (\operatorname {de-let} \ \operatorname {de-let} ))}$ ${\displaystyle \operatorname {de-let} }$ ${\displaystyle }$ ${\displaystyle V}$
	${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))}$