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

edit

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

  1. alpha conversion -  
  2. beta reduction -  
  3. eta reduction -  

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,   is the substitution of the name   by the lambda expression   in lambda expression  .
  • Free Variable Set   is the set of variables that do not belong to a lambda abstraction in  .

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

edit

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.  
  2.  
  3.  
  4.  

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

edit

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

  1.  
  2.  
  3.  

Substitution Operator

edit

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

  1.  
  2.  
  3.  
  4.  

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

edit

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. [1]

  - Free Variable Set Comment   - Bound Variable Set Comment
  where x is a variable   where x is a variable
  Free variables of M excluding x   Bound variables of M plus x.
  Combine the free variables from the function and the parameter   Combine the bound variables from the function and the parameter

Usage;

edit

References

edit
  1. ^ Barendregt, Henk; Barendsen, Erik (March 2000), Introduction to Lambda Calculus (PDF)