A chemical concrete machine for lambda calculus

This post is a call for building one. More precisely, for building one for graphic lambda calculus, which satisfies all the requests  from section 5 of The chemical abstract machine by Berry and Boudol  for a calculus more general than lambda calculus.

First a short comment on “The chemical abstract machine”. This is a very interesting article, thanks are due  to Mike Stay for telling me about it, in relation to what is described in my previous post  Can graphic lambda calculus be implemented in some form of DNA computing?  The following quote describes exactly what I was looking for (p.1 from the linked file):

Intuitively, the state of a system is like a chemical solution in which floating molecules can interact with each other according to reaction rules … Solutions are finite multisets of molecules …

But from here I will not jump to identify terms in lambda calculus with solutions, like it’s done in section 5.2 on the $\gamma$ calculus. Nor shall I use membranes and airlocks, as useful as they seem (and probably there is a possible implementation of those in graphic lambda calculus).

Finally, there is something which I don’t understand in the article, concerning variables and substitutions. I might be wrong, please tell if so, but apparently an abstract chemical machine still uses names for variables, which appear as “ions”. What I don’t get is: how are two solutions, each one corresponding to a lambda term, the same if the two lambda terms are the same by renaming the variables?

In graphic lambda calculus there is no such problem, because there are no variable names. Moreover, lambda terms (which appear as certain graphs in graphic lambda calculus) are molecules and the moves between them (like the graphic beta move) are chemical reactions.

How can this be done? Here is sketch, mind you that I propose things which I believe are possible from a chemical perspective, but I don’t have any chemistry knowledge.  If you do, and if you are interested to make a chemical concrete machine for graphic lambda calculus, then please contact me.

The graphs from $GRAPH$ which we need for the lambda calculus sector of the graphic lambda calculus, are  made by three gates corresponding to lambda abstraction, application and fan-out (I shall ignore the termination gate). So we need three molecules. The five coloured triangles are parts of the molecules which bond one with the other. Say there is a bond strength associated with each pairing, such that the bigger is the bond strength, more easily the bond is made and more stronger it is.

Remark that the molecules from the right of the figure don’t seem to have oriented arrows inside. That is why we need several types of bonding places. The table of bond strengths is this: The strength coefficients are taken out of … my imagination, such that they satisfy a number of mental experiments I did with them.  As you see there are:

• two bonding places — yellow and red, which correspond to input half-arrows,
• two bonding places — blue and green, which correspond to output half-arrows,
• one bonding place – magenta, which can be seen as well as input or output half-arrow.

The bipartite graph from the lower part of the figure shows which bonding places CAN bond (i.e. they have bonding strength not equal to $0$).  In the upper part of the figure there is a table with strengths.

As you see, this solves the problem of representing decorated nodes of oriented graphs. Nice.

Now, let’s pass to the main move, the graphic beta move. This should be a chemical reaction. Imagine that we have an enzyme called “beta”, which recognizes magenta-magenta bonds. When it does recognize such a bond, it does like in the next figure: So, the beta enzyme cuts the other bonds, like in the middle part of the picture, then the bonding places bond according to the strength table. Voila!

If you want to play with, here is a “chemical” representation of the 2-zipper, try to see how it works. I hope this adds more details to my call of building a real, concrete chemical machine (or to recognize one with at least the expressivity of untyped lambda calculus). Can anybody do it?