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:

type_lambda_appl

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

type_lambda

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

type_appl

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.

What about the beta move?

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]

type_beta_1

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]

type_beta_2

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]

type_beta_3

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.

________________________________________________________

 

Advertisements

3 thoughts on “Actors as types in the beta move, tentative”

  1. I have considered systems where the Actors are called Interpreters, or Interpretors if one needs a distinctive term.

    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}.

    1. Thank you, can you send me a reference (file or link)?
      In the first linked post is defined a magma of types associated to a graph. If the magma is free then the graph is well typed. But if the magma is not free then nevertheless it is an interesting object, like the quandle associated to a knot diagram.
      Here in this post I just pretend that actors are like types in order to justify one behaviour of GLC actors, the one which allows to perform beta reduction as an interaction between actors. There is a part which will follow soon about the DIST move, also like an interaction of actors. (and the real story is that the treatment of DIST made me change the actors and their behaviours in some details because now the ports, and not the nodes, belong to actors; Louis has something perhaps related, or influencing this, because of a formalism of him which works with graphs as built from arrows only)
      What is strange though is that if we take seriously that actors are a bit like types, because types here are only local decorations (manifested by the fact that there is no constraint on the generated magma to be free) then actors also have only local meaning.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s