LambdaAPI3 is a java-written implementation of applied lambda-calculus. It makes use of term sharing using a directed acyclic graph (dag). A synthetic presentation of the dag sharing technique is given in Sharing in the Evaluation of lambda Expressions.
This document is related to the version 2.0 of the software. LambdaAPI3 design is exposed through the following sections:
LambdaAPI3 makes use of the usual definition of lambda-terms with constants:
T ::= V | C | λV.T | TT
These four forms of a lambda-term are respectively represented by:
where Variable, Constant, Abstraction and Application are interfaces that specialize the Term interface.
A Variable is created free. It may later be bound to an Abstraction, whose body contains all the references to this Variable.
For example, for instantiating a delta combinator λx.xx
Each Term has a reference count, which shows how many times the Term is referenced.
For the example of the delta combinator λx.xx
In beta reduction, the reductible expression (redex) is an Application whose function is an Abstraction. The result of redex contraction is the Abstraction body in which each reference to the Abstraction bound Variable is replaced by a reference to the Application argument:
(λx.M[x]) N -> M[x -> N]
This operation focuses issues. List them:
The operation of beta reduction implies that the Abstraction body is detached from the Abstraction.
At the end of operation, the redex (Application + Abstraction + bound Variable) is unused and may be recycled after separating its components.
Term recycling issue is the object of the Garbage collection section.
There are two possibilities. Either the redex belongs to a Term (which references it once or more), either the redex is the Term to contract and it is not referenced at all.
If the redex is not referenced then it is simply replaced by its contraction. Also we discuss here the case where the redex belongs to a whole Term (not referenced) and is referenced once or more.
A first issue is to locate the redex reference(s) within the whole Term. A second one is to make the substitution.
We know the number of reference to the redex but not what Term references it. Also we need to perform a scan of the whole Term in order to locate redex reference(s). An optimization is to stop scanning as soon as the reference count is obtained.
Once located the references to the redex, we can first break each redex reference by replacing it by a hole, then contract the redex and finally replace each hole by a reference to the contraction.
In the previous section we were concerned about redex referencing (and replacement). In this one we care about the Abstraction part of the redex, which is, remember it, destroyed at the end of operation.
At the beginning of the operation, the redex Abstraction is referenced by the redex Application and, optionally, elsewhere within the whole Term, once or more. If the Abstraction is referenced elsewhere, it cannot be touched, it must be duplicated.
Duplication is a major operation, which needs to be optimized. A full optimization is to locate all the free Abstractions. This option requires more calculus than the duplication itself and has therefore been abandoned. Applied optimization has been to not duplicate the Abstractions that are known as closed. The whole Abstraction is, of course, duplicated, closed or not.
Bound Variable replacement requires a scan of the Abstraction body. An optimization is also here to stop scanning when the number of references is obtained. Unlike redex, the substitution of the Variable reference by the argument reference requires only one pass.
If the bound Variable is not referenced (within the Abstraction body) then the redex argument will be unused at the end of the operation. In that event the argument may be recycled after separating its contents.
Term recycling issue is the object of the Garbage collection section.
In delta reduction, the redex is an Application whose function is a Constant. The result of redex contraction depends on the Constant and its argument:
C N -> M
The Constant C represents a function of one or more arguments. When this function has several arguments, the contraction of the redex using all but the last argument consists in storing the argument within the Constant object.
The Constant function may be evaluated and the redex contracted once all the arguments stored. It may requires also (depending on the Constant) that the arguments are in their normal form.
Beta/delta reduction is usually invoked through the calculus of a normal form. LambdaAPI3 offers various Term.normalForm(...) methods designed for:
Normal form evaluation uses normal order of redex contraction ie the leftermost outermost redex is systematically selected.
In order to avoid any program stack overflow, recursion is used in no method that concerns beta reduction or normal form evaluation.
Lambda calculus is a great consumer object instances but the types of these objects are few. Also a specialized garbage collector is a serious option, which we adopt here.
LambdaAPI3 adopts the full garbage collection option: all produced Term has to be explicitly collected (once become useless). This is accomplished by calling the ReductionUtils.breakTermDeeply(Term) method. A tool is provided for verifying the full garbage collection of Terms.
LambdaAPI3 is supplied with a set of accessories. List them with their reference methods or classes:
| Last update: 2013-07-28 | Copyright (c) 2013 The_xmloperator_project |