Tag Archives: tutorial

Visual tutorial for “the soup”

I started here a visual tutorial for chemlambda and it’s gui in the making. I call it a tutorial for the “soup” because it is about a soup of molecules. A living soup.

Hope that in  the  recent future will become THE SOUP. The distributed soup. The decentralized living soup.

Bookmark the page because content will be added on a daily basis!


Ancient Turing machine helps Chemical concrete machine

In this post I want to prove that only with arrow molecules and enzyme moves we can generate all we need for the chemical concrete machine, by using the minimal (?) formalism from  Chemical concrete machine, short list of gates and moves . This is done with the help of ideas from the old post   Ancient Turing machines (I): the three Moirai, which   contains a discussion about generating moves for graphic lambda calculus.

In the post Local FAN-IN eliminates GLOBAL FAN-OUT (II) , at the end, I prove a switch move from CO-COMM and FAN-IN moves. In the next figure, I call this move (which is, recall, a “macro move”, made by a succession of three moves) SWITCH.  In the same figure appears a move CREA’. The name is justified by the resemblance with the CREA move proposed in Ancient Turing machines (I): the three Moirai .


Before giving the proof of CREA’, let me remark that from these macro moves, together with the ones selected in the post  Chemical concrete machine, short list of gates and moves , we can recover all the generating moves of the three Moirai described in the ancient Turing machine post. For example, CREA’ , used for a triple of arrows, gives both the  Clotho’s  CREA  original move and the Atropos  GARB move.

Here is the proof of CREA’:


From a bag of arrows at our discretion, this move gives us fan-out gates and termination gates.  Moreover, it is pleasant to see that, as the SWITCH move is a consequence of CO-COMM and FAN-IN, the CREA’  move is a consequence of CO-ASSOC and FAN-IN.

We need the other three trivalent gates, let’s see how we can obtain them (generate them from arrows, by using moves, recall that moves are enzymes, in the world of the chemical concrete machine).

The fan-in gate is generated like this (we already generated termination gates):


The lambda abstraction and application gates can be generated by using the graphic beta move and a SWITCH move.


Now we have all the gates we need and we can proceed to constructing whatever combinator we want from them, mainly by using SWITCH moves. One elegant way for doing this would be to construct zippers first, by using the graphic beta moves, then construct the S,K,I combinators from zippers, as indicated in  Combinators and zippers.

Probably, the real chemical concrete machine will function with terms (molecules) created by some more natural chemistry tricks, but it is pleasant to see that in principle we can also construct what we need, before passing to the “computation” part, only by using arrows and moves.

Chemical concrete machine, short list of gates and moves

Continuing from  Local FAN-IN eliminates GLOBAL FAN-OUT (II)  and   Local FAN-IN eliminates global FAN-OUT (I)  I propose the following list of gates and moves, which are taken from graphic lambda calculus, with the FAN-IN and DIST moves added. (So this could be called the “chemical concrete machine sector”, and it has Turing universality, via the fact that it contains the combinatory logic.)


Principle: each gate is a molecule, each move is an enzyme.


Dictionary:  we need four trivalent gates, which can be distinguished one from another by looking at the number of inputs/outputs and from a choice of colour between red and green. To these add the arrows, loops and the termination gate. The translation from graphic lambda calculus notation to this new coloured notation is the following.


Each of these gates is a molecule.  [Speculations: (1) by looking at DNA backbones, could be the 5′-3′ phosphate-deoxyribose backbone be used as \rightarrow? ]


The moves, translated. Each move is made possible by an enzyme (hence move = enzyme). Here is the list, with the names taken from graphic lambda calculus, by using the dictionary for translation.





  • Elimination of loops:



Implementation needed, but this is out of my competence.  I was thinking that could be possible by using DNA origami techniques, but it might turn out that the schema here is even more close to the structure of DNA. This is an outrageous speculation, but I can’t stop to remark that there are 4 trivalent gates, making two pairs of duality (seen in the graphic beta move and in the FAN-IN move), and this resembles to the A-T, G-C pairing (but it might be a coincidence).

Local FAN-IN eliminates GLOBAL FAN-OUT (II)

As I wrote in   Local FAN-IN eliminates global FAN-OUT (I) , the introduction of the three moves (FAN-IN and the two DIST moves) eliminates global FAN-OUT from the lambda calculus sector of the graphic lambda calculus.  In this post we shall see that we can safely eliminate other two moves, namely R1a, R1b, as well as improving the behaviour of the crossings from the \lambda-TANGLE sector.

The equilibrium is thus established: three new moves instead of the three old moves. And there are some unexpected advantages.



Proof.  (a) Done in the following picture.


The proof of (b) is here:


Finally, here is the proof of (c):



The \lambda-TANGLE sector of the graphic lambda calculus is obtained by using the lambda-crossing macros


