Tag Archives: typed lambda calculus

Types and places

Simply typed graphic lambda calculus    is an added layer of decorations with types  over graphic lambda calculus, described by the following rules:

bckw_101

See  Example: decorations of S,K,I combinators in simply typed graphic lambda calculus   for the compatibility with simply typed lambda calculus.

Compared with the purity of graphic lambda calculus,  types (at least of this kind) seem a step back. However, graphic lambda calculus has also the emergent algebra sector, see  arXiv:1305.5786 [cs.LO] section 5, and also here the series

The starting point of the research subject on “computing with space” is to try to understand the computational content of emergent algebras arXiv:0907.1520 [math.RA]. This has lead to graphic lambda calculus, passing by decorated binary trees and decorated tangle diagrams, until the non-decorated formalism of graphic lambda calculus. This formalism is not yet completely finished; indeed, the extended graphic beta move,  arXiv:1302.0778 [math.GT], especially section 8,   which mixes the emergent algebra part with the purely logic part, is still in beta stage.

Therefore, I’m coming back to the decorated version and remark that, as concerns the two gates which appear in the emergent algebra sector, they can be decorated with places:

tagemerg_1

Places form an emergent algebra. Types form a free magma (for well decorated graphs).

Advertisements

Example: decorations of S,K,I combinators in simply typed graphic lambda calculus

Continuing from   Simply typed graphic lambda calculus  , let’s look at decorations for the S,K,I combinators.

We work in the lambda calculus sector of the graphic lambda calculus, which contains graphs in GRAPH which are associated to terms in lambda calculus by the algorithm explained here.

We want to decorate the arrows of such graphs, according to the rules given in the following figure:

bckw_101

Decorations are denoted by letters \sigma, \tau … or by letters a, b, c …. (what’s in a name?).  These decorations are called “types”. There is only one operation, called “\rightarrow“, which takes a pair of types (\sigma, \tau) and returns the type \sigma \rightarrow \tau.

In algebraic terms, here’s what is happening. We start with a graph in GRAPH and we decorate all it’s arrows with different letters from an alphabet (of types). Then we associate to it the magma with:

  • generators being the (decorations of the) arrows
  • relations being the ones from the rules of decorations given in the previous figure.

If the magma is free,  then we say that the graph is well typed. That means we can find a finite collection of types, with no relation between them, such that all arrows can be decorated by some element of the free magma generated by that collection of types.

_____________________

Remark 1:  Please, don’t let me reinvent the wheel.  Surely somewhere in the big work on type theory, there is something analogous done already. Just send me citations and I shall add them with due acknowledgements.

_____________________

Remark 2: This is exactly the same idea which is used in knot theory, where we associate to a knot diagram it’s knot  quandle. But with a twist: while in knot theory we look for quandles which are not free (we cannot eliminate all relations between the generators), in this simply typed lambda calculus we concentrate only on those graphs which have free magmas associated.  Please look at the right, lower corner from the previous figure, where is given the rule of decoration for the \varepsilon gate. (We are not going to use it in relation to the lambda calculus sector.)  As you see, this is compatible with the trivial quandle with the operation xy = y.

_____________________

Remark 3:  I am not going to enter or take the extremely interesting path of cartesian closed categories , basically because my strong bias against anything cartesian. The initial source of this bias comes from the experience with sub-riemannian geometry, where any application of cartesian ideas, like slicing a problem until it becomes 1 dimensional, then solving it by 1d calculus and analysis techniques, then reassembling the slices, leads always to “rigidity results”, which have the form: if you try then you arrive at a contradiction. Don’t get me wrong, there are amazing and extremely deep such results, but they are always in the form of a proof by contradiction.

Remark 4: The point of view from this simply typed graphic lambda calculus is surely related to the Hindley-Milner type system.

_____________________

Let’s see how this works for the I, K, S combinators, then for the \Omega combinator.

The procedure is the following:

  • we number the nodes of the graph (arbitrarily)
  • we put arbitrary, different labels on each arrow of the graph
  • we write the relations which appear from each node, according to the rules of decoration
  • finally, we examine the generated magma, to see if, eliminating some generators by using the relations, we can arrive to prove that’s a free magma.

In the next figure this is done for the I combinator (the identity) and for the K combinator.

bckw_103

We obtain the right types for identity and K combinators (there are no contexts, that’s for later). It was easy, they are “well typed” according to the definition from here.

Now, let’s look at the S combinator:

bckw_104

We have to work a bit, but not too much:

bckw_105

(For the convenience of the readers, I added in the figures the usual notations for combinators and types. )

We obtain again the right types for S as well as for the variables involved.

_____________________

Let’s try to decorate  the combinator \Omega = (\lambda x . xx) (\lambda x. xx).

bckw_106

We obtain the following magma presentation:

bckw_107

which cannot be free, because of relations (4) and (6). So \Omega is not well typed, exactly like in the simply typed lambda calculus.

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.