User:Thepigdog/Lambda Calculus - canonical naming definition

The standard definition uses some rules that are not explained, as the basis of the definition of Lambda Calculus. These rules relate to naming of variables in the Lambda Calculus.

In general the problem of how variables may be renamed is quite difficult. However the problem is resolved in a compiler by identifying, in the parser, which variable object each variable symbol refers to.

This definition takes a similar approach by substituting all names with canonical names, which are constructed based on the position of the definition of the name in the expression. The approach is analogous to what a compiler does, but has been adapted to work within the constraints of mathematics. Mathematics does not have a new operator, so constructing canonical names is used instead of new, in identifying each name object.

Semantics

The execution of a lambda expression proceeds using the following reductions and transformations,

1. alpha conversion - $\operatorname {alpha-con} (a)\to \operatorname {canonym} [A,P]=\operatorname {canonym} [a[A],P]$
2. beta reduction - $\operatorname {beta-redex} [\lambda p.b\ v]=b[p:=v]$
3. eta reduction - $x\not \in \operatorname {FV} (f)\to \operatorname {eta-redex} [\lambda x.(f\ x)]=f$

where,

• canonym is a renaming of a lambda expression to give the expression standard names, based on the position of the name in the expression.
• Substitution Operator, $b[p:=v]$ is the substitution of the name $p$ by the lambda expression $v$ in lambda expression $b$.
• Free Variable Set $\operatorname {FV} (f)$ is the set of variables that do not belong to a lambda abstraction in $f$.

Execution is performing beta reductions and eta reductions on sub expressions in the canonym of a lambda expression until the result is a lambda function (abstraction) in the normal form.

All alpha conversions of a lambda expression are considered to be equivalent.

Canonym - Canonical Names

Canonym is a function that takes a lambda expression and renames all names canonically, based on their positions in the expression. This might be implemented as,

1. $\operatorname {canonym} [L,Q]=\operatorname {canonym} [L,O,Q]$
2. $\operatorname {canonym} [\lambda p.b,M,Q]=\lambda \operatorname {name} (Q).\operatorname {canonym} [b,M[p:=Q],Q+N]$
3. $\operatorname {canonym} [X\ Y,x,Q]=\operatorname {canonym} [X,x,Q+F]\ \operatorname {canonym} [Y,x,E+S]$
4. $\operatorname {canonym} [x,M,Q]=\operatorname {name} (M[x])$

Where, N is the string "N", F is the string "F", S is the string "S", + is concatenation, and "name" converts a string into a name

Map Operators

Map from one value to another if the value is in the map. O is the empty map.

1. $O[x]=x$
2. $M[x:=y][x]=y$
3. $x\neq z\to M[x:=y][z]=M[z]$

Substitution Operator

If L is a lambda expression, x is a name, and y is a lambda expression; $L[x:=y]$ means substitute x by y in L. The rules are,

1. $(\lambda p.b)[x:=y]=\lambda p.b[x:=y]$
2. $(X\ Y)[x:=y]=X[x:=y]\ Y[x:=y]$
3. $z=x\to (z)[x:=y]=y$
4. $z\neq x\to (z)[x:=y]=z$

Note that rule 1 must be modified if it is to be used on non canonically renamed lambda expressions. See Changes to the substitution operator.

Free and Bound Variable Sets

The set of free variables of a lambda expression, M, is denoted as FV(M). This is the set of variable names that have instances not bound (used) in a lambda abstraction, within the lambda expression. They are the variable names that may be bound to formal parameter variables from outside the lambda expression.

The set of bound variables of a lambda expression, M, is denoted as BV(M). This is the set of variable names that have instances bound (used) in a lambda abstraction, within the lambda expression.

The rules for the two sets are given below.

$\operatorname {FV} (M)$ - Free Variable Set	Comment	$\operatorname {BV} (M)$ - Bound Variable Set	Comment
$\operatorname {FV} (x)=\{x\}$	where x is a variable	$\operatorname {BV} (x)=\{\}$	where x is a variable
$\operatorname {FV} (\lambda x.M)=\operatorname {FV} (M)\cap \neg \{x\}$	Free variables of M excluding x	$\operatorname {BV} (\lambda x.M)=\operatorname {BV} (M)\cup \{x\}$	Bound variables of M plus x.
$\operatorname {FV} (M\ N)=\operatorname {FV} (M)\cup \operatorname {FV} (N)$	Combine the free variables from the function and the parameter	$\operatorname {BV} (M\ N)=\operatorname {BV} (M)\cup \operatorname {BV} (N)$	Combine the bound variables from the function and the parameter

Usage;

• The Free Variable Set, FV is used above in the definition of the eta-reduction.
• The Bound Variable Set, BV, is used in the rule for beta-redex of non canonical lambda expression.

Links

• Lambda Calculus