Tag Archives: lambda calculus

Graphic lambda calculus and chemlambda(III)

This post introduces chemlambda v2. I continue from the last post, which describes the fact that chemlambda v1, even if it has only local rewrites, it is not working well when used with the dumbest possible reduction algorithms.

Nature has to work with the dumbest algorithms, or else we live in a fairy tale.

Chemlambda v2 is an artificial chemistry, in the following sense:

  • it is a graph rewrite system over oriented fatgraphs made of a finite number of nodes, from the list: 5 types of 3-valent nodes, A (application), L (lambda abstraction), FO (fanout), FI (fanin), FOE (external fanout), 1 type of 2-valent node Arrow, 3 types of 1-valent nodes, FRIN (free in), FROUT (free out), T (termination). Compared to chemlambda v1, there is a new node, the FOE. The nodes, not the rewrites, are described in this early explanation called Welcome to the soup. (Mind that the gallery of example which is available at the end of these explanation mixes chemlambda v1 and chemlambda v2 examples.)
  • the rewrites CO-COMM and CO-ASSOC of chemlambda v1 are not available, instead there are several new DIST rewrites: FO-FOE, L-FOE, A-FOE, FI-FO, and a new beta like rewrite FI-FOE. As in chemlambda v1, the patterns of the rewrites fit with the interaction combinator rewrites if we forget the orientation of the edges, but the 3-valent nodes don’t have a principal port, so they don’t form interaction nets. Moreover, the are conflicts among the rewrites, i.e. there are configurations of 3 nodes such that we have a node which belongs to two pairs of nodes which may admit rewrites. The order of application of rewrites may matter for such conflicts.
  • there is an algorithm of application of rewrites, which is either the deterministic greedy algorithm with a list of priority of rewrites (for example beta rewrites have priority over DIST rewrites, whenever there is a conflict), or the random application algorithm.

 

Sources for chemlambda v2:

 

The goal of chemlambda v2: to explore the possibility of molecular computers in this artificial chemistry.

This needs explanations. Indeed,  does the system work with the simplest random algorithm? We are not interested into semantics, because it is, or it relies on global notions, We are not (very) interested into reduction strategies for lambda terms, because they are not as simple as the dumbest algorithms we use here. Likewise for readback, etc.

So, does chemlambda v2 work enough for making molecular computers?  Pure untyped lambda calculus reduction problems are an inspiration. If the system works for the particular case of graphs related to lambda terms then this is a bonus for this project.

As you see, instead of searching for an algorithm which could implement, decentralized say, a lambda calculus reduction strategy, we ask if a particular system reduces (graphs related to) terms with one algorithm from the fixed class of dumbest ones.

That is why the universality in the sense of Lafont is fascinating. In this post I argued that Lafont universality property of interaction combinators means, in this pseudo-chemical sense, that the equivalent molecular computer based on interaction combinators reactions (though not the translations) works for implementing a big enough class of reactions which are Turing universal in particular (Lafont  shows concretely that he can implement Turing machines).

(continues with the part IV)

Advertisements

Graphic lambda calculus and chemlambda (II)

Chemlambda v2 is an entirely different project than GLC and chemlambda v1. This post continues from the first part. It explains the passage towards chemlambda v2.

A problem of GLC and chemlambda v1 is that research articles are opinion pieces, not validated by programs and experiments. The attempt to use GLC with the Actor Model in order to build a decentralized computing proposal, aka distributed GLC, failed because of this. Does all of this work?

The CO-COMM and CO-ASSOC rewrites lead to the situation that,  in order to be useful, either:

  • they have to be applied by a human or by a(n unknown) very clever algorithm
  • or they are applied in both directions randomly, which implies that no GLC or chemlambda v1 reduction ever terminates.

Here is an early visual tutorial  which introduces the nodes of chemlambda v2.  At the end of it you are pointed to a gallery of examples which mixes chemlambda v1 with chemlambda v2, like these:

 

Or, another example, the Y combinator. In chemlambda v1, without using CO-COMM and CO-ASSOC, the Y combinator applied to an unspecified term behaves like this.  In chemlambda v2, where there is a supplimentary node and other rewrites, the Y combinator behaves almost identically, but some nodes (the yellow FOE here instead of the green FO before) are different:

 

ycombi

 

 

See this page for a list of works, tagged with the version of chemlambda used.

(continues with part III)

 

 

