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

One thought on “Types and places”

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