lambda.txt

The definition of lambda calculus used in this project, syntax and simantics.
This may vary from the formal definition of lambda caluclus as the project
demands it.

====Elements:
  There are the parts that are written out:

Function: _._
  The left-hand side is the function's header, the right-hand side is the
function's body. The header is a variable, while the body can be any element.

Application: (_ _)
  The left-hand side is the called function and the right-hand side is its
argument. Both can be any element.

Variable: _
  An atom unit consisting of a identifier. They can be equal to or not equal
to other variables.

====Forms:
  There are the forms that the govern, in addition to their own rules, how
elements are put together.

Bound and Free Variables:
  A bound variable is any variable that occurs within the body of a function
that has an equal variable in its header. It can occur at any level of nesting
within the body.
  A free variable is any variable that is not bound. They are currantly not
allowed as they carry no meaning.

Closed and Open Functions:
  A closed function is one that all variables within it are bound. They do not
have to be bound to this function's header, instead they can be bound to
functions within the function's body.
  An open function is any function that is not closed. Currantly they can only
occur as part of the body of a closed function.

Expression:
  Either a closed function, or a function application whose left and right
hand sides are expressions.
  Currently the system only works with expressions that meet this definition
as it eliminates some harder to deal with sub-cases.

====Operations:
  There are how the elements and forms are transformed as part of the
calculation.

Evaluation:
  Evaluation is applied to expressions. If the expression is a function it
evaluates to itself. If the expression is an application its left hand side is
evaluated, its right hand side is exaluated and then the function on the left
is appled with the function on the right as its argument.
  The result is the result of the application.

Application:
  When as a function is appled it starts a substution on its body, replacing
instances of its header parameter with the argument. The result is the body of
the function after substution.

Substution: [ _ / _ ]
  Substution replaces a variable with an element. When writing out the left
hand side, the element or the substution value, replaces the right hand side,
the variable or the substution target. Substution can be used on any element.
  If substution is used on a function the result is the original function if
the substution target is equal to the function's header variable. Otherwise,
the substution is applied to the function body.
  If substution is used on a variable the result is the original variable if
it is not equal to the substution target, if they are equal the result is the
substution value.
  If substution is used on an application it is used on the left and right
hand sides of the application.

====Other stuff to follow:
  It should be noted that the above is just the minimum to get the interprater
running. Many other things can be added.