Playing with LambdaAPI

LambdaAPI is a java-written implementation of lambda-calculus. Its aim is to support applications of lambda-calculus. The purpose of the present document is to explain how to use the LambdaAPI software. You are invited to experiment with it. You are of course supposed to have some notion of what is called lambda-calculus.

This document relates to version 1.0 of the LambdaAPI software.

• Installation
• Various tests
• Term serialization
• Beta reduction
• Parallelized beta-reductions
• Some settings

Installation

The LambdaAPI software is provided in source form exclusively. Experimenting with it consists in compiling, running, and editing it repeatedly. Then it's easier to use an IDE and you should use one. For its development, we have used the Eclipse Platform.

In order to install the software with Eclipse you just have to:

1. create a new Java project (File / New / Project... / Java),
2. give it a name,
3. copy the provided source directory content into the project source directory,
4. refresh the project hierarchy (File / Refresh).

The software uses only the JRE System Library (jdk 1.4 or later).

For running (Run / Run...), you have to specify the main class: org.xmloperator.lambda.MainTest. After running, you should see on the Console view something like:

All is OK, during 361 ms.

Various tests

You have passed the full validation test. The console message concludes All is OK and gives a time delay. This delay will of course depend on the characteristics of your machine and the type of the java virtual machine. In order to obtain more information on this validation test, you can (temporarily) change the value of the IS_VERBOSE parameter in the MainTest class. Proceed as follows:

1. Open an editing view of the MainTest class.
2. Find the line that ends with: boolean IS_VERBOSE = false;
3. Replace false by true.
4. Save MainTest.
5. Rerun MainTest.

On the console view, you obtain a list of test messages and the usual conclusion All is OK. Each test is usually concluded by one message line, starting with the name of the concerned class.

The full validation test is composed of several package validation tests. Each package validation test is composed of zero or more class validation test(s). Each of these classes and packages contains a Test class, with a main method. This means that you can decide to run just this class or this package. If so, simply specify the Test class into the running dialog.

The next sections focus on features of the software. You will be proposed to change parameter values (in the same way as for the IS_VERBOSE parameter). You can also add your own tests. Run either the MainTest class or a more specific Test class. Each Test class has its own IS_VERBOSE parameter that you can set to true.

Term serialization

LambdaAPI manipulates generalized nameless lambda-terms. It defines an object model with several possible syntactic forms (i.e., serializations). Two serializers are provided: the prefixed one and the usual one. The following table displays some common terms, as obtained with these serializers.

As you can see, the prefixed form is specified by the presence of the character c before each application. Thus, parentheses are useless.

Note that the terms F, FST, SND, V and TETA are represented as generalized terms, since they include end-of-scopes that contain an abstraction or an application. This, of course, doesn't appear in the usual form without end-of-scope. The operation that transforms a generalized term into a normalized term is called scope extrusion.

Beta reduction

This section is about beta-reduction, one redex at a time. This beta-reduction is implemented by the TreeBetaUtils class but our current test is implemented by the ChurchNumerals class. Open the org.xmloperator.lambda.tree.generate.ChurchNumerals class, set the TRACE parameter to true and run. You obtain a sequence of normalization reports. We reproduce here the report concerning the application of the Church representation of 2 on itself:

<1>
caacevcevvaacevcevv
-+---^--^-*********
acaacevcevvcaacevcevvv
======================
<2>
acaacevcevvcaacevcevvv
 -+---^--^-***********
aaccaacevcevvevccaacevcevvevv
 ============================
<3>
aaccaacevcevvevccaacevcevvevv
   -+---^--^-**              
aacaceevceevvccaacevcevvevv
   ==========              
<4>
aacaceevceevvccaacevcevvevv
  -+-^---^--^**************
aacevcevccaacevcevvevv
  ====================
<5>
aacevcevccaacevcevvevv
         -+---^--^-** 
aacevcevcaceevceevvv
         ========== 
<6>
aacevcevcaceevceevvv
        -+-^---^--^*
aacevcevcevcevv
        =======
ChurchNumerals OK (2 2)[10] == 4/4 using 6 steps.

