Notes for gamification of chemlambda

Here are some obvious notes  which are filed here about chemlambda graphs in GraphML.  Hope they may be used with … ? … why not Liviz.js  to get quick something OS to play with.

In the previous post The Quantomatic GUI may be useful for chemlambda (NTC vs TC, III) is mentioned the quantomatic gui, which can easily do all this, but is not free. Moreover, the goals for the gui proposed here are  more modest and easily attainable. Don’t care about compatibility with this or that notion from category theory because our approach is different and because the gui is just step 0. So any quick and dirty, but effective code will do, I believe.

______________________________

Recall the idea: gamification of chemlambda.

  • get quick a chemlambda GUI, as described  in  A user interface for GLC  and use it, with a collection of predefined goals to make a gamification of chemlambda.
  • obviously that means choosing a format for representing the graphs and moves, many variants here, in this post is described such a choice — GraphML. The work consists into transforming the definitions of graphs and moves into a chosen format.
  • the various buttons and options from the post describing the gui are simple scripts, perhaps in javascript?  of the kind: find and replace predefined patterns by others, all involving up to 4 nodes and 8 arrows, so almost a no brainer, consisting in writing into the chosen format which are the patterns (i.e. the configurations of at most 4 nodes and 8 arrows ) which are involved in the chemlambda moves and which are the replacement rules (i.e. transforming the definition of chemlambda moves into code)
  • open the possibility to define arbitrary patterns (named here “macros”) and arbitrary moves (named here “macro moves”)
  • transform into code the algorithm described in Conversion of lambda calculus terms into graphs , with the care to use instead chemlambda. This is good for having a button for importing lambda terms into chemlambda  easily.
  • with all this done, pick a visualization tool which is open, looks good and  is easy to use, like the one previously mentioned.
  • write some scripts for converting to and from GraphML (or whatever other choice one likes) to  the input of the viz tool.
  • pick some examples, transform them into challenges and make public the game.

___________________________

For those with a  non functional right hemisphere, here is the GraphML description of chemlambda graphs and what would mean to do a move.

I use this source for GraphML.

A chemlambda graph is  any graph which is directed, with two types of 3-valent nodes and one type of  1-valent node, with the nodes having some attributes. [For mathematicians, is an oriented graph made by trivalent, locally planar nodes, and by some 1-valent nodes, with arrows which may have free starts or free ends, or even loops.]

Moreover, we accept arrows (i.e. directed edges) with free starts, free ends, or both, or with start=end and no node (i.e. loops with no node). For all those we need, in GraphML, to use some “invisible” nodes [multiple variants here, only one is described.]

Here are the trivalent, locally planar nodes:

 

  • application node

<node id=”n0″ parse.indegree=”2″ parse.outdegree=”1″>
<data key=”d0″>green</data>
<port name=”middle_out”/>
<port name=”left_in”/>
<port name=”right_in”/>
</node>

  • fanin node

<node id=”n3″ parse.indegree=”2″ parse.outdegree=”1″>
<data key=”d0″>red</data>
<port name=”middle_out”/>
<port name=”left_in”/>
<port name=”right_in”/>
</node>

  • lambda node

<node id=”n1″ parse.indegree=”1″ parse.outdegree=”2″>
<data key=”d0″>red</data>
<port name=”middle_in”/>
<port name=”left_out”/>
<port name=”right_out”/>
</node>

  • fanout node

<node id=”n2″ parse.indegree=”1″ parse.outdegree=”2″>
<data key=”d0″>green</data>
<port name=”middle_in”/>
<port name=”left_out”/>
<port name=”right_out”/>
</node>

  • termination node

<node id=”n4″ parse.indegree=”1″ parse.outdegree=”0″>
<data key=”d0″>term</data> </node>

(where “term” denotes a color we agree to use for the termination node, in xfig made drawings this node  appears like this  –>–|  )
  • two invisible nodes 1 valent

<node id=”n5″ parse.indegree=”0″ parse.outdegree=”1″>
<data key=”d0″>invisible</data> </node>

<node id=”n6″ parse.indegree=”1″ parse.outdegree=”0″>
<data key=”d0″>invisible</data> </node>

(where “invisible” should be something to  agree to use)

  • invisible node 2 valent