Graphic lambda calculus and chemlambda (I)

Looks like there is a need to make a series of posts dedicated to the people who try to use this blog as a source in order to understand graphic lambda calculus (aka GLC) and chemlambda. This is the first one.

Sources for GLC:

  • the best source is the article M. Buliga, Graphic lambda calculus. Complex Systems 22, 4 (2013), 311-360   (link to article in journal) (link to article in arXiv)
  • you can see the GLC page (link) here, which has been updated many times after chemlambda appeared, but it is unmodified starting from the section “What is graphic lambda calculus?” and there are links to many others posts here which explain GLC as it is, that is before chemlambda.

GLC is a graph rewriting system for fatgraphs made of trivalent or 1-valent nodes. The trivalent nodes used are A (application), L (lambda), FO (fanout), epsilon (for dilations). There is one 1-valent node, T (termination). Loops with no nodes and arrows, i.e. oriented edges with no nodes are accepted as well. There is no algorithm proposed for the reduction of these graphs.

The graph rewrites are:

– local ones (i.e. involving only a finite number, a priori given, of nodes and edges)

  •   graphic beta move, which is like Lamping graph rewrite, only purely local, i.e. there is no limitation on the global shape of the graph, thus it is  somehow more general than the beta rewrite from untyped lambda beta calculus; a possible interpretation is C= let x=B in A rewrites to x=B and C=A

 

  • betaCO-COMM and CO-ASSOC rewrites for the FO (fanout) which are, due to the orientation of the edges, really like graphical, AST forms of co-commutativity and co-associativity
  • local pruning group of rewrites, which describe the interaction of the trivalent nodes with the T node; incidentally T and FO interact like if T is a co-unit for FO
  • a group of rewrites for the dilation nodes, which are those of emergent algebras, which involve the fanout FO and the dilation nodes

 

– global rewrites:

  • global fan-out
  • global pruning

 

In section 3 of the article on GLC is given an algorithm of conversion of untyped lambda terms into graphs which is a little more than a modification of the AST of the lambda term, in such a way that the orientation of the edges is respected. That is because the lambda node L has one incoming edge and two outgoing edges!

I prove then that GLC can be used for untyped lambda beta calculus, but also for emergent algebras and also for a variant of knot theoretic graphs where there is no need for them to be planar. Finally, I show that there might be other “sectors” of graphs which may be interesting, regardless of their meaning (or lack of it) with respect to lambda calculus.

The problem of GLC is that it has these global rewrites. Can these be replaced by local rewrites?

That’s how chemlambda appeared.

I was aware that some applications of global fanout can be done with local rewrites, but not all. Also, the interest in GLC was not extended to the interest into emergent algebras, to my dismay.

On the other side I became obsessed with the idea that if the global fanout can be replaced by local rewrites entirely then it should be possible in principle to see the rewrites as chemical reactions between individual molecules. A bigger problem would be then: would these reactions reduce the graph-molecules under the dumbest algorithm among all, the random one? Nature functions like this, so any algorithm which would be global in some sense is completely excluded.

This led me to write the article: M. Buliga, Chemical concrete machine (link to DOI) (link to arXiv version).  This is chemlambda v1, which is actually a transition from GLC to something else, or better said to another research subject in the making.

Other sources for this mix glc-chemlambda v1:

 

Chemlambda v1, or the “chemical concrete machine”, is a graph rewriting algorithm which uses the trivalent nodes A, L, FI (fan-in), FO, and the 1-valent node T and only local rewrites:

  • the graphic beta rewrite (between the nodes L and A) and the fan-in rewrite (between the nodes FI and FO)

 

convention_2

 

  • the CO-COMM and CO-ASSOC rewrites

 

 

convention_3

 

  • two DIST (from distributivity) rewrites, for the pairs A-FO and L-FO

 

 

convention_6

  • local pruning rewrites (involving the 1-valent node T)

 

convention_4

 

  •  and elimination of loops

 

convention_5

 

As you see, all rewrites except CO-COMM and CO-ASSOC are alike the ones from Lafont article Interaction combinators, except that the graphs are directed and the nodes don’t have a principal port for interaction. Here are the interaction combinators rewrites

 

 

lafont-2

