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
- 2. Lambda-calculus
- 3. From terms to nets
- 4. Interaction net reduction
- 5. From nets to terms
- 6.1. Directed nets
- 6.2. Tree nets
- 8.2. Disconnected vs. connected scopes

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

- nameless lambda-terms and their associated operations, including serialization and beta-reduction,
- optimal lambda-nets and their transformations from and to lambda terms.

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

- The packages with names like
`org.xmloperator.lambda.tree.*`are exclusively concerned with lambda-terms. - The packages with names like
`org.xmloperator.lambda.net.*`are exclusively concerned with lambda-nets. - The package org.xmloperator.lambda.translate is concerned with transformations between lambda-terms and lambda-nets and optimal reduction from lambda-term to lambda-term.

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:

- UsualSerializer provides input/output using the usual notation with
`\`

for lambda,`/`

for end-of-scope and a variable name obtained from the index of the abstraction matching this variable. - PrefixedSerializer notation is similar to the De Bruijn notation, except that each application is prefixed by a fixed symbol. The advantage of this notation is to avoid the need of parentheses.

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 `Port`s, 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 `Operator`s (with connected principal `Port`s) is realized by calling the interact method of one of the two `Operator`s. 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 `Port`s, 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 :

- A delimiter is bound to an abstractor.
- The abstractor is duplicated by a duplicator. The delimiter is duplicated by another duplicator, with the same index.
- The two duplicators interact. They are annihilated and two independent scope bindings appear.
- 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 |