<node id=”n7″ parse.indegree=”1″ parse.outdegree=”1″>
<data key=”d0″>invisible</data> </node>

Uses of  invisible nodes:

  • in chemlambda graphs we admit arrows which start from one of the 3 valent nodes but the end is free. Instead of the free end we may use  the invisible node  with id=”n6″ from before.

<edge source=”n101″ target=”n6″/>

  • There are also accepted arrows which end in a 3 valent node or in a 1 valent termination node, but their start is free. For those we may use the invisible node with id=”n5″ from before.

<edge source=”n5″ target=”n102″/>

  • There are accepted arrows with free starts and ends, so we represent them with the help of invisible nodes with id=”n5″ and id=”n6″.

<edge source=”n5″ target=”n6″/>

  • Finally, we accept also loops, with no nodes, these are represented with the help of the 2 valent invisible nodes line the one with id=”n7″

<edge source=”n7″ target=”n7″>

____________________________________________

 

Examples:
(a) – recognize pattern for beta move
(b) – perform (when called) the beta move

  • (a) recognize pattern for beta move.

– input is a chemlambda graph (in GraphML)

– output is the same graph and some supplementary file of annotations of the graph.

  • This program looks in the input graph for all patterns where the beta move can be applied.  This pattern looks like this in the GraphML convention:

<node id=”n101″ parse.indegree=”2″ parse.outdegree=”1″>
<data key=”d0″>green</data>
<port name=”middle_out”/>
<port name=”left_in”/>
<port name=”right_in”/>
</node>
<node id=”n102″ parse.indegree=”1″ parse.outdegree=”2″>
<data key=”d0″>red</data>
<port name=”middle_in”/>
<port name=”left_out”/>
<port name=”right_out”/>
</node>
<edge source=”n102″ target=”n101″ sourceport=”right_out” targetport=”left_in”/>
<edge source=”n106″ target=”n102″ sourceport=”???_1″ targetport=”middle_in”/>
<edge source=”n102″ target=”n103″ sourceport=”left_out” targetport=”???_2″/>
<edge source=”n105″ target=”n102″ sourceport=”???_3″ targetport=”right_in”/>
<edge source=”n101″ target=”n104″ sourceport=”middle_out” targetport=”???_4″/>

Here “???_i” means any port name.

If such a pattern is found, then the collection of id’s (of edges and nodes) from it is stored in some format in the annotations file which is the output.

  • (b) perform (when called) the beta move

When called, this program takes as input the graph and the annotation file for beta moves pattern and then wait for the user to pick one of these patterns (i.e. perhaps that the patterns are numbered in the annotation file, the user interface shows then on screen and the user clicks on one of them).

When the instance of the pattern is chosen by the user, the program erases from the input graph the pattern (or just comments it out, or makes a copy first of the input graph and then works on the copy, …) and replaces it by the following:

<edge source=”n106″ target=”n104″ sourceport=”???_1″ targetport=”???_4″/>
<edge source=”n105″ target=”n103″ sourceport=”???_3″ targetport=”???_2″/>

It works only when the nodes n101 or n102 are different than the nodes  n103 ,n104, n105, n106,  because if not then when erased leads to trouble. See the post Graphic beta move with details.

As an alternative one may proceed by introducing invisible nodes which serve as connection points for the arrows from n106 to n104 and n101 to n103, then erase the nodes  among n101, n102 which are not among  n103, n104, n105, n106 .

___________________________________________

A concrete example:

reg_1

  • The input graph is the one from the first row of the figure:

<node id=”n1″ parse.indegree=”0″ parse.outdegree=”1″>
<data key=”d0″>invisible</data>
<port name=”out”/>
</node>
<node id=”n2″ parse.indegree=”0″ parse.outdegree=”1″>
<data key=”d0″>invisible</data>
<port name=”out”/>
</node>
<node id=”n3″ parse.indegree=”1″ parse.outdegree=”0″>
<data key=”d0″>invisible</data>
<port name=”in”/>
</node>
<node id=”n4″ parse.indegree=”1″ parse.outdegree=”0″>
<data key=”d0″>invisible</data>
<port name=”in”/>
</node>

[comment: these are the four free ends of arrows which are numbered in the figure by “1”, … , “4”.   So you have a graph with two inputs and two outputs,  definitely not a graph of a  lambda term! ]

