Variable binding, symmetric monoidal closed theories, and bigraphs

TL;DR

This paper explores using symmetric monoidal closed (SMC) structures to represent syntax with variable binding, especially for linear languages, and applies this to bigraphs to offer an alternative categorical framework.

Contribution

It introduces a novel approach to modeling variable binding syntax using SMC theories and applies it to bigraphs, providing an alternative categorical perspective.

Findings

SMC theories can effectively model variable binding syntax.

Application to bigraphs yields an alternative categorical framework.

Comparison shows differences between original and new bigraph categories.

Abstract

This paper investigates the use of symmetric monoidal closed (SMC) structure for representing syntax with variable binding, in particular for languages with linear aspects. In our setting, one first specifies an SMC theory T, which may express binding operations, in a way reminiscent from higher-order abstract syntax. This theory generates an SMC category S(T) whose morphisms are, in a sense, terms in the desired syntax. We apply our approach to Jensen and Milner's (abstract binding) bigraphs, which are linear w.r.t. processes. This leads to an alternative category of bigraphs, which we compare to the original.