Pullback and pushout squares in a special double category with connection
We present a categorical formulation of the rewriting of possibly cyclic term graphs, based on a variation of algebraic 2-theories. We show that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al. – but for the case of circular redexes , for which we propose (and justify formally) a different treatment. The categorical framework allows us to model in a concise way also automatic garbage collection and rules for sharing/unsharing and...
We interpret the collection of invertible bimodules as a groupoid and call it the Picard groupoid. We use this groupoid to generalize the classical construction of crossed products to what we call groupoid crossed products, and show that these coincide with the class of strongly groupoid graded rings. We then use groupoid crossed products to obtain a generalization from the group graded situation to the groupoid graded case of the bijection from a second cohomology group, defined by the grading...