UPDATE(2020): All you need to read is this.
A mol file is any finite list of items of the following kind, which
satisfies conditions written further. Take a countable collection of
variables, denote them by a, b, c, … . There is a list of symbols:
L, A, FI, FO, FOE, Arrow, T, FRIN, FROUT. A mol file is a list made of
lines of the form:
– L a b c (called abstraction)
– A a b c (called application)
– FI a b c (called fanin)
– FO a b c (called fanout)
– FOE a b c (called other fanout)
– Arrow a b (called arrow)
– T a (called terminal)
– FRIN a (called free in)
– FROUT a (called free out)
The variables which appear in a mol file are called port names.
Condition 1: any port name appears exactly twice
Depending on the symbol (L, A, FI, FO, FOE, Arrow, T, FRIN, FROUT),
every port name has two types, the first from the list (left, right,
middle), the second from the list (in,out). The convention is to write
this pair of types as middle.in, or left.out, for example.
Further I repeat the list of possible lines in a mol file, but I shall
replace a, b, c, … by their types:
– L middle.in left.out right.out
– A left.in right.in middle.out
– FI left.in right.in middle.out
– FO middle.in left.out right.out
– FOE middle.in left.out right.out
– Arrow middle.in middle.out
– T middle.in
– FRIN middle.out
– FROUT middle.in
Condition 2: each port name (which appears in exactly two places
according to condition 1) appears in a place with the type *.in and in
the other place with the type *.out
Two mol files define the same molecule up to the following:
– there is a renaming of port names from one mol file to the other
– any permutation of the lines in a mol file gives an equivalent mol file
(The reason is that a mol file is a notation for an oriented graph
with trivalent or 2-valent or univalent nodes, made of locally planar
trivalent nodes L, A, FI, FO, FOE , 2valent node Arrow and 1valent
nodes T, FRIN, FROUT. In this notation the port names come from an
arbitrary naming of the arrows, then the mol file is a list of nodes,
in arbitrary order, along with port names coming from the names of
arrows.)
(In the visualisations these graphs-molecules are turned into
undirected graphs, made of nodes of of various radii and colours. To
any line from a mol file, thus to any node from the oriented graph,
correspond up to 4 nodes in the graphs from the visualisations.
Indeed, the symbols L, A, FI, FO, appear as nodes or radius
main_const and colour red_col or green_col, FOE, T and Arrow have different colours. Their respective ports
appear as nodes of colour in_col or out_col, for the types “in” or
“out”, and radius “left”, “right”, “middle” for the corresponding
types.FRIN has the colour in_col, FROUT has the colour out_col)
The chemlambda rewrites are of the following form: replace a left
pattern (LT) consisting of 2 lines from a mol file, by a right pattern
(RT) which may consist of one, two, three or four lines. This is
written as LT – – > RT
The rewrites are: (with the understanding that port names 1, 2, … c,
from LT represent port names which exist in the mol file before the
rewrite and j, k, … from RT but not appearing in LT represent new
port names)
http://chorasimilarity.github.io/chemlambda-gui/dynamic/moves.html
– A-L (or beta):
L 1 2 c , A c 4 3 – – > Arrow 1 3 , Arrow 4 2
– FI-FOE (or fan-in):
FI 1 4 c , FOE c 2 3 – – > Arrow 1 3 , Arrow 4 2
– FO-FOE :
FO 1 2 c , FOE c 3 4 – – > FI j i 2 , FO k i 3 , FO l j 4 , FOE 1 k l
– FI-FO:
FI 1 4 c , FO c 2 3 – – > FO 1 i j , FI i k 2 , FI j l 3 , FO 4 k l
– L-FOE:
L 1 2 c , FOE c 3 4 – – > FI j i 2, L k i 3 , L l j 4 , FOE 1 k l
– L-FO:
L 1 2 c , FO c 3 4 – – > FI j i 2 , L k i 3 , L l j 4 , FOE 1 k l
– A-FOE:
A 1 4 c , FOE c 2 3 – – > FOE 1 i j , A i k 2 , A j l 3 , FOE 4 k l
– A-FO:
A 1 4 c , FO c 2 3 – – > FOE 1 i j , A i k 2 , A j l 3 , FOE 4 k l
– A-T: A 1 2 3 , T 3 – – > T 1 , T 2
– FI-T: FI 1 2 3 , T 3 – – > T 1 , T 2
– L-T: L 1 2 3 , T 3 – – > T 1 , T c , FRIN c
– FO2-T: FO 1 2 3 , T 2 – – > Arrow 1 3
– FOE2-T: FOE 1 2 3 , T 2 – – > Arrow 1 3
– FO3-T: FO 1 2 3 , T 3 – – > Arrow 1 2
– FOE3-T: FOE 1 2 3 , T 3 – – > Arrow 1 2
– COMB: any node M (excepting Arrow) any out
port c , Arrow c d – – > M d
Each of these rewrites are seen as a chemical interaction of the mol
file (molecule) with an invisible enzyme, which rewrites the LT into
RT.
(Actually one can group the rewrites into families, so there are
needed enzymes for (A-L, FI-FOE), for (FO-FOE, L-FOE, L-FO, A-FOE,
A-FO, FI-FOE, FI-FO) for (A-T, FI-T, L-T) and for (FO2-T, FO3-T,
FOE2-T, FOE3-T). COMB rewrites,a swell as the Arrow elements, have a
less clear interpretation chemically and there may be not needed, or
even eliminated, see further how they appear in the reduction
algorithm.)
The algorithm (called “stupid”) of application of the rewrites has
two variants: deterministic and random. Further I explain both. For
the random version there are needed some weights, denoted by wei_*
where * is the name of the rewrite.
(The algorithms actually used in the demos have a supplementary family
of weights, which are used in relation with the count of the enzymes
used, I’ll pass this.)
The algorithm takes as input a mol file. Then there is a cycle which
repeats (indefinitely, or a prescribed number of times specified at
the beginning of the computation, or it stops if there are no rewrites
possible).
Then it marks all lines of the mol file as unblocked.
Then it creates an empty file of replacement proposals.
Then the cycle is:
1- identify all LT which do not contain blocked lines for the move
FO-FOE and mark the lines from the identified LT as “blocked”. Propose
to replace the LT’s by RT’s. In the random version flip a coin with
weight wei-FOFOE for each instance of the LT identified and according
to the coin drop block or ignore the instance.
2- identify all LT which do not contain blocked lines for the moves
(L-FOE, L-FO, A-FOE, A-FO, FI-FOE, FI-FO) and mark the lines from
these LT’s as “blocked” and propose to replace these by the respective
RTs. In the random version flip a coin with the respective weight
before deciding to block and replacement proposals.
3 – identify all LT which do not contain blocked lines for the moves
(A-L, FI-FOE) and mark the lines from these LT’s as “blocked” and
propose to replace these by the respective RTs. In the random version
flip a coin with the respective weight before deciding to block and
replacement proposals.
4 – identify all LT which do not contain blocked lines for the moves
(A-T, FI-T, L-T) and for (FO2-T, FO3-T, FOE2-T, FOE3-T) and mark the
lines from these LT’s as “blocked” and propose to replace these by the
respective RTs. In the random version flip a coin with the respective
weight before deciding to block and replacement proposals.
5- erase all LT which have been blocked and replace them by the
proposals. Empty the proposals file.
6- the COMB cycle: repeat the application of COMB moves, in the same
style (blocks and proposals and updates) until no COMB move is
possible.
7- mark all lines as unblocked
The main cycle ends here.
The algorithm ends if (the number of cycles is attained, or there are
no rewrites performed in the last cycle, in the deterministic version,
or there were no rewrites in the last N cycles, with N predetermined,
in the random version).
___________________________________