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

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

- Dictionary from emergent algebra to graphic lambda calculus (I)
- Dictionary from emergent algebra to graphic lambda calculus (II)
- Dictionary from emergent algebra to graphic lambda calculus (III)

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*:

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

## One thought on “Types and places”