In Theorem 6.3   arXiv:1305.5786 [cs.LO]  I proved that all the oriented Reidemeister moves (with the crossings replaced by the respective macros), with the exception of the moves R2c, R2d, R3a and R3h, can be proved by using the graphic beta move and elimination of loops.  We can improve the theorem in the following way.

Theorem.  By using the graphic beta move, elimination of loops, FAN-IN and CO-COMM, we can prove all the 16 oriented Reidemeister moves.

Proof. The missing moves R2c, R2d, R3a and R3h are all equivalent (by using the graphic beta move and elimination of loops, see this question/answer at mathoverflow) with the following switching move, which we can prove with FAN-IN and CO-COMM:


The proof is done.

Local FAN-IN eliminates global FAN-OUT (I)

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.

I want to describe a way to eliminate the global FAN-OUT move from combinatory logic (as appears in graphic lambda calculus via the algorithm described here ).


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 \lambda-TANGLE sector.


Definition. The local FAN-IN move is described in the next figure and it can be applied for any \varepsilon \not = 1.



  • 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 \Upsilon 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):



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 GRAPH.  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 .

Pair of synapses, one controlling the other (B-type NN part III)

In  Teaser (I) and Teaser (II) I discussed about the possibility to construct neural networks with controlled connections, resembling the B-type neural networks of Turing, in the following sense:

  • they are formed by “neurons”, which in Turing’s description are boolean logic gates, and here they are graphs from graphic lambda calculus which correspond to lambda calculus terms. But there’s no real restriction on that, graphic lambda calculus being more general and powerful than untyped lambda calculus, one may consider “neurons” which are outside the lambda calculus sector. The fact is that a “neuron” here should be interpreted as any graph in GRAPH with at least one input but only one output. Later, when we shall speak about the order of performing moves in such neural networks, it will be seen that each “neuron” is a bag containing graphs which are modified (or reduced, as people say) independently one from another. Neurons are packing conventions from a formal viewpoint, but this viewpoint may not be the best one, a better viewpoint would be to see neurons as well as synapses, described further, as real constructs, like in the related project of the chemical concrete machine, In particular, neurons may do other things than computing in the lambda calculus sense (classical computation), they may do some more geometrical or physical or robot-like activities, not usually considered computations.
  • the connections between neurons are controlled in a B-type NN, by TRUE – FALSE control wires or inputs. Turing explains that controls themselves can be realized as constructions with boolean neurons (i.e. in his language B-type NNs are particular cases of his A-type NNs). In Teaser (II)    is explained how the connections between graphic lambda calculus neurons can be constructed by using a 2-zipper and a switch, such that a connection is controlled (by the same TRUE-FALSE mechanism, but this time TRUE and FALSE are literary the graphs of the corresponding terms in lambda calculus) by another connection.

There is an important difference, besides the power of the calculi used (boolean vs. graphic lambda), namely that there is no signal transmitted through the wires  of the network. That is because graphic lambda calculus does not need variable names. I shall come back to this very important point (which is a big advantage for implementing such networks in reality) in a future post, but let me mention two simple facts:

  • an analogy: think about hardware and software, a difference between them is that software may be associated to the pattern of signals which circulates in the hardware. The hardware is the machine inhabited by the software, they are not in the same plane of physical reality, right? Well, in this implementation there is literary no difference between those, exactly because there are no signals (software) transmitted through the hardware.
  • this use of names, software, variable and signals is a pain for those trying to make sense how to implement in reality computing constructs. But, if you think, the need to name that stuff “x” and that other stuff “y”, to make alpha conversions in order to avoid name clashes, or even to describe computations in a linear string of symbols, all this are in no relation with physical reality, they are only cultural constraints of humans (and their artificial constructs). It all has to do with the fact that humans communicate science through writing, and of course, it has to do with the enumeration techniques of the cartesian method , which “is designed as a technique for understanding performed by one mind in isolation, severely handicapped by the bad capacity of communication with other isolated minds”. Molecules in a cell or in a solution do not align in a string according to the experimenter writing habits, from left to right, right to left, or vertical. They just don’t wait for an external  clock  to rhythm their ballet, nor for the experimenter to draw it’s familiar coordinate system. These are all limitations of the method, not of nature.


Further, in this post, I shall use “synapse” instead “connection”.  Let’s see, now that we know we can implement synapses by a TRUE-FALSE mechanism, let’s see if we can do it simpler. Also, if it is possible to make the “synapses control other synapses” concept more symmetric.

Instead of the little magenta triangles used in Teaser I, II posts (which are not the same as the magenta triangles used in the chemical concrete machine post) , I shall use a more clear notation:


The design of a synapse proposed in Teaser (II)  involved two switches and a zipper, justified by the direct translation of TRUE-FALSE lambda calculus terms in the freedom sector of graphic lambda calculus.  Think now that in fact we have there two synapses, one controlling the other. The zipper between them is only a form of binding them together in unambiguous way.

