LambdaAPI2 design

LambdaAPI2 is another java-written implementation of pure lambda-calculus. Its aim is to support applications of pure lambda-calculus. LambdaAPI2 is based on constructs described in Compiling the Lambda-calculus into Interaction Combinators. For short, we will refer to that document as the LambdaCompiling document. The purpose of the present document is to explain how LambdaAPI2 represents the lambda-terms and realizes their reductions.

This document relates to version 1.0 of the LambdaAPI2 software.

Lambda-term

Differently from LambdaAPI, LambdaAPI2 makes use of the usual definition (T ::= V|λV.T|TT) of lambda-terms. With LambdaAPI2, a lambda-term is either:

Each variable instance is unique. It is either free or bound to an abstraction, which contains this variable instance.

Access to lambda-terms is read-only. it is done through the java interfaces: Term, Variable, Abstraction, Application of the org/xmloperator/lambda2/term/model package.

Terms are instantiated using the VariableImpl class constructor and the buildAbstraction(...) and buildApplication(...) factory methods of the Term interface.

Term reducing is done through the TermReducer interface. It is not proposed a direct implementation of this interface but an indirect one using a combinators-based interaction net (interaction nets are known to be good engines for the lambda-calculus because their sharing characteristics).

Lambda-net

Lambda-nets are interaction nets that realize such a mapping with lambda-terms:

Lambda-nets are made of cells (with ports), free ports and connections. By free port, we don't mean a port (of a cell) that is not connected but a port that belongs to no cell. We use free ports for closing the net, by connecting every port.

Free ports support the interaction net. There is a body support and zero or more free variable support(s). As an example, the simplest lambda-net, the wire lambda-net, is made of a body support connected to a free variable support. The entire lambda-net must be accessible through its body support. Disjoint parts of the net are garbaged.

The port, cell and lambda-net entities are represented by the java interfaces Port, Cell and LambdaNet of the org/xmloperator/lambda2/net/model package and their implementations PortImpl, CellImpl, LambdaNetImpl of the org/xmloperator/lambda2/net/impl package.

Nets are instantiated using the LambdaNetImpl class constructor and the buildAbstraction(...) and buildApplication(...) factory methods of the LambdaNet interface. The only difference with terms is replacing variable instances by free ports. The buildAbstraction(...) methods implements not only the Abstraction construct of LambdaCompiling but also the Eraser one and the Copy one.

From term to net

A lambda-term is translated into an interaction net for reducing.

The used interaction system is composed of the three combinators of Lafont (eraser, duplicator, constructor) plus an abstractor and an applicator, which behave as multiplexors. Interactions rules for the combinators of Lafont are recalled here ("e" for eraser, "d" for duplicator, "c" for constructor):

Combinators interaction rules

The abstractor (symbol "a") and the applicator (symbol "p") have an arity equal to five and interacts together by annihilation. Each one is erased by interacting with an eraser or duplicated by interacting with a duplicator. None interacts with a constructor neither with itself. Annihilation is shown here:

Abstractor-applicator annihilation

Specialized entities implement cells depending on their symbols:

The lambda-net is built at the image of the lambda-term it represents.

From net to term

After some reduction steps, we desire to read back the lambda-term a lambda-net represents. But this operation is not trivial because the lambda-net has no more the structure of a just built lambda-net. It needs to be decoded.

For decoding purpose, the interaction system is completed with an infinite set of indexed symbols, called decoders. A decoder (symbol "x") may have any arity and any index. The index represents a variable in the lambda-term. A decoder interacts only with the applicator, the duplicator or the eraser, as shown here:

Decoder interaction rules

As an example, the net build from the lambda-term "xu", where the term "u" doesn't contain the variable "x", is decoded in the following way:

Application decoding

The process of reading back a closed (i.e. without free variable) term in normal form is the following:

Optimizations

Optimizations occur at the term level, at the cell level and at the interaction level.

Optimizations at the term level:

Optimization at the cell level:

Optimization at the interaction level:

Nothing special is made about garbage collection.


Last update: 2005-12-08 Copyright (c) 2005 The_xmloperator_project