In the chemical concrete machine article are mentioned Berry and Boudol chemical abstract machine and Fontana and Buss alchemy, but not Lafont.  My fault. From what I knew then the beta rewrite came from Lamping or better Wadsworth, the fan-in came from Turaev (knotted trivalent graphs), and the DIST rewrites came from the graphical version of linear emergent algebras, or even better from the Reidemeister 3 rewrite in knot theory.

 

 

In this article there is no algorithm for application of the rewrites. (You shall see that in chemlambda v2, which is an artificial chemistry,  there are actually several, among them the deterministic greedy one, with a list of priority of the rewrites, because there are collisions otherwise, and the random one, which interested me the most.)

However I suggest that the rewrites can be seen as done in a truly chemical sense, mediated by (invisible) enzymes, each rewrite type with it’s enzyme.

I proved that we can translate from GLC to chemlambda v1 and that global fan-out and global pruning can be replaced by sequences of rewrites from chemlambda v1. There was no proof that this replacement of the global rewrites with cascades of local rewrites can be done by the algorithms considered. I proved the Turing universality by using the BCKW system of combinators.

The chemical concrete machine article ends however with:

“With a little bit of imagination, if we look closer to what TRUE, FALSE and IFTHENELSE are doing, we see that it is possible to adapt the IFTHENELSE to a molecule which releases, under the detection of one molecule (like TRUE), the ”medicine” A, and under the detection of another molecule (like FALSE) the ”medicine” B.”

The chemlambda page (link) here is reliable for chemlambda v1, but it also contain links to newer versions.

(continues with part II)

 

Deterministic vs random, an example of grandiose shows vs quieter, functioning anarchy

In the following video you can see the deterministic, at the right random evolution of the same molecule, duplex.mol from the chemlambda repository. They take about the same time.

The deterministic one is like a ballet, it has a comprehensible development, it has rhythm and drama. Clear steps and synchronization.

The random one is more fluid, less symmetric, more mysterious.

What do you prefer, a grand synchronized show or a functioning, quieter anarchy?

Which one do you think is more resilient?

What is happening here?

The molecule is inspired from lambda calculus. The computation which is encoded is the following. Consider the lambda term for the identity function, i.e. I=Lx.x. It has the property that IA reduces to A for any term A. In the molecule it appears as a red trivalent node with two ports connected, so it looks like a dangling red globe. Now, use a tree of fanouts to multiply (replicate) this identity 8 times, then build the term

(((II)(II))((II)(II)))(((II)(II))((II)(II)))

Then use one more fanout to replicate this term into two copies and reduce all. You’ll get two I terms, eventually.
In the deterministic version the following happens.

– the I term (seen as a red dangling node) is replicated (by sequence of two rewrites, detail) and gradually the tree of fanouts is destroyed

– simultaneously, the tree of applications (i.e. the syntactic tree of the term, but seen with the I’s as leaves) replicates by the fanout from the end

– because the reduction is deterministic, we’ll get 16 copies of I’s exactly when we’ll get two copies of the application tree, so in the next step there will be a further replication of the 16 I’s into 32 and then there will be two, disconnected, copies of the molecule which represents ((II)(II))((II)(II))

– after that, this term-molecule reduces to (II)(II), then to II, then to I, but recall that there are two copies, therefore you see this twice.

In the random version everything mixes. Anarchy. Some replications of the I’s reach the tree of applications before it has finished to replicate itself, then reductions of the kind II –> I happen in the same time with replications of other pieces. And so on.
There is no separation of stages of this computation.
And it still works!

I used quiner_experia, with the mol file duplex.mol. The first time I modified all the weights to 0 (to have deterministic application) and took the rise parameter=0 (this is specific to quiner_experia, not present in quiner) too, because the rise parameter lower the probabilities of new rewrites, exponentially, during the same step, in order to give fair chances to any subset of all possible rewrites possible.
Then I made a screencast of the result, without speeding it, and by using safari to run the result.
For the random version I took all the weights equal to 1 and the rise parameter equal to 8 (empirically, this gives the most smooth evolution, for a generic molecule from the list of examples). Ran the result with safari and screencasted it.
Then I put the two movies one near the other (deterministic at left, random at right) and made a screencast of them running in parallel. (Almost, there is about 1/2 second difference because I started the deterministic one first, by hand).
That’s it, enjoy!
For chemlambda look at the trailer from the collections of videos I have here on vimeo.

Crossings as pairs of molecular bonds; boolean computations in chemlambda

I collect here the slightly edited versions of a stream of posts on the subject from the microblogging chemlambda collection. Hopefully this post will give a more clear image about this thread.