This is done using the prefixed serializer. If you prefer the usual form, then change the value of the SERIALIZER_TYPE parameter in the MainTest class, from Prefixed to Usual, and rerun. Here is the result:

<1>
(\xy.x(xy))(\xy.x(xy))
--+--^-^---***********
\x.(\yz.y(yz))((\yz.y(yz))x)
============================
<2>
\x.(\yz.y(yz))((\yz.y(yz))x)
   --+--^-^---**************
\xy.(\zu.z(zu))x((\zu.z(zu))xy)
  =============================
<3>
\xy.(\zu.z(zu))x((\zu.z(zu))xy)
    --+--^-^---*               
\xy.(\z.x(xz))((\zu.z(zu))xy)
     ========                
<4>
\xy.(\z.x(xz))((\zu.z(zu))xy)
    --+----^--***************
\xy.x(x((\zu.z(zu))xy))
    ===================
<5>
\xy.x(x((\zu.z(zu))xy))
        --+--^-^---*   
\xy.x(x((\z.x(xz))y))
         ========    
<6>
\xy.x(x((\z.x(xz))y))
        --+----^--*  
\xy.x(x(x(xy)))
        =====  
ChurchNumerals OK (2 2)[10] == 4/4 using 6 steps.

For each beta-reduction, you can see the term represented before and after the reduction. The rewritten part is underlined each time. Redex underlining is done using the following characters:

Parallelized beta reductions

Beta reductions can be parallelized by translating the lambda term to an interaction net and operating on it (see From Lambdascope to LambdaAPI). The parallelized beta reductions are implemented by the Reducer class. To try it, set the TRACE parameter of this org.xmloperator.lambda.translate.Reducer class to true and run. This produces, for the data used in the previous section, the following output:

<1>: 2 binder(2 abs., 4 del.), 2 free abs.
caacevcevvaacevcevv
-+---^--^-*********
<2>: 1 binder(2 abs., 4 del.), 3 free abs.
acaacevcevvcaacevcevvv
 -+---^--^-***********
<3>: 1 binder(2 abs., 4 del.), 2 free abs.
aaccaacevcevvevccaacevcevvevv
   -+---^--^-**              
                -+---^--^-** 
<4>: 1 binder(3 abs., 6 del.), 1 free abs.
aacaceevceevvcaceevceevvv
  -+-^---^--^************
<5>: 1 binder(2 abs., 6 del.), 1 free abs.
aacevcevcacevcevvv
        -+-^--^-^*
aacevcevcevcevv
Reducer OK (2 2) -> 4 using 5 step(s).

As you can see, the third step reduces two redexes at a time.

But the gain of only one step does not warrant parallelization. In order to compare the efficiencies of the two algorithms, we need to use a more complex lambda-term. Consider the term (c4 c2 c2 I I), where ck is the Church representation of the numeral k and I the identity. In order to evaluate the time required for reducing this term to its normal form using the two algorithms, set in the ChurchNumerals class and in the Reducer class the IS_VERBOSE parameter to true and the N_VALUE_WITHIN_TERM_CN_C2_C2_I_I parameter to 4. Then run. This produces (after some time) the following output:

ChurchNumerals (4 2 2 I I) : 249552 steps in 37093 ms
Reducer (4 2 2 I I) : [26/1211] using 10 ms

In this example, the parallelization is clearly justified; [26/1211] means: 26 beta interactions for a total of 1211 interactions.

Some settings

Scope binding

Scope binding is an optimization technique that avoids scope extrusion on closed terms. This technique is used by default by LambdaAPI, but may be invalidated. To repeat the last test without scope binding, set to false the SCOPE_BINDING parameter in the MainTest class and run. The total interaction count increases from 1211 to 1301.

Garbaging or reusing

By default, LambdaAPI reuses objects that are intensively instantiated, such as the elements of an interaction net. This technique has advantages:

• The required memory space is reduced to the minimum.
• This implementation could be used by code with time constraint in a real time system.

But there are drawbacks:

• The management of object reusing is (slightly) more time-consuming than what can be done by modern garbage collectors.
• Returning systematically unused objects to their factory in an application program is a fastidious task.

If you don't want to reuse objects, then set the REUSE parameter to false in the MainTest class.