Freedom sector of graphic lambda calculus

Yes, graphic lambda calculus has a freedom sector. Which means in that sector you can do anything you like (modulo some garbage, though). It’s yet not clear to me if this means a kind of universality property of graphic lambda calculus.

The starting point is the procedure of packing arrows explained in this post.  This procedure can be seen in the following way:


Here, the left and right void circles with the respective arrows represent: the one from the left is a generic out arrow which exits from a gate and the one from the right is a generic in arrow which enters in a gate.

This gives the following idea: replace the inputs and the outputs of the gates from graphic lambda calculus by the following graphs (the green wiggly arrow means “replace”):


For example, look how it’s done for the \curlywedge graph. Technically we define new macros, one for each elementary gate. Let’s call these macros “the free gates”.


These free gates define the free sector of the graphic lambda calculus, which consists all graphs made by free gates, along with the move of cutting or gluing arrows.

The free sector has inside a copy of the whole graphic lambda calculus, with the condition of adding a local move of elimination of garbage, which is the local move of elimination (goes only one way, not both) of any graph which is not made by free gates with at most, say, 100 arrows + gates. This move is needed, for example, for the case of emulating the graphic beta move with free gates, where we are left with some garbage consisting of one \lambda gate and one \curlywedge gate, seen as disconnected graphs.

3 thoughts on “Freedom sector of graphic lambda calculus”

Leave a Reply

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

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

Google photo

You are commenting using your Google 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 )

Connecting to %s