Continues from part (I).
How to simulate a move with a quine. Let’s think.
The starting point is a mol file which describes the graph. Then there is a program which does the reductions. We should see the program (or the specific part of it which does a move) as the enzyme of that move. OK, but a program is something and a mol file is a different thing.
Recall though that chemlambda is Turing universal. That means in particular that for any particular mol file A.mol and any particular program P which reduces mol files there is a chemlambda molecule and a reduction algorithm which simulate how the program reduces the mol file. Kind of a bootstrapping, right?
Yes, but let’s say it again: given A.mol and P there exist B.mol such that P reduces B.mol simulates the computation (P reduces A.mol).
In particular there is a part E.mol of the B.mol file (or more abstractly a subgraph of the molecule B) whose reductions in the “context” B simulate the part of the program P acting on A and doing a reduction.
That part is actually a molecule, just as A, which can be thought as being the enzyme of the move (which is implemented in P).
Then, instead of making a (theoretically possible) algorithm which generates from A.mol and P the file B.mol, etc, instead of that we may do something simpler.
We would like to use a quine as E.mol.
That is because it respects the chemical analogy in the sense that the reduction of E.mol preserves the number of nodes (atoms).
For this we look again at what is a move, and also at what new primitive we need in order to make all this to function.
A move is described by a pair of patterns (i.e. molecules), called LEFT and RIGHT pattern, with the property that there is a pairing between the free ports of the LEFT pattern and the RIGHT pattern.
The move then is implemented by an algorithm which:
- does a pattern matching for the LEFT pattern
- then replaces the LEFT pattern by the RIGHT pattern.
(I should add that not any instance of the LEFT pattern in A.mol is replaced by a RIGHT pattern, because there may be conflicts created by the fact that a node of A.mol appears in two different LEFT patterns, so there is a need for a criterion which decides which move to do. I neglect this, you’ll see later why, but roughly I concentrate on the move, because the criterion (or priority choice) is a different problem.)
Aha! We need the possibility to make pairings of edges, or even better (seen the mol format) we need a way to make pairings of ports.
I shall use the notation a:b for such a pairing. Notice that:
- we see such pairings when we say that x is of type a, i.e x:a (recall that one can see types as pairings between edges of molecules and edges of other molecules which represent types from the Calculus of Constructions)
- the pairing a:A saying that the edge a belongs to the actor A is a pairing (induces a pairing) between the edges of a molecule and the edges of an actor diagram in distrubted GLC
- the pairing a:b, where a is an edge of a molecule and x is an edge of another molecule which represents an emergent algebra term (see the thread on projective conical spaces) says that edge “a” is in place “b”
- the pairing a:b can be the consequence of a copmmunication; non-exclusively one may think of a:b as a consequence of c?(b) | c!(a)
- in conclusion moves are particular pairings coupled with an algorithm for associating a LEFT pattern to a RIGHT pattern, pretty much as typing is a pairing with another algorithm, or places (i.e. emergent algebras and their reductions) is of the same kind; the algorithm which does the pairing is a matter of communication procedure and it can be implemented by process calculi, actor models or whatever you like best.
So, let’s pick a small quineas E.mol, like a 9- or 10-quine which has the property that it has one LEFT pattern for (say) beta move and let’s do the following:
- pair a LEFT pattern from A.mol with the same (pattern matching) from E.mol
- reduce E.mol (bootstrapping) and get E’.mol which is identical to E.mol up to renaming some of the port (i.e.edge) names
- update the pairing (which is akin of the intention of replacement of LEFT pattern by RIGHT pattern)
- let the program in charge of A.mol to rewire (apply the update)
It’s perhaps a too short explanation, will come with details from A to Z next year.
Wish you the best for 2015!