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.
LambdaAPI proposes a full set of interfaces and associated implementation for representing:
The LambdaAPI software is structured by these lambda-terms and lambda-nets:
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:
\ for lambda, / for end-of-scope and a variable name obtained from the index of the abstraction matching this variable.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.
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.
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.
Building a Term from a lambda-net is realized by the translate method of the FromNetToTerm class.
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.
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.
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 :
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 |