From Lambdascope to LambdaAPI

LambdaAPI is a java-written implementation of lambda-calculus. Its aim is to support applications of lambda-calculus. LambdaAPI is based on constructs described in Lambdascope. Another optimal implementation of the lambda-calculus. The purpose of the present document is to explain how LambdaAPI represents the Lambdascope constructs.

In order to explain the mapping from Lambdascope to LambdaAPI, we chose to follow in this document the section order of the Lambdascope document. We hope that this will help the reader, who is supposed to have read (and understood) the Lambdascope document.

This document relates to version 1.0 of the LambdaAPI software.

1. Introduction

LambdaAPI proposes a full set of interfaces and associated implementation for representing:

The LambdaAPI software is structured by these lambda-terms and lambda-nets:

2. Lambda-calculus

LambdaAPI represents nameless lambda-terms by the interfaces Abstraction, Application, EndOfScope and Leaf, all of which extend the Term interface. They are defined in the package org.xmloperator.lambda.tree.model. This model represents generalized lambda-terms in the sense that an EndOfScope may contain an Abstraction or an Application. There is no explicit binding between a Leaf or an EndOfScope and its matched Abstraction.

Reading and writing lambda-terms, using different notations, is supported by a separate interface, called Serializer and defined in the package org.xmloperator.lambda.tree.serialize. The following Serializer implementations are provided:

The beta-reduction, including the scope extrusion, is realized by the reduce method of the TreeBetaUtils class. The complete extrusion of one EndOfScope is realized by the extrude method of the AlphaUtils class.

The closure of a Term can be verified by using the verifyClosure method of the same AlphaUtils class.

3. From terms to nets

Each symbol of the interaction net is represented by an Operator. The Operators are: the Applicator, the Abstractor, the Delimiter, the Duplicator and the Eraser. An Operator has between one and three Ports. Various methods are proposed for accessing to a Port. For connecting two Ports, one calls the connectTo method on one Port with the other Port as argument. The closure of a net can be verified by calling the verifyClosure method of the NetTraversal class, applied to the root Eraser.

Building an interaction net from a lambda-Term is realized by the translate method of the FromTermToNet class.

4. Interaction net reduction

Triggering off an interaction between two Operators (with connected principal Ports) is realized by calling the interact method of one of the two Operators. A beta-reduction followed by the application of the x-rules is realized by the reduce method of the NetBetaUtils class. A complete reduction, for obtaining the normal form, is realized by the reduceDeeply method. The leftmost redex determination is realized on the read-back tree, described in section 6.2.

5. From nets to terms

Building a Term from a lambda-net is realized by the translate method of the FromNetToTerm class.

6.1. Directed nets

Each Port is directed. At the connection between two Ports, the compatibility of their directions is checked. The direction of a Port is given by its isInput method.

6.2. Tree nets

Reading back trees is based on the Walk type. It represents the level syntactic category of the automaton grammar. A WalkingContext is an object used as a context for traversing the whole read-back tree. It is based on a root Eraser, a body index, a Walk stack and a current Port. Because walking through a zero index Delimiter results in some loss of information, it is necessary to add to the WalkingContext a symmetrical, complementary Walk stack. The WalkingContextTranslater complements the WalkingContext by a root Term in order to translate the walking context in that Term.

8.2. Disconnected vs. connected scopes

The authors of Lambdascope noted that extruding a scope over a term costs an amount of time which is a linear function of the size of this term, and that this extruding could be avoided if the term is closed. From the observation that an abstraction is closed if no end-of-scope matches it, one can reasonably expect an efficiency enhancement from something like a scope binding.

A scope binding, in any form, is easy to realize at the Term-to-Net level: one abstractor is bound to zero or more delimiter(s). The problem is to maintain the scope binding structure together with the interactions. Think about the following scenario :

  1. A delimiter is bound to an abstractor.
  2. The abstractor is duplicated by a duplicator. The delimiter is duplicated by another duplicator, with the same index.
  3. The two duplicators interact. They are annihilated and two independent scope bindings appear.
  4. One of the two delimiters is erased. Then its bound abstractor becomes closed while the other one remains not closed.

There are other scenarios showing that, for maintaining an exact scope binding, it is necessary to introduce a full set of scope operators. These new operators become as numerous as the standard ones and their interactions consume as much time; the benefit is lost. For this reason, LambdaAPI chooses to implement a lazy scope binding, which is sufficient for asserting that some abstractor is closed but not for asserting that an arbitrary abstractor is not closed.

The LambdaAPI lazy scope binding is based on the ScopeBinder, which binds one or more Abstractor(s) to one or more Delimiter(s). It is not time-consuming and allows some global gain in time (about 20%), but only on terms which can be reduced in a few steps because, beyond a certain number of steps, there is no more than one, global, ScopeBinder.

Last update: 2004-09-13 Copyright (c) 2004 The_xmloperator_project