UPDATE: There is now a page dedicated to chemlambda v2.
The mol file format for a chemlambda molecule is a list of lines. Each line represents a graphical element, like described at the chemlambda project index page.
The moves, or graph rewrites, are visualised at the moves page.
The expression of the moves in mol format can be inferred from the main script, but perhaps this is tedious, therefore I shall give them here directly.
The graphical elements are L, A, FI, FO, FOE, Arow, T, FRIN, FROUT, each with a certain number of ports, as explained in the mentioned index page. Each port has two types:
- one can be “in” or “out”
- the other can be “middle”, “left” or “right”
and there is a convention of writing the ports of any graphical element in a given order.
Here I shall write a graphical element in the following form. Instead of the line “L a b c” from the mol file I shall write “L[a,b,c]”, and the same for all other graphical elements. Then the mol file will be seen as a commutative and associative product of the graphical elements.
This goes back to the initial proposal by Louis Kauffman, who tried to use the formal reduction from Mathematica for the graphic lambda calculus.
Now, we can improve the notation L[a,b,c] by thinking about a, b, c as indices of a tensor, of course. This is reasonable because in any mol file which represents a chemlambda molecule, any port variable appears at most twice, so it is like a summing variable.
Let’s do this by writing
in order to emphasize that “a” has type “in” and “b”, “c” have type out, but otherwise preserving the order a,b,c in the notation (this order allows to infer, from the symbol “L” of the graphical element, they other types of the ports, namely for the L element “a” has also type “middle”, “b” has type “left” and “c” has type “right”).
Same for all other elements.
Here are the moves, then, with the convention that “U=V” means “transform U into V”.
COMB. Denote by any graphical element with an out port “a”, then
L-A (i.e. the BETA move).
FI-FOE(i.e. the FAN-IN move).
L-FO, L-FOE (aka DIST-L).
and the same for L-FOE, where the left hand side … is replaced by and the rest stays the same.
A-FO, A-FOE (aka DIST-A).
and the same for A-FOE, where the left hand side … is replaced by and the rest stays the same.
FI-FO (aka DIST-FI).
FO-FOE (aka DIST-FO).
The question, of course, is: if we see the moves as equalities and the graphical elements as tensors in a vector space, then how many solutions exist for the moves equations (perhaps eliminating the PRUNING moves, or by seeing as an element of the vector space)?