Here at the chorasimilarity open notebook, the subject has been touched previously, but perhaps that the handmade drawings made it harder to understand (than with the modern 🙂 technology from the chemlambda repository):

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

(especially the last picture!)

All this comes with validation means. This is a very powerful idea: in the future validation will replace peer review, because it is more scientific than hearsay from anonymous authority figures (aka old peer review) and because it is more simple to implement than a network of hearsay comments (aka open peer review).

All animations presented here are obtained by using the script quiner.sh and various mol files. See instructions about how you can validate (or create your own animations) here:
https://github.com/chorasimilarity/chemlambda-gui/blob/gh-pages/dynamic/README.md

Here starts the story.

(Source FALSE is the hybrid of TRUE, boole.mol file used)

boole

Church encoding gives a way to define boolean values as terms in the lambda calculus. It is easy:

TRUE= Lx.(Ly.x)

FALSE= Lx.(Ly.y)

So what? When we apply one of these terms to another two, arbitrary terms X and Y, look what happens: (arrows are beta reductions (Lx.A)B – – > A[x:=B] )

(TRUE X) Y – – > (Ly.X) Y – – > X (meaning Y goes to the garbage)

(FALSE X) Y – – > (Ly.y) Y – – > Y (meaning X goes to the garbage)

It means that TRUE and FALSE select a way for X and Y: one of them survives, the other disappears.

Good: this selection is an essential ingredient for computation

Bad: too wasteful! why send a whole term to the garbage?

Then, we can see it otherwise: there are two outcomes: S(urvival) and G(arbage), there is a pair of terms X and Y.

– TRUE makes X to connect with S and Y to connect with G

– FALSE makes X to connect with G and Y to connect with S

The terms TRUE and FALSE appear as molecules in chemlambda, each one made of two red nodes (lambdas) and a T (termination) node. But we may dispense of the T nodes, because they lead to waste, and keep only the lambda nodes. So in chemlambda the TRUE and FALSE molecules are, each, made of two red (lambda) nodes and they have one FROUT (free out).

They look almost alike, only they are wired differently. We want to see how it looks to apply one term to X and then to Y, where X and Y are arbitrary. In chemlambda, this means we have to add two green (A) application nodes, so TRUE or FALSE applied to some arbitrary X and Y appear, each, as a 4 node molecule, made of two red (lambda) two green (A), with two FRIN (free in) nodes corresponding to X and Y and two FROUT (free out) nodes, corresponding: one to the deleted termination node, thus this is the G(arbage) outcome, and the other to the “output” of the lambda terms, thus this is the S(urvival) outcome.

But the configuration made of two green A nodes and two red L nodes is the familiar zipper which you can look at in this post

betazipper

In the animation you see TRUE (at left) and FALSE (at right), with the magenta FROUT nodes and the yellow FRIN nodes.

The zipper configurations are visible as the two vertical strings made of two green, two red nodes.

What’s more? Zippers, they do only one thing: they unzip.

The wiring of TRUE and FALSE is different. You can see the TRUE and FALSE in the lower part of the animation. I added four Arrow (white) nodes in order to make the wiring more visible. Arrow nodes are eliminated in the COMB cycle, they have only a fleeting existence.

This shows what is really happening: look at each (TRUE-left, FALSE-right) configuration. In the upper side you have 4 nodes, two magenta, two yellow, which are wired together at the end of the computation. In the case of TRUE they end up wired in a X pattern, in the case of FALSE they end up wired in a = pattern.

At the same time, in the lower side, before the start of the computation, you see the 4 white nodes which: in the case of TRUE are wired in a X pattern, in the case of FALSE are wired in a = pattern. So what is happening is that the pattern ( X or = ) is teleported from the 4 white nodes to the 4 magenta-yellow nodes!

The only difference between the two molecules is in this wire pattern, X vs =. But one is the hybrid of the other, hybridisation is the operation (akin to the product of knots) which has been used and explained in the post about senescence and used again in more recent posts. You just take a pair of bonds and switch the ends. Therefore TRUE and FALSE are hybrids, one of the other.

(Source Boolean wire, boolewire.mol file used )

If you repeat the pattern which is common to TRUE and FALSE molecules then you get a boolean wire, which is more impressive “crossings teleporter”. This time the crosses boxed have been flattened, but the image is clear:

