Combinators and zippers

The goal of this post is to show how to use graphic lambda calculus for understanding the SKI combinators. For the graphs associated to the SKI combinators see this post.

__________

UPDATE: See also the post “Combinators and stickers“.

__________

Zippers have been introduced here.  In particular, the first three zippers are depicted in the following figure.

zipper_2

The combinator I has the expression I = \lambda x . x and it satisfies the relation I A \rightarrow A, where \rightarrow means any combination of beta reduction and alpha renaming (in this case is just one beta reduction: I A = \left( \lambda x . x \right) A \rightarrow A).

In the next figure it is shown that the combinator I  (figured in green) is just a half of the zipper_1, with an arrow added (figured in blue).

zipper_3

When you open the zipper you get A, as it should.

The combinator K = \lambda xy.x satisfies K A B = (KA)B \rightarrow A. In the next figure the combinator K (in green) appears as half of the zipper_2, with one arrow and one termination gate added (in blue).

zipper_4

When you open the zipper you obtain a pair made by A   and B which gets the termination gate on top of it. GLOBAL PRUNING sends B to the trash bin.

Finally, the combinator S = \lambda xyz. ((xz)(yz)) satisfies SABC = ((SA)B)C \rightarrow (AC)(BC). The combinator S (in green) appears to be made by half of the zipper_3, with some arrows added and also with a “diamond” added (all in blue). Look well at the “diamond”, it is very much alike the emergent sum gate from this post.

zipper_5

Advertisements

5 thoughts on “Combinators and zippers”

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