(**********************************************************)
(* SUBSEXPL *)
(* Step by step simulation of the reduction in explicit *)
(* substitution calculi: suspension calculus, lambda s_e *)
(* calculus, lambda sigma calculus and a version of the *)
(* suspension calculus that combines beta contractions *)
(* *)
(* Group of Theory of Computation, *)
(* Universidade de Brasilia - Brasil *)
(* ULTRA group, *)
(* Heriot-Watt University - UK *)
(* Authors: Flavio L. C. de Moura, Mauricio Ayala-Rincon *)
(* and F. Kamareddine. *)
(* *)
(* Permission to copy and reuse this file mantaining its *)
(* procedence indicated above *)
(**********************************************************)
SUBSEXPL is a step by step simulation of reductions in the lambda calculus and in the three explicit substitution calculi:
0. lambda calculus
1. lambda sigma calculus
2. lambda s_e
3. suspension calculus
4. suspension calculus combining beta contractions
Contents:
README this file
Examples this file contains some examples which includes Church numerals, arithmetic operators, booleans, if-then-else, iteration, recursion, etc.
Makefile the makefile
guillaume script for automatic generation of the counter-example of Guillaume
guillaume-README description on how to simulate the counter-example of Guillaume
mellies script for automatic generation of the counter-example of Mellies
mellies-README description on how to simulate the counter-example of Mellies
subsexpl.ml main file
setypes.ml description of types
setypes.mli description of types
seredsus.ml one-step reduction for the suspension
seredsuscomb.ml one-step reduction for the suspension combining
seredls.ml one-step reduction for the lambda sigma
seredlse.ml one-step reduction for the lambda s_e
sematchsus.ml search for redices in the suspension
sematchsuscomb.ml search for redices in the suspension combining
sematchls.ml search for redices in the lambda sigma
sematchlse.ml search for redices in the lambda s_e
selexersus.ml lexer for the suspension
selexersuscomb.ml lexer for the suspension combining
selexerls.ml lexer for the lambda sigma
selexerlse.ml lexer for the lambda s_e
sepure.ml function used to simulate the reductions in the pure lambda-calculus
pure.ml the main loop for the pure lambda-calculus
sigma.ml the main loop for the lambda sigma calculus
lambdase.ml the main loop for the lambda s_e calculus
susp.ml the main loop for the suspension calculus
suspcomb.ml the main loop for the suspension combining calculus
common.ml contains some common functions used by all calculi.
input.ml common input functions (like functions that ask for rule number, position, etc)
output.ml common output functions (like functions that generate the menu)
subsexpl.bin executable in GNU/linux platforms
ledit-1.11 directory with ledit source
doc directory containing html documentation of the modules
adding-a-new-calculus step by step tutorial for adding a new calculus into SUBSEXPL
tutorial.ps (tutorial.pdf) a SUBSEXPL tutorial
Installation instructions:
Either you can just run the executable file, named subsexpl.bin, in your machine or compile the system from the source. Both options are easy:
1. I want just to run SUBSEXPL in my GNU/linux without compiling it:
In this case just download the binary file named subsexpl???.bin, where ??? should be replaced by x86 if you have a PC like machine or ppc if you have a macintosh. Type './subsexpl???.bin' in a terminal. Optionally, you can also download the file ledit.out and type './ledit.out ./subsexpl.bin' to be able to use the ledit facilities.
2. I want to compile SUBSEXPL into my machine:
The following instructions work for both versions with and without the x-symbol package. Download the source code file, named subsexplcomb.tar.gz or subsxsymbol.tar.gz. Extract this file by typing "tar zxpvf subsexpl.tar.gz" in a terminal. It will create the directory subsexpl. Go to this directory typing 'cd subsexpl' and then type "make" (or "make opt") and, if there is no compilation error, you will get two executable files at the end: subsexpl.bin (or subsexpl.opt) and ledit.out.
3. Using subsexpl:
First check if the file subsexpl.bin has execution permition, and if necessary type "chmod u+x subsexpl.bin".
To start subsexpl type "./subsexpl.bin".
If you would like to use subsexpl with the advantages of ledit, type "./ledit.out ./subsexpl.bin".
Reductions can be saved in files according to the following structure:
- the first line of the file should have the number of the calculus to be used. The available options are: 0 for the pure lambda calculus, 1 for the lambda-sigma calculus, 2 for the lambda s_e calculus and 3 for the suspension calculus.
- the second line of the file must contain the expression to be reduced. For instance, A(L(A(L(2),3)),3).
- the following lines correspond to the number of the rule to be applied and the position in the term to apply the selected rule. The position i.j.k should be typed as ijk. See the initial screen of each calculi to see the available rules.
As an example, suppose that you wrote a file named my_reduction with the following contents:
0
A(L(A(L(2),3)),A(L(A(2,1)),5))
1
11
2
21
To simulate this reduction in SUBSEXPL type:
./ledit.out ./subsexpl.bin my_reduction
This command will load the file my_reduction and perform the rule 1 (which corresponds to a beta-reduction) at position 11, and then perform the rule 2 (which corresponds to an eta-reduction) at position 21. After that you will get the following screen:
Expression: A(L(1),A(1,5))
1. Beta: 0
2. Eta:
3. Leftmost/outermost normalisation.
4. Rightmost/innermost normalisation.
5. Back one step.
6. See history.
7. Latex output.
8. Save current reduction.
9. Restart current reduction.
10. Restart SUBSEXPL.
11. Quit.
Give the number:
This screen shows the current expression and all the available options.
For a more detailed description see tutorial.ps (tutorial.pdf).