boolewire

Therefore, TRUE and FALSE represent choices of pairs of chemical bonds! Boolean computation (as seen in chemlambda) can be seen as management of promises of crossings.

(Source Promises of crossings, ifthenelsecross.mol file used )

You see 4 configurations of 4 nodes each, two magenta and two yellow.

In the upper left side corner is the “output” configuration. Below it and slightly to the right is the “control” configuration. In the right side of the animation there are the two other configurations, stacked one over the other, call them “B” (lower one) and “C” (upper one).

Connecting all this there are nodes A (application, green) and L (lambda, red).

ifthenelsecross

You see a string of 4 green nodes, approximately vertical, in the middle of the picture, and a “bag” of nodes, red and green, in the lower side of the picture. This is the molecule for the lambda term

IFTHENELSE = L pqr. pqr

applied to the “control” then to the “B” then to the “C”, then to two unspecified “X” and “Y” which appear only as the two yellow dots in the “output” configuration.

After reductions we see what we get.

Imagine that you put in each 4 nodes configuration “control”, “B” and “C”, either a pair of bonds (from the yellow to the magenta nodes) in the form of an “X” (in the picture), or in the form of a “=”.

“X” is for TRUE and “=” is for false.

Depending on the configuration from “control”, one of the “B” or “C” configuration will form, together with its remaining pair of red nodes, a zipper with the remaining pair of green nodes.

This will have as an effect the “teleportation” of the configuration from “B” or from “C” into the “output”, depending on the crossing from “control”.

You can see this as: based on what “control” senses, the molecule makes a choice between “B” and “C” promises of crossings and teleports the choice to “output”.

(Source: Is there something in the box?, boxempty.mol used)

I start from the lambda calculus term ISZERO and then I transform it into a box-sensing device.

In lambda calculus the term ISZERO has the expression

ISZERO = L a. ((a (Lx.FALSE)) TRUE)

and it has the property that ISZERO N reduces either to TRUE (if N is the number 0) or FALSE (if N is a number other than 0, expressed in the Church encoding).

The number 0 is
0 = FALSE = Lx.Ly.y

For the purpose of this post I take also the number 2, which is in lambda calculus

2=Lx.Ly. x(xy)

(which means that x is applied twice to y)

Then, look: (all reductions are BETA: (Lx.A)B – – > A[x:=B] )

ISZERO 0 =
(L a. ((a (Lx.FALSE)) TRUE) ) (Lx.Ly.y) – – >
((Lx.Ly.y) (Lx.FALSE)) TRUE – – >
(Ly.y)TRUE – – > (remark that Lx.FALSE is sent to the garbage)
TRUE (and the number itself is destroyed in the process)

and

ISZERO 2 =
(L a. ((a (Lx.FALSE)) TRUE) ) (Lx.Ly. x(xy)) – – >
((Lx.Ly. x(xy)) (Lx.FALSE)) TRUE – – > (fanout of Lx.FALSE performed secretly)
(Lx.FALSE) ((Lx.FALSE) TRUE) – – >
FALSE ( and (Lx.FALSE) TRUE sent to the garbage)

Remark that in the two cases there was the same number of beta reductions.

Also, the use of TRUE and FALSE in the ISZERO term is… none! The same reductions would have been performed with an unspecified “X” as TRUE and an unspecified “Y” as FALSE.

(If I replace TRUE by X and FALSE by Y then I get a term which reduces to X if applied to 0 and reduces to Y if applied to a non zero Church number.)

Of course that we can turn all this into chemlambda reductions, but in chemlambda there is no garbage and moreover I want to make the crossings visible. Or, where are the crossings, if they don’t come from TRUE and FALSE (because it should work with X instead of TRUE and Y instead of FALSE).

Alternatively, let’s see (a slight modification of) the ISZERO molecule as a device which senses if there is a number equal or different than 0, then transforms, according to the two cases, into a X crossing or a = crossing.

Several slight touches are needed for that.

1. Numbers in chemlambda appear as stairs of pairs of nodes FO (fanout, green) and A (application, green), as many stairs as the number which is represented. The stairs are wrapped into two L (lambda, red) nodes and their bonds.
We can slightly modify this representation so that it appears like a box of stairs with two inputs and two outputs, and aby adding a dangling green (A, application) node with it’s output connected to one of its inputs (makes no sense in lamnda calculus, but behaves well in the beta reductions as performed in chemlambda).

