In computer science, a "let" expression associates a function definition with a restricted scope.
The "let" expression may also be defined in mathematics, where it associates a Boolean condition with a restricted scope.
The "let" expression may be considered as a lambda abstraction applied to a value.
The let-expression is present in some functional languages in two forms; let or "let rec".
Let rec is an extension of the simple let expression which uses the fixed-point combinator to implement recursion.
The languages Scheme,[2] ML, and more recently Haskell[3] have inherited let expressions from LCF.
[citation needed] A closely related "where" clause, together with its recursive variant "where rec", appeared already in Peter Landin's The mechanical evaluation of expressions.
Like the if-then-else the type returned by the expression is not necessarily Boolean.
The syntax may also support the declaration of existentially quantified variables local to the let expression.
In Haskell, let may be mutually recursive, with the compiler figuring out what is needed.
The natural use of the let expression is in application to a restricted scope (called lambda dropping).
These rules define how the scope may be restricted; where F is not of type Boolean.
then, So, But from the mathematical interpretation of a beta reduction, 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, so, This result is represented in a functional language in an abbreviated form, where the meaning is unambiguous; Here the variable x is implicitly recognised as both part of the equation defining x, and the variable in the existential quantifier.
Let expressions may be defined with multiple variables, then it can be derived, so, The Eta reduction gives a rule for describing lambda abstractions.
This rule along with the two laws derived above define the relationship between lambda calculus and let expressions.
To avoid the potential problems associated with the mathematical definition, Dana Scott originally defined the let expression from lambda calculus.
The simple, non recursive let expression was defined as being syntactic sugar for the lambda abstraction applied to a term.
The fixed-point combinator may be represented by the expression, This representation may be converted into a lambda term.
A lambda abstraction does not support reference to the variable name, in the applied expression, so x must be passed in as a parameter to x.
Using the eta reduction rule, gives, A let expression may be expressed as a lambda abstraction using, gives, This is possibly the simplest implementation of a fixed point combinator in lambda calculus.
However one beta reduction gives the more symmetrical form of Curry's Y combinator.
This is achieved by replacing multiple function definitions with a single function definition, which sets a list of variables equal to a list of expressions.
There is no exact structural equivalent in lambda calculus for let expressions that have free variables that are used recursively.
The general case needs an extra level of looping which makes the meta function a little more difficult.