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.

Advertisements

6 thoughts on “Example: decorations of S,K,I combinators in simply typed graphic lambda calculus”

  1. I like this way of putting things! Re: Remark 1, the basic idea of typing-as-decorating-edges appears for example in Harry Mairson’s “From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple” (http://www.cs.brandeis.edu/~mairson/Papers/fsttcs02.pdf), but I haven’t seen this description of Hindley-Milner-style typing as trying to prove that a certain magma is freely-generated. My knowledge of the literature on unification is limited, though. It does remind me a bit of Philippe de Groote’s “An algebraic correctness criterion for intuitionistic proof nets” (http://www.loria.fr/~degroote/papers/lfcs97.pdf).

    1. Thank you for the comment and links! Will come back to this as soon as I read more. In this post there is only one constructor, but I can add the PAIR constructor as well, not in GLC, but in chemlambda.

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