In the animation you can see, in the lower part of the figure:
-at left the number 0 with an empty box (there are two Arrow (white) nodes added for clarity)
-at right the number 2 with a box with 2 stairs
… and in each case there is this dangling A node (code in the mol file of the form A z u u)
boxempty

2. The ISZERO is modified by making it to have two FRIN (free in, yellow) and two FROUT (free out, magenta) nodes which will be involved in the final crossing(s). This is done by a clever (hope) change of the translation of the ISZERO molecule into chemlambda: first the two yellow FRIN nodes represent the “X” and the “Y” (which they replace the FALSE and the TRUE, recall), and there are added a FOE (other fanout node, yellow) and a FI (fanin node, red) in strategic places.

________________________________

let x=A in B in chemlambda

The beta reduction from lambda calculus is easy to be understood as the command
let x=B in A
It corresponds to the term (Lx.A)B which reduces to A[x=B], i.e to the term A where all instances of x have been replaced by B.
(by an algorithm which is left to be added, there are many choices among them!)

In Christopher P. Wadsworth, Semantics and Pragmatics of the Lambda Calculus , DPhil thesis, Oxford, 1971, and later John Lamping, An algorithm for optimal lambda calculus reduction, POPL ’90 Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p. 16-30, there are proposals to replace the beta rule by a graph rewrite on the syntactic tree of the term.

These proposals opened many research paths, related to call by name strategies of evaluations, and of course going to the Interaction Nets.

The beta rule, as seen on the syntactic tree of a term, is a graph rewrite which is simple, but the context of application of it is complex, if one tries to stay in the real of syntactic trees (or that of some graphs which are associated to lambda terms).

This is one example of blindness caused by semantics. Of course that it is very difficult to conceive strategies of applications of this local rule (it involves only two nodes and 5 edges)  so that the graph after the rewrite has a global property (means a lambda term).

But a whole world is missed this way!

In chemlambda the rewrite is called BETA or A-L.
see the list of rewrites
http://chorasimilarity.github.io/chemlambda-gui/dynamic/moves.html

In mol notation this rewrite is

L 1 2 c , A c 3 4  – – > Arrow 1 4 , Arrow 3 2

(and then is the turn of COMB rewrite to eliminate the arrow elements, if possible)

As 1, 2, 3, 4, c are only port variables in chemlambda, let’s use other:

L A x in , A in B let  – – >  Arrow A let , Arrow B x

So if we interpret Arrow (via the COMB rewrite) as meaning “=”, we get to the conclusion that

let x=B in A

is in chemlambda

L A x in

A in B let

Nice. it almost verbatim the same thing.  Remark that the command”let” appears as a port variable too.

Visually the rewrite/command is this:

beta
As you see this is a Wadsworth-Lamping kind of graph rewrite, with the distinctions that:
(a) x, A, B are only ports variables, not terms
(b) there is no constraint for x to be linked to A

The price is that even if we start with a graph which is related to a lambda term, after performing such careless rewrites we get out of the realm of lambda terms.

But there is a more subtle difference: the nodes of the graphs are not gates and the edges are not wires which carry signals.

The reduction works well for many fundamental examples,
http://chorasimilarity.github.io/chemlambda-gui/dynamic/demos.html
by a simple combination of the beta rewrite and those rewrites from the DIST family I wrote about in the post about duplicating trees.
https://chorasimilarity.wordpress.com/2015/05/04/the-illustrated-shuffle-trick-used-for-tree-duplication/

So, we get out of lambda calculus, what’s wrong with that? Nothing, actually, it turns out that the world outside lambda, but in chemlambda, has very interesting features. Nobody explored them, that is why is so hard to discuss about that without falling into one’s preconceptions (has to be functional programming, has to be lambda calculus, has to be a language, has to have a global semantics).
___________________________________________

All successful computation experiments with lambda calculus in one list

What you see in this links: I take a lambda term, transform it into a artificial molecule, then let it reduce randomly, with no evaluation strategy. That is what I call the most stupid algorithm. Amazing is that is works.
You don’t have to believe me, because you can check it independently, by using the programs available in the github repo.

Here is the list of demos where lambda terms are used.