<node id=”n105″ parse.indegree=”2″ parse.outdegree=”1″>
<data key=”d0″>green</data>
<port name=”middle_out”/>
<port name=”left_in”/>
<port name=”right_in”/>
</node>
<node id=”n106″ parse.indegree=”2″ parse.outdegree=”1″>
<data key=”d0″>green</data>
<port name=”middle_out”/>
<port name=”left_in”/>
<port name=”right_in”/>
</node>
<node id=”n108″ parse.indegree=”2″ parse.outdegree=”1″>
<data key=”d0″>green</data>
<port name=”middle_out”/>
<port name=”left_in”/>
<port name=”right_in”/>
</node>

[comment: these are 3 application nodes]

<node id=”n107″ parse.indegree=”1″ parse.outdegree=”2″>
<data key=”d0″>red</data>
<port name=”middle_in”/>
<port name=”left_out”/>
<port name=”right_out”/>
</node>
<node id=”n109″ parse.indegree=”1″ parse.outdegree=”2″>
<data key=”d0″>red</data>
<port name=”middle_in”/>
<port name=”left_out”/>
<port name=”right_out”/>
</node>
<node id=”n110″ parse.indegree=”1″ parse.outdegree=”2″>
<data key=”d0″>red</data>
<port name=”middle_in”/>
<port name=”left_out”/>
<port name=”right_out”/>
</node>

[comment: these are 3 lambda abstraction nodes]

<edge source=”n1″ target=”n105″ sourceport=”out” targetport=”right_in”/>
<edge source=”n107″ target=”n105″ sourceport=”left_out” targetport=”left_in”/>
<edge source=”n105″ target=”n106″ sourceport=”middle_out” targetport=”left_in”/>

<edge source=”n2″ target=”n106″ sourceport=”out” targetport=”right_in”/>
<edge source=”n106″ target=”n107″ sourceport=”middle_out”
targetport=”middle_in”/>
<edge source=”n107″ target=”n108″ sourceport=”right_out” targetport=”left_in”/>

<edge source=”n108″ target=”n109″ sourceport=”middle_out”
targetport=”middle_in”/>
<edge source=”n110″ target=”n108″ sourceport=”right_out” targetport=”right_in”/>
<edge source=”n109″ target=”n110″ sourceport=”right_out”
targetport=”middle_in”/>

<edge source=”n109″ target=”n4″ sourceport=”left_out” targetport=”in”/>
<edge source=”n110″ target=”n3″ sourceport=”left_out” targetport=”in”/>

  • This graph reduces via 3 beta reductions to

<node id=”n1″ parse.indegree=”0″ parse.outdegree=”1″>
<data key=”d0″>invisible</data>
<port name=”out”/>
</node>
<node id=”n2″ parse.indegree=”0″ parse.outdegree=”1″>
<data key=”d0″>invisible</data>
<port name=”out”/>
</node>
<node id=”n3″ parse.indegree=”1″ parse.outdegree=”0″>
<data key=”d0″>invisible</data>
<port name=”in”/>
</node>
<node id=”n4″ parse.indegree=”1″ parse.outdegree=”0″>
<data key=”d0″>invisible</data>
<port name=”in”/>
</node>

<edge source=”n1″ target=”n3″ sourceport=”out” targetport=”in”/>
<edge source=”n2″ target=”n4″ sourceport=”out” targetport=”in”/>

____________________________________________

For this choice which consists into using invisible nodes, a new program is needed (which may be useful for other purposes, later)

(c) arrow combing

The idea is that a sequence of arrows  connected via 2-valent invisible nodes should count as an arrow in a chemlambda graph.

So this program does exactly this: if n1001 is different than n1002  then replaces the pattern

<node id=”n7″ parse.indegree=”1″ parse.outdegree=”1″>
<data key=”d0″>invisible</data>
<port name=”in”/>
<port name=”out”/>
</node>
<edge source=”n1001″ target=”n7″ sourceport=”???_1″ targetport=”in”/>
<edge source=”n7″ target=”n1002″ sourceport=”out” targetport=”???_2″/>

by

<edge source=”n1001″ target=”n1002″ sourceport=”???_1″ targetport=”???_2″/>

 

_________________________________________

 

Advertisements

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