I am updating the paper on almost daily. It is the first time when I am doing such a thing, it is maybe interesting to see what comes out of this way of writing.
The last addition is something I was thinking about for a long time, something which is probably well known in some circles, but maybe not. It is about eliminating variable (names) from such a calculus. This has been done in several ways, here is another (or the same as a previous one?).
The idea is simple. let be any term and a variable. Look at the syntactic tree of , then glue to all leaves decorated by the leaves of a tree with nodes consisting of FAN-OUT gates.
Further on I shall identify syntactic trees with terms. I shall add to such trees a new family
(of trees), constructed from the elementary tree depicted at (a) in the next figure. At (b) we see an example of such a tree. We consider also the trivial tree (c).
We have to think about such trees as devices for multiplying the occurences of a variable. I call them FAN-OUT trees. All these trees, with the exception of the trivial one (c), are planar binary trees. We shall add the following rule of associativity:
(ASSOC) any two FAN-OUT trees with the same number of leaves are identified.
This rule will be applied under the following form: we are free to pass from a FAN-OUT tree to an equivalent one which has the same number of leaves. The name “associativity” comes from the fact that a particular instance of this rule (which deserves the name “elementary associativity move”) is this:
With the help of these FAN-OUT trees we shall replace the multiple occurences of a variable by such trees. Let us see what become the rules of calculus by using this notation.
conversion is no longer needed, because variables have no longer names. Instead, we are free to graft usual trees to FAN-OUT trees. This way, instead of terms we shall use “neurons”.
Definition: The forgetful form (b) of a syntactic tree (a) (of a term) is the tree with the name variables deleted.
A neuron is the result of gluing the root of a forgetful form of a syntactic tree to the root of a FAN-OUT tree, like in the following figure.
The axon of the neuron is the FAN-OUT tree. The dendrites of the neuron are the undecorated edges of the forgetful form of the syntactic tree. A dendrite is bound if it is a left edge pointing to a node decorated by . For any bound dendrite, the set of dependent dendrides are those of the sub-tree starting from the right edge of the node (where the bound dendrite is connected via a left edge), which are moreover not bound. Otherwise a dendrite is free. The soma of the neuron is the forgetful form of the syntactic tree.
Substitution. We are free to connect leaves of axons of neurons with dendrites of other neurons.
In order to explain the substitution we have to add the following rule:
(subst) The leaves of an axon cannot be glued to more than one bounded dendrite of another neuron. If a leaf of the axon of the neuron is connected to a bound dendrite of the neuron , then it has to be the leftmost leaf of the axon of . Moreover, in this case all other leaves of which are connected with have to be connected only via dendrites which are dependent on the mentioned bound dendrite of , possibly via adding leaves to the axon of by using (assoc).
Substitution is therefore assimilated to connecting neurons.
New (beta*). The rule (beta*) takes the following graphical form. In the next figure appear only the leaf of the neuron connecting to the node (the other leaves of the axon of not drawn) and only some of the dendrites depending on the bound one relative to the node which is figured.
The neuron may have other dendrites, not figured. According to the definition of the neuron, together with the node and adiacent edges form a bigger neuron. Also figured is another leaf of the axon of the neuron , which may point to another neuron. Finally, in the RHS, the bound dendrite looses all dependents.
Important remark. Notice that there may be multiple outcomes from (subst) and (beta*)! Indeed, this is due to the fact that connections could be made in several ways, by using all or only of part of the dependent dendrites. Because of that, it seems that this version of the calculus is richer than the previous one, but I am not at all sure if this is the case.
Another thing to be remarked is that the “” sign in this version of these rules is reflexive and transitive, but not symmetric. Previously the “$ latex =$” sign was supposed to be symmetric.
(R1) That is easy, we use the emergent algebra gates:
(R2) Easy as well:
The rules (ext1), (ext2) take obvious forms.
Therefore, if we think about computation as reduction to a normal form (if any), in this graphical notation with “neurons”, computation amounts to re-wiring of neurons or changing the rewiring inside the soma of some neurons.
Variables dissapeared, with the price of introducing FAN-OUT trees.
As concerns the remark previously made, we could obtain a calculus which is clearly equivalent with by modifying the definition of the neuron, in this way.
In order to clearly specify which are the dependent dendrites, we could glue to any bound dendrite a FAN-OUT tree, such that the leaves of this tree connect again with a set of dependent dendrites of the same neuron. In this way, substitution and (beta*) will amount of erasing such a FAN-OUT tree and then perform the moves, as previously explained, but using this time all the dependent dendrites which were connected to the bound dendrite by the erased tree.