Now, details of the process:
– I take a lambda term and I draw the syntactic tree
– this tree has as leaves the variables, bound and free. These are eliminated by two tricks, one for the bound variables, the other for the free ones. The bound variables are eliminated by replacing them with new arrows in the graph, going from one leg of a lambda abstraction node, to the leaf where the variable appear. If there are more places where the same bound variable appears, then insert some fanout nodes (FO). For the free variable do the same, by adding for each free variable a tree of FO nodes. If the bound variable does not appear anywhere else then add a termination (T) node.
– in this way the graph which is obtained is no longer a tree. It is a trivalent graph mostly, with some free ends. It is an oriented graph. The free ends which correspond to a “in” arrow are there for each free variable. There is only one end which correspond to an “out” arrow, coming from the root of the syntactic tree.
– I give a unique name to each arrow in the graph
– then I write the “mol file” which represents the graph, as a list of nodes and the names of arrows connected to the nodes (thus an application node A which has the left leg connected to the arrow “a”, the right leg connected to the arrow “b” and the out leg connected to “c”, is described by one line “A a b c” for example.

OK, now I have the mol file, I run the scripts on it and then I look at the output.

What is the output?

The scripts take the mol file and transform it into a collection of associative arrays (that’s why I’m using awk) which describe the graph.

Then they apply the algorithm which I call “stupid” because really is stupidly simplistic: do a predetermined number of cycles, where in each cycle do the following
– identify the places (called patterns) where a chemlambda rewrite is possible (these are pairs of lines in the mol file, so pairs of nodes in the graph)
– then, as you identify a pattern, flip a coin, if the coin gives “0” then block the pattern and propose a change in the graph
– when you finish all this, update the graph
– some rewrites involve the introduction of some 2-valent nodes, called “Arrow”. Eliminate them in a inner cycle called “COMB cycle”, i.e. comb the arrows
-repeat

As you see, there is absolutely no care about the correctness of the intermediary graphs. Do they represent lambda terms? Generically no!
Are there any variable which are passed, or evaluations of terms which are done in some clever order (eager, lazy, etc)? Not at all, there are no other variables than the names of the arrows of the graph, or these ones have the property that they are names which appear twice in the mol file (once in a port “in”, 2nd in a port “out”). When the pattern is replaced these names disappear and the names of the arrows from the new pattern are generated on the fly, for example by a counter of arrows.

The scripts do the computation and they stop. There is a choice made over the way of seeing the computation and the results.
One obvious choice would be to see the computation as a sequence of mol files, corresponding to the sequence of graphs. Then one could use another script to transform each mol file into a graph (via, say, a json file) and use some graph visualiser to see the graph. This was the choice in the first scripts made.
Another choice is to make an animation of the computation, by using d3.js. Nodes which are eliminated are first freed of links and then they vanish, while new nodes appear, are linked with their ports, then linked with the rest of the graph.

This is what you see in the demos. The scripts produce a html file, which has inside a js script which uses d3.js. So the output of the scripts is the visualisation of the computation.

Recall hat the algorithm of computation is random, therefore it is highly likely that different runs of the algorithm give different animations. In the demos you see one such animation, but you can take the scripts from the repo and make your own.

What is amazing is that they give the right results!

It is perhaps bizzare to look at the computation and to not make any sense of it. What happens? Where is the evaluation of this term? Who calls whom?

Nothing of this happens. The algorithm just does what I explained. And since there are no calls, no evaluations, no variables passed from here to there, that means that you won’t see them.

That is because the computation does not work by the IT paradigm of signals sent by wires, through gates, but it works by what chemists call signal transduction. This is a pervasive phenomenon: a molecule enters in chemical reactions with others and there is a cascade of other chemical reactions which propagate and produce the result.

About what you see in the visualisations.
Because the graph is oriented, and because the trivalent nodes have the legs differentiated (i.e. for example there might be a left.in leg, a right.in leg and a out leg, which for symmetry is described as a middle.out leg) I want to turn it into an unoriented graph.
This is done by replacing each trivalent node by 4 nodes, and each free end or termination node by 2 nodes each.
For trivalent nodes there will be one main node and 3 other nodes which represents the legs. These are called “ports”. There will be a color-coded notation, and the choice made is to represent the nodes A (application) and FO by the main node colored green, the L (lambda) and FI (fanin, exists in chemlamda only) by red (actually in the demos this is a purple)
and so on. The port nodes are coloured by yellow for the “in” ports and by blue for the “out” ports. The “left”, right”, “middle” types are encoded by the radius of the ports.

__________________________________________________