A simplified form of this idea of a pair of synapses is the following:


In the upper part of the figure you see the pair of synapses, taking the a form like  this: ><. There are two synapses there, one is >, which is controlled by the other <.  The connection between the blue 1 and the red 3′ is controlled by the other synapse. In order to see how, let’s perform a graphic beta move and obtain the graph from the lower part of the figure.

The red 3 can connect, in the sense explained by the switch mechanism from Teaser (II) with blue 1′ or blue 2′, all three of them belonging to the controlling synapse. Say red 3  connects with blue 1′ and look what happens:


OK, so we obtain a connection between blue 1 and red 3′. Suppose now that red 3 connects with blue 2′, look:


Yes, blue 1 does not connect with red 3′, they just exchanged a pair of termination gates. That’s how the pair of synapses work.

Finally, let me remark that the use of termination gates is a bit ugly, it breaks the symmetry,  is not really needed.

Teaser: B-type neural networks in graphic lambda calculus (II)

The connections in a B-type neural network can be trained.  The following  quote and figure are taken from the article  Turing’s Neural Networks of 1948, by Jack Copeland and Diane Proudfoot:

Turing introduced a type of neural network that he called a ‘B-type unorganised machine’, consisting of artificial neurons, depicted below as circles, and connection-modifiers, depicted as boxes. A B-type machine may contain any number of neurons connected together in any pattern, but subject always to the restriction that each neuron-to-neuron connection passes through a connection-modifier.


A connection-modifier has two training fibres (coloured green and red in the diagram). Applying a pulse to the green training fibre sets the box to pass its input–either 0 or 1–straight out again. This is pass mode. In pass mode, the box’s output is identical to its input. The effect of a pulse on the red fibre is to place the modifier in interrupt mode. In this mode, the output of the box is always 1, no matter what its input. While it is in interrupt mode, the modifier destroys all information attempting to pass along the connection to which it is attached. Once set, a connection-modifier will maintain its function unless it receives a pulse on the other training fibre. The presence of these modifiers enables a B-type unorganised machine to be trained, by means of what Turing called ‘appropriate interference, mimicking education’.

Let’s try to construct such a connection in graphic lambda calculus.  I shall use the notations from the previous post  Teaser: B-type neural networks in graphic lambda calculus (I).

3. Connections.   In lambda calculus, Church booleans are the following terms: TRUE = \lambda x . \lambda y .x and FALSE = \lambda x. \lambda y. y (remark that TRUE is the combinator K).  By using the algorithm for transforming lambda calculus terms into graphs in GRAPH, we obtain the following graphs:


They act on other graphs (A, B) like this:


The graphs are almost identical: they are both made by a 2-zipper with an additional termination gate and a wire. See the  post   Combinators and zippers  for more explanations about TRUE, or K.

I am going to exploit this structure in the construction of a connection. We are going to need the following ingredients: a 2-zipper, an INPUT BOX (otherwise called “switch”, see further) and an OUTPUT BOX,

which is almost identical with a switch (it is identical as a graph, but we are going to connect it with other graphs at each labelled edge):


I start with the following description of objects and moves from the freedom sector of graphic lambda calculus (the magenta triangles were used also in the previous post).  I call the object from the middle of the picture a switch.


As you can see, a switch can be transformed into one of the two graphs (up and down parts of the figure).  We can exploit the switch in relation with the TRUE and FALSE graphs. Indeed, look at the next figure, which describes graphs almost identical with the TRUE and FALSE graph (as represented by using zippers), with an added switch:


Now we are ready for describing a connection like the one from the B-type neural networks (only that better, because it’s done in graphic lambda calculus, thus much more expressive than boolean expressions). Instead of training the connection by a boolean TRUE of FALSE input (coming by one of the green or red wires in the first figure of the post), we replace the connection by an OUTPUT BOX (should I call it “synapse”? I don’t know yet) which is controlled by a switch. The graph of a connection is the following:


The connection between an axon and a dendrite is realized by having the axon at “1” and the dendrite at “3”. We may add a termination gate at “2”, but this is irrelevant somehow. At the top of the figure we have a switch, which can take any of the two positions corresponding, literary, to TRUE or FALSE. This will transform the OUTPUT BOX into one of the two possible graphs which can be obtained from a switch.

You may ask why did I not put directly a switch instead of an OUTPUT BOX. Because, in this way, the switch itself may be replaced by the OUTPUT BOX of another connection. The second reason is that by separating the graph of the connection into a switch, a 2-zipper and an OUTPUT BOX, I proved that what is making the switch to function is the TRUE-FALSE like input, in a rigorous way. Finally, I recall that in graphic lambda calculus the green dashed ovals are only visual aids, without intrinsic significance. By separating the OUTPUT BOX from the INPUT BOX (i.e. the switch) with a zipper, the graph has now an unambiguous structure.