6. The simulator (BigraphSim)🔗

The executable counterpart of the bigraph library (Jensen and Milner, Bigraphs and mobile processes (revised), TR-580, 2004; Milner, The Space and Motion of Communicating Agents, 2009): bigraphs as finite, proof-free data, a matcher, and runs. The search for occurrences is untrusted; a checker proved sound against the library decides every occurrence it proposes, and completeness of the search is a separate theorem. Symbols are those of the Notation chapter. Every other result is in BigraphSim/: renumbering and tensor with an identity (Ren.lean, TensorId.lean), the tree notation (Term.lean), search and branching histories (Run.lean, History.lean), invariants and counting of controls (Prov.lean, Count.lean), and equality up to renumbering (Canon.lean); the completeness proof is in Logic/COcc*.lean; the composition operators on descriptions are in Logic/Compose.lean with their bridges to the library in Logic/ComposeBridge*.lean, and the condition that names are listed once is in Logic/FaceOk.lean.

1. 6.1. Bigraphs as data
2. 6.2. Composition operators on descriptions
3. 6.3. Occurrences and the checker
4. 6.4. The matcher
5. 6.5. Runs
6. 6.6. Erasing data, and image-finiteness
7. 6.7. Components and decomposition
8. 6.8. The explorer