Actors as types in the beta move, tentative

Recall the posts about types as decorations of a GLC graph?  Like this one

Example: decorations of S,K,I combinators in simply typed GLC

In the chemlambda version, the decoration with types for the lambda and application graphical elements is this:

or with g-patterns:

L[x:b, y:a, z:a->b]

A[x:a->b, y:a, z:b]

Recall also that there is a magma associated to any graph (or g-pattern) which is easy to define. If the magma is free then we say that the g-pattern is well typed (not that we need “well” further).

Let’s mix this with actors. We make the attribution of the port variables of a g-pattern to actors (id’s) and we write  that the port variable x belongs to the actor a  like this

x:a

I don’t want to define an operation -> for actors id’s, like if they are types. Instead I shall use the Arrow graphical element and the COMB move (see the moves of chemlambda in terms of g-patterns here).

Here is a COMB move, a bit modified:

L[x:b, y:a, z:d]     –COMB–>  L[x:b, y:a, u:a] Arrow[u:b, z:d]

which says something like

:d should be  :a->:b

The same for the application

A[z:d, v:a, w:b]  –COMB–>  Arrow[z:d, s:a] A[s:b , v:a, w:b]

which says something like

:d should be :a->:b

which, you agree, is totally compatible with the decorations from the first figure of the post.

Notice the appearance of port variables u:a, u:b  and s:a, s:b, which play the role a->b.

We allow the usual COMB moves only if the repeating variables have the same actors.

The LEFT g-pattern of the beta move is, say with actors:

L[x:a, y:d, z:c]  A[z:c, v:b, w:e]

Apply the two new COMB moves;

L[x:a, y:d, z:c]  A[z:c, v:b, w:e]

–2 COMB–>

L[x:a, y:d, u:d]

Arrow[u:a, z:c]  Arrow[z:c, s:b]

A[s:e , v:b, w:e]

An usual COMB move applies here:

L[x:a, y:d, u:d]

Arrow[u:a, z:c]  Arrow[z:c, s:b]

A[s:e , v:b, w:e]

<–COMB–>

L[x:a, y:d, u:d]

Arrow[u:a, s:b]

A[s:e , v:b, w:e]

and now the new beta move would be:

L[x:a, y:d, u:d]

Arrow[u:a, s:b]

A[s:e , v:b, w:e]

–BETA–>

Arrow[x:a, w:e]

Arrow[v:b, y:d]

This form of the beta move resembles with the combination of CLICK and ZIP from zipper logic.

Moreover the Arrow elements could be interpreted as message passing.

________________________________________________________

An interpreter $\mathcal{J}$ interprets a formal language of syntactic forms relative to its own syntactic form, which defines a functional type.
An interpreter $\mathcal{J}$ may be identified with a functional type expression $\mathcal{J}$ and this may be thought of as the simplest expression that $\mathcal{J}$ can interpret as having a meaning. Every syntactic form falling short of $\mathcal{J}$ is assigned an error type relative to $\mathcal{J}.$