codedot

Previously, we found that a natural set of agent types for uniform memory consists of one binary agent (ξ), two unary ones (φ and ψ), and another one without any auxiliary ports (ν). As planned, let us try to construct a formal interaction system based exclusively on these agents.

In order to prove universality of an interaction system, it is sufficient to provide δ, γ, and ε in its terms. So far, we are not ready to simulate the whole system of interaction combinators. However, it appears that the following LISP-style interaction rules for {ξ, φ, ψ, ν} can at least result in simulation of the two rules γ >< γ and δ >< δ as well as ε >< α, α ∈ {γ, δ, ε}:

ξ[ξ(a, b), ξ(c, d)] >< ξ[ξ(a, c), ξ(b, d)];
φ[a] >< ξ[a, ν], ψ[a] >< ξ[ν, a];
ν >< ξ[ν, ν], ν >< φ[ν], ν >< ψ[ν].

Let us notice that behavior of ξ, φ, ψ, and ν agents is similar to that of cons, car, cdr, and nil in LISP, respectively. In lambda calculus, they can be represented as P₂, T, F, and λx.T. This is why we can name the agent types C («constructor»), L («left»), R («right»), and N («null») to ease notation. This way, the above rules result in the following reduction sequence which simulates δ annihilation (swapping L and R will in turn result in simulation of γ annihilation):