Perhaps the post When priority matters gives a false impression. I want to dispel that right away.
In that post we see two possible reductions, depending on the PRIORITY CHOICE, either BETA>DIST or DIST>BETA.
In the case BETA>DIST the reduction stops quickly.
On the contrary, in the case DIST>BETA the reduction does not stop, because it enters in a cyclic process which produces an unbounded number of bubbles (i.e. loops graphical elements).
Moreover, we start from the g-pattern form of the combinator (Lx.xx)(Lx.xx).
Or, this may lead to the false impression that somehow this has anything to do with the choice between normal order reduction and applicative order reduction from lambda calculus.
Yes, because a standard example of the difference between these reduction strategies is the following one.
Let’s denote by Omega the combinator (Lx.xx)(Lx.xx). Consider then the term
Under the normal order reduction this term suffers one beta reduction
(Lx.z) Omega –BETA–> z
and that’s all, the reduction stops.
On the contrary, under the applicative order reduction strategy, the reduction never stops, because we first try to reduce Omega, leading to a cycle
(Lx.z) Omega –BETA–> (Lx.z) Omega
The question is: is there any connection between these two phenomena?
- is the sequential chemlambda reduction with BETA>DIST like normal order reduction in lambda calculus?
- is the sequential chemlambda reduction with DIST>BETA like applicative order reduction?
No, not the slightest.
In order to prove this I shall reduce in chemlambda with the sequential strategy the g-pattern which represents the term (Lx.z) Omega. Let’s see what happens, but first let me remind what we do.
The sequential strategy is described by the following algorithm. I write it again because the g-pattern of Lx.z brings a termination node “T”, therefore we have to consider also the local pruning moves LOC-PR.
The algorithm of the sequential reduction strategy is this. At each reduction step do the following:
- if no LEFT patterns of the moves BETA, DIST, FAN-IN and LOC-PR are present in the g-pattern, then stop, else
- identify the LEFT patterns of the moves BETA, DIST, FAN-IN and LOC-PR. If there is a graphical element which is part of two distinct patterns then apply a PRIORITY CHOICE
- apply the moves from LEFT to RIGHT
- apply the COMB moves until no Arrow element
can be eliminated
The PRIORITY CHOICE means a predefined choice between doing one of the two moves in conflict. The conflict may be between BETA and DIST, between BETA and LOC-PR or between DIST and LOC-PR.
In the following we shall talk about the PRIORITY CHOICE only if needed.
In the first picture we see, in the upper side, the g-pattern which represents the term (Lx.z) Omega, then the first reduction step.
I kept the same names for the ports from the last post and I added new names for the ports of the new graphical elements.
First, remark that the g-pattern which represents (Lx.z) is
I named by “z” one of the ports of the lambda node L, which would correspond to the variable z of the term Lx.z. But recall that chemlambda does not use variable names, so the name “z” is there only by my choice of names for the port variables, could be anything instead (which was not used before in one of the g-pattern’s ports).
Then, A[n1,1,0] corresponds to the application of something linked to the port n1 (namely the g-pattern of (Lx.z), i.e. L[z,n2,n1] T[n2]) to something linked to the port 1 (i.e. the g-pattern of Omega, which was discussed in the post “When priority matters”).
Nice! What happened?
- there is an Arrow element which does not disappear, Arrow[z,0]. This is something which corresponds to the g-pattern of z, seen as lambda calculus term.
- and there is another g-pattern, disconnected from that Arrow[z,0] graphical element.
So, in a sense, this looks like the result of the normal order reduction, but no priority choice was involved!
However, the chemlambda sequential reduction continues, like explained in the picture of the 2nd reduction step.
OK, the Arrow[z,0] still exists after the reduction step, and a LOC-PR move appear.
Let’s see what happens in the 3rd reduction step.
The reduction stops here. There is nothing more to do, according to the sequential reduction strategy.
Differently from the reduction of Omega alone, explained in the previous post, this time there is NO PRIORITY CHOICE NEEDED.
Ergo, the priority choice has nothing to do here. The sequential chemlambda reduction of the g-pattern corresponding to (Lx.z) Omega stops after 3 steps, no matter which was the PRIORITY CHOICE made before the start of the computation.