(**********************************************************)
(* 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 download 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. Start the Emacs editor and a shell inside
the Emacs window by typing "M-x shell". Now start the x-symbol mode by
typing "M-x x-symbol-mode" in the Emacs window. The mini-buffer will
ask you about the "Token Language for X-Symbol mode:". Answer with
"TeX macro". To start SUBSEXPL type './subsexpl???.bin' in this Emacs
window.
2. I want to compile SUBSEXPL into my machine:
Download the source code file, named subsxsymbol.tar.gz. Extract this
file by typing "tar zxpvf subsxsymbol.tar.gz" in a terminal. It will
create the directory subsexpl. Go to this directory typing 'cd
subsexpl' and then type "make" and, if there is no compilation error,
you will get a binary file called subsexpl.bin. Now follow the step 1
above replacing subsexpl???.bin for 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
3 for the suspension calculus and
4 for the combining 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:
./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).