TY - RPRT
T1 - Axiomatizing Binding Bigraphs
AU - Damgaard, Troels Christoffer
AU - Birkedal, Lars
PY - 2005/3
Y1 - 2005/3
N2 - Extending the result for pure bigraphs given in [Mil04], we axiomatize static congruence for binding bigraphs as described in [Chapter 11, HM04], 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.
AB - Extending the result for pure bigraphs given in [Mil04], we axiomatize static congruence for binding bigraphs as described in [Chapter 11, HM04], 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.
M3 - Report
T3 - IT University Technical Report Series
BT - Axiomatizing Binding Bigraphs
PB - IT-Universitetet i København
CY - Copenhagen
ER -