UPDATE: This is from yesterday 15.10.2019. It gives the possible RHS of DIST rewrites in a more precise way, compatible with the 6 nodes: A, FI, D (port 2 “in”) and L, FO, FOE (port 2 “out”) (each node has port 1 “in” and port 3 “out”). Moreover which can be decorated with generic dilations which satisfy em-convex. It turns out that there are exactly two possibilities for each rewrite. However, there are fewer than 3^36 rewrite systems which are potentially interesting, because many of these rewrites inhibit others.
For example all the rewrites used in the working version of kali are there (with the exception of those involving the node FO, there is a separate treatment for this node; also I ignore for the moment the rewrites invoving T and I take for granted the 3 beta-like rewrites, which are not generated by the rhs.js script, because they are not DIST rewrites).The version I have today shortens the list a lot and soon enough will be merged into a more explorable version of kali.
How many rewrites are possible in anharmonic lambda and how do they relate one with the other? Is there a way to discover experimentally the best collection of rewrites? I think it is and that’s what I’m doing right now.
Let me explain.
Suppose we start by the anharmonic group, isomorphic with S(3), or why not we start with S(4), with an eye into the relation it has with projective geometry. But basically we want to associate to every element of the group (call it G) a trivalent node with named ports “1”, “2” and “3”, such that we can decorate the edges of a graph made by such nodes by “terms” which are somehow relevant with respect to the geometric nature of the group G (either S(3) as the anharmonic group, or S(4) as it appears in projective geometry). For the moment how we do that, or why are we doing it, or even what that has to do with lambda calculus are irrelevant questions.
There are two big possibilities further.
Either we work with graphs with undirected edges, but we restrict the patterns which trigger rewrites at pairs of nodes connected via the ports “3”, i.e. at pairs of nodes linked by an edge which connects the port “3” of on enode with the port “3” of the other. For example this is the case in Interaction Combinators. The advantage is that there will never be conflicting rewrites.
Or we work with graphs with directed edges, we attach orientations to ports (say ports “1” is always “in”, i.e. the orientation point to the node, the port “3” is always “out” and the port “2” may be “in” or “out”, depending on the node type) and we ask that any edge connects a port which is “in” with a port which is “out”. Then we look for patterns which trigger rewrites ahich are made by a pair of nodes linked by an edge which connects a port “3” with a port “1”. This is like in chemlambda. The advantage here is opposite: we allow conflicting rewrites.
So in either case we think about rewrites which have as LHS (left hand side) a pair of nodes, as explained, and as RHS (right hand side) either no node (actually two edges), like in the case of the beta rewrite, or 4 nodes. The pattern of 4 nodes should be like in Interaction Combinators (say like GAMMA-DELTA rewrites) or like the DIST rewrites in chemlambda.
If I take the second case, namely graphs with oriented edges, as explained. how many different rewrites are possible? More precisely, denote a node with a “+” if the port “2” is “in” and with a “-” if the port “2” is out. Then, how many rewrites from 2 nodes to 4 nodes, in the pattern DIST, are possible?
Doing it by hand is dangerous, so we better do it with a program. >We are looking for patterns of 4 nodes arranged like in DIST rewrites, each node being a “+” or a “-” node, with oriented edges, so that the 4 half edges (or external ports) have the same orientation as the corresponding ones of the LHS pattern made of 2 nodes (“+” or “-“). How many are they?
There are 4 cases, depending on the LHS nodes, which we denote by “+,+”, “-,-“, “+,-” and “-,+”.
I was surprised to learn from programs that theer are 386=16X23 possible RHS patterns, divided into 80=16X5, 80=16X5, 112=16X7 and 96=16X6 patterns.
While I can understand the 16X part, the 5,5,7,6 are strange to me. The 16X appears from the fact that for a node “+” we can permute the “1”,”2″ ports without changing the edges orientations, and similarly for a node “-” we can permute the “2” “3” ports with the same (lack of) effect.
Now let’s get further. We look now at the nodes which are decorated with elements of the group G, or say the group G acts somehow on the set of node types which has as many elements as G. We look for rewrites from LHS to RHS such that the decoration of the external ports does not change during the rewrites. This imposes strong restrictions on the choice of nodes (and it means something geometrically as well).
Not any possible rewrite can be accepted though. For example we reject rewrites with the property that the RHS contains a copy of the LHS. So each rewrite has associated a collection of rewrites which are inhibited by it. This will place restrictions on the collections of rewrites which we may choose for our calculus.
We reject also rewrites whose RHS contain a copy of the LHS of a rewrite we like, like the beta rewrite.
We reject rewrites which have the RHS made such that the external ports will all be “2”, because such a pattern will last forever during further rewrites.
Still when we look at what is left we see that we have about |G|X|G| LHS patterns and much more RHS choices, so there will still be many possible calculi.
We may look for symmetries, related to the action of G on the node types and we may ask: which is the most (or a most) symmetric collection and which will be a least symmetric (but maximal in number)?
Or we may say that the human mind is feeble and let the collections compete, by reducing a family of graphs. Take lambda calculus and some tests and let the possible collections compete. Take emergent algebras and some tests and do the same. Or even look for collections more fit for certain chosen tests from lambda calculus or others.
Who will win?