For being able to build a chemical concrete machine (see the posts A chemical concrete machine for lambda calculus and Why build a chemical concrete machine, and how?) we have to prove that universal computation can be attained with only local moves in graphic lambda calculus. Or, the lambda calculus sector of the graphic lambda calculus, which gives universality to graphic lambda calculus, uses the global FAN-OUT move (see theorem 3.1 (d) arXiv:1305.5786 [cs.LO]. Similarly, we see in proposition 3.2 (d), which describes the way combinatory logic appears in graphic lambda calculus, that again global FAN-OUT is used.
There are reasons to dislike global moves in relation to B-type neural networks (see the last post Pair of synapses, one controlling the other (B-type NN part III) ). Similar concerns can be found in the series of posts which has as the most recent one Dictionary from emergent algebra to graphic lambda calculus (III) .
In this first post I shall introduce a local FAN-IN move and two distributivity moves and I shall prove that they eliminate the need for using global FAN-OUT in combinatory logic. In the next post I shall prove that we can eliminate two other moves (so that the total number of moves of graphic lambda calculus stays the same as before) and moreover we can recover from distributivity and local FAN-OUT moves the missing oriented Reidemeister moves from the -TANGLE sector.
Definition. The local FAN-IN move is described in the next figure and it can be applied for any .
- as you see, in the move appears a dilation gate, what can this has to do with combinatory logic? As I explained previously, the properties of the gates are coming through the moves they are involved in, and not from their name. I could have introduced a new gate, with two inputs and one output, call this new gate “fan-in gate” and use it in the FAN-IN move. However, wait until the next post to see that there are other advantages, besides the economy of gates available, in using a dilation gate as a fan-in.
- the FAN-IN move resembles to the packing arrows trick which is used extensively in the neural networks posts. This suggests to use as a fan-in gate
the green triangle gate and as fan-out gate the red triangle gate. This would eliminate the gate from the formalism, but is not clear to me how this replacement would interfere with the rest of the moves.
- the FAN-IN move resembles with the dual of the graphic beta move, but is not the same (recall that until now I have not accepted the dual of the graphic beta move in the list of the moves of graphic lambda calculus, although there are strong reasons to do so):
- in the Dictionary from emergent algebra to graphic lambda calculus (II) I introduced a “mystery move”
which is needed in the emergent algebra sector in order to make the dictionary to work (and related as well to the goal of non using global FAN-OUT in that sector). This latter move is in fact a distributivity move (see further), but we are free to choose different moves in different sectors of the graphic lambda calculus,
- I know it is surprising that until now there was nothing about evaluation strategies in graphic lambda calculus, the reason being that because there are no variables then there is noting to evaluate. However, the situation is not so simple, at some point, for example in the chemical concrete machine or for neural networks, some criterion for choosing the order of moves will be needed. But it is an important point to notice that replacing global FAN-OUT (which could be seen as a remnant of having variables and evaluating them) by local FAN-IN has nothing to to with evaluation strategies.
Definition: The distributivity moves (related to the application and lambda abstraction gates) are the following:
- the first distributivity move is straighforward, an application gate is just doubled and two fan-out moves establish the right connections. We see here why the “mystery move” can be seen as a kind of distributivity move,
- the second distributivity move is where we need a fan-in gate (and where we use a dilation gate instead): because of th orientation of the arrows, after we double the lambda abstraction gates, we need to collect two arrows into one!
Combinatory logic terms appear in graphic lambda calculus as trees made by application gates, with leaves one of the combinators S, K, I (seen as graphs in . I want to show the following. [UPDATE: made some corrections.]
Theorem. We can replace the global FAN-OUT move with a sequence of local FAN-IN , DIST, CO-COMM and local pruning moves, every time the global FAN-OUT move is applied to a term made by SKI combinators.
Proof. First, remark that a sequence of DIST moves for the application gate allows to reduce the problem of replacing global FAN-OUT moves for any combinator to the problem of replacing it for S, K, and I. This is because the DIST move for the application gate allows to do the FAN-OUT of trees of application gates:
Now we have to prove that we can perform global FAN-OUT for I , K, S combinators. For the combinator I the proof is the following:
For the combinator K we shall also use a local pruning move:
Finally, the proof for the combinator S is the following:
Now we are going to use 3 DIST moves, followed by the switch of arrows explained in Local FAN-IN eliminates GLOBAL FAN-OUT (II) , which is applied in the dashed green ellipse from the next figure:
And we are done.
UPDATE: At close inspection, it turns out that we don’t need to do switch (macro) moves. Instead, if we go back at the point we were before the last figure, we may use first CO-ASSOC and then perform the three FAN-IN moves .