5.4. Scope🔗

Theorem5.4.1

uses 1used by 0✓L∃∀N

Every encoding, of an open or a closed process, obeys Jensen's scope rule for the binding signature \beta_\pi in which the datum port of an input or replicated input binds inward (scope: the node) and the port of a restriction binds outward (scope: the node's parent). For every X, \rho and P with \mathrm{fn}_\rho(P) \subseteq X,

\mathrm{ScopeRule}_{\beta_\pi}\bigl(\llbracket P \rrbracket_{X,\rho}\bigr) :

every port that shares a link with a binding port lies strictly below the binder's scope, and no inner name is on that link (Jensen's Def 4.20, all names global). Moreover every binding port of the encoding lies on an edge.

Rests on not audited: Bg.BindSig.binds, NameSet.Elt.

Lean code for Theorem5.4.1●3 declarations

theoremdefined in Pi/Scope.lean

complete

theorem agentπ_scope (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc)
  (hp : NamesIn X.names ρ p) : Bg.Abstract.ScopeRule piBind ⟦p⟧

theorem agentπ_scope (X : NameSet Nat)
  (ρ : Nat → Nat) (p : Proc)
  (hp : NamesIn X.names ρ p) :
  Bg.Abstract.ScopeRule piBind ⟦p⟧

**Every π agent obeys Jensen's scope rule**, open or closed, as an
abstract bigraph: whichever representative is taken.

theoremdefined in Pi/Scope.lean

complete

theorem encπ_binder_edge (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc)
  (hp : NamesIn X.names ρ p) (v : (encπ X ρ p hp).V)
  (i : Fin (sig.ar ((encπ X ρ p hp).ctrl v)))
  (hb : piBind.binds ((encπ X ρ p hp).ctrl v) i = true) :
  ∃ e, (encπ X ρ p hp).link (Sum.inr ⟨v, i⟩) = Sum.inl e

theorem encπ_binder_edge (X : NameSet Nat)
  (ρ : Nat → Nat) (p : Proc)
  (hp : NamesIn X.names ρ p)
  (v : (encπ X ρ p hp).V)
  (i :
    Fin (sig.ar ((encπ X ρ p hp).ctrl v)))
  (hb :
    piBind.binds ((encπ X ρ p hp).ctrl v)
        i =
      true) :
  ∃ e,
    (encπ X ρ p hp).link
        (Sum.inr ⟨v, i⟩) =
      Sum.inl e

…and every binder of its encoding is on an edge: bound links are
closed.

defdefined in Pi/Scope.lean

complete

def piBind : Bg.BindSig sig

def piBind : Bg.BindSig sig

**Jensen's binding signature for π**: the datum port of an input binds
inward, a restriction's port outward.