Simply typed graphic lambda calculus

Let me prepare the path towards discussing about types and spaces. In this post is a first proposal for a simply typed graphic lambda calculus, which is compatible with simply typed lambda calculus.

The leading idea is:

types are decorations, in the same way as elements of an emergent algebra are decorations.

Motivation: Remember that emergent algebras appeared as an effort to understand the formalism of decorated binary trees which appeared first in Dilatation structures I. Fundamentals, section 4. Various efforts have been spent for this, as witnessed in Computing with space, sections 3-6,  until finally arriving to the formalism of graphic lambda calculus, as exposed in  arXiv:1305.5786 [cs.LO] . The main “trick” of graphic lambda calculus is that it eliminates variables, therefore it eliminates decorations of graphs!

So, the program is that now we go back from the other side, logic, where types are decorations, as you will see, in order to connect with emergent algebras, which deal with the problem of describing spaces in a purely relational way, without any appeal to points (well, in the graphic lambda calculus formalism).

Interesting thing will appear, surely.

__________________________

In this version of simply typed lambda calculus we introduce types (just a bag of names  \sigma, \tau, … ), with one operation, denoted by \rightarrow.  We use types as decorations of arrows of graphs in GRAPH, according to the following decoration rules:

bckw_101

 

Remark how the decoration of the \varepsilon gate corresponds to the trivial quandle.

I don’t claim that I can decorate any graph in GRAPH by using these rules.  But when I can do it, then under any move from graphic lambda calculus the decoration remains compatible with the decoration rules. Indeed, this is proved in the next figure:

bckw_102

The pruning and the FAN-OUT moves are trivially preserving decorations.

__________________________

In another post we shall see why is this compatible with the simply typed combinatory logic.

Advertisements

2 thoughts on “Simply typed graphic lambda calculus”

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