Axiomatizing Binding Bigraphs (revised)
TR-2005-71, Authors: Troels C. Damgaard and Lars Birkedal
Axiomatizing Binding Bigraphs (revised)
November 2005
Abstract
Extending Milners work on pure bigraphs, we axiomatize static congruence for binding bigraphs and prove that the theory generated is complete. In doing so, we also define a normal form for binding bigraphs, and prove that the four forms are unique up to certain isomorphisms. Compared with the axioms stated by Milner for pure bigraphs, we have extended the set with 5 axioms concerned with binding; and as our ions have names on both faces, we have two axioms -- handling inner and outer renaming. The remaining axioms are transfered straightforwardly.
Technical report TR-2005-71 in IT University Technical Report Series, October 2005.
Available as PDF.