III Mobile Processes

Theorem 1 (Congruent processes are one agent, and conversely). Every law of structural congruence is an isomorphism of shapes, including Jensen's exchange of two restrictions, νxνy P ≡ νyνx P, where the two binder nodes simply trade places. The law was added after a check showed it is needed: without it νxνy x̄y and νyνx x̄y are one agent but not congruent (Pi/Converse.lean). So is substitution: the shape of P with c for index k is the shape of P with index k made c (substπ, an isomorphism defined by recursion on the process).

theorem sc_soundπ {X : NameSet Nat} {ρ : Nat → Nat} {p q : Proc} (h : SC p q)
    (hp : NamesIn X.names ρ p) : agentπ X ρ p hp = agentπ X ρ q (Pi.NamesIn.of_sc h hp)

Conversely, for closed processes, one agent means congruent. Equal agents have isomorphic shapes, since no edge of an encoding is idle and no port of a closed process reaches past its binders; and isomorphic shapes are congruent processes, open or closed, so structural congruence is exactly isomorphism of shapes. The proof is an induction on the number of nodes: a binder at the top is brought out to the outermost restriction on both sides and removed, and otherwise a top component is split off on both sides and the parts compared. The exchange law is used there, once; without it the converse fails, as above. Closedness is needed: a port on a bound index and a port on the free name the environment gives that index are linked alike.

theorem sc_iffπ {X : NameSet Nat} {ρ : Nat → Nat} {p q : Proc} (hp : Closed p)
    (hq : Closed q) (hpX : NamesIn X.names ρ p) (hqX : NamesIn X.names ρ q) :
    agentπ X ρ p hpX = agentπ X ρ q hqX ↔ SC p q

Theorem 2 (Soundness). Every reduction of every process is a reaction of the encodings under the two rules, for every name set and environment.

theorem red_soundπ {p q : Proc} (h : Red p q) : ∀ (X : NameSet Nat) (ρ : Nat → Nat),
    (hp : NamesIn X.names ρ p) →
      React piRules (agentπ X ρ p hp) (agentπ X ρ q (NamesIn.of_red h hp))

As in Chapter II, the parameter keeps its edges, so a component whose dangling indices are named by the environment is the rule plugged with its parts. Substitution meets the reactum in one lemma: a received body, copied and its local name wired to the datum, is the body with the datum substituted.

theorem plugRef_ren_subst {m k l : Nat} (R : RShape sig m k l) (nm : Fin k → Nat) (zn : Fin l → Nat)
    (hzn : ∀ s t, zn s = zn t → s = t) {X : NameSet Nat} (hX : ∀ s, zn s ∉ X.names)
    (z : Nat) (g : Nat → Nat) (hg : ∀ n ∈ X.names, g n = n) (s₀ : Fin l) (hgz : g z = zn s₀)
    (t : Fin k) (hin : R.inner s₀ = .inr t) (y : Chan) (ρ : Nat → Nat) (hy : nm t = y.name ρ)
    {E F : Type} (f : E → F) (r : Ref E) (hr : ∀ n ∈ r.fv ρ 1, n ∈ X.names) :
    R.plugRef nm zn (((r.cls (consEnv z ρ)).mapE f).ren g) =
      (((r.subst 0 y).cls ρ).mapE f).mapE Sum.inl

Theorem 3 (Occurrence determinacy for rules that pass names). Two instances of a rule in context, equivalent by a map that fixes the rule's nodes, have equivalent reactums. The contexts are any, the parameters any binding-discrete ones. Three properties of the redex are assumed, and both π redexes have them: every edge of the rule is reached by a port of the rule, so the map fixes it; every inner name reaches an edge of the rule, different ones different edges, so a parameter port on an inner name goes to one on the same inner name; and every slot is reached by a port of the rule, so the contexts' links of a slot correspond.

structure OccN {m k l : Nat} (R : RShape S m k l) (l' : Nat) where
  nm : Fin k → Nat
  zn : Fin l → Nat
  hz : ∀ s t, zn s = zn t → s = t
  zn' : Fin l' → Nat
  hz' : ∀ s t, zn' s = zn' t → s = t
  X : NameSet Nat
  hX : ∀ s, zn s ∉ X.names
  hX' : ∀ s, zn' s ∉ X.names
  d : Bg S Iface.origin ⟨m, NameSet.union (innN zn hz) X⟩
  hb : BDiscrete ob d
  K : Iface Nat
  D : Bg S (nFace nm X) K

noncomputable def occEquivN :
    SupportEquivI ι κ (o.Gy R' ϱ η).lean (o₀.Gy R' ϱ η).lean

Theorem 4 (The correspondence). For every closed process p, the reactions of the agent of p are exactly the agents of the reducts of p, over all active contexts and all binding-discrete parameters.

theorem react_iffπ (X : NameSet Nat) (ρ : Nat → Nat) {p : Proc} (hcl : Closed p)
    (hp : NamesIn X.names ρ p) (b : Abstract sig Nat) :
    React piRules (agentπ X ρ p hp) b ↔
      ∃ q, ∃ hr : Red p q, b = agentπ X ρ q (NamesIn.of_red hr hp) :=
  ⟨react_completeπ X ρ hcl hp, fun ⟨_, hr, hb⟩ => hb ▸ red_soundπ hr X ρ hp⟩

The rule's nodes are read back as positions of the process. The process is rearranged around them up to structural congruence: the restrictions at the top to the front, the two matched components split out, the send and the input split out of their sums. The π reduction is then read off. Only the two channels are read back from the agent, and they are equal because the rule links both to one slot. The received name is never read back: it is the rule's own edge, and the reactum wires it to the datum, which is the send's. Occurrence determinacy (Theorem 3) then carries the given reaction to the canonical instance of that reduction, whose reactum is the reduct. Jensen states his correspondence with the proof sketched as following the earlier ones [Jen06, Thm 7.21]; this is a kernel-checked version, for closed processes.

Theorem 5 (Different agents). The two agents differ: the first has a binder in a region, the second has none.

theorem jensen_agents_ne : agentπ X01 ρ01 pShared namesShared ≠ agentπ X01 ρ01 pPrivate namesPrivate

Theorem 6 (Each reacts to its reduct). By Theorem 4, these are also the only reactions of the two agents, since both processes are closed.

theorem jensen_react :
    React piRules (agentπ X01 ρ01 pShared namesShared)
        (agentπ X01 ρ01 qShared (NamesIn.of_red red_shared namesShared)) ∧
      React piRules (agentπ X01 ρ01 pPrivate namesPrivate)
        (agentπ X01 ρ01 qPrivate (NamesIn.of_red red_private namesPrivate))

Jensen's printed reduct of the second process puts νz outside the replicated input [Jen06, p. 113]. His rule keeps it inside, and so does 0 | (νz (z̄y | z(u))) | !x(u).νz (z̄u | z(v)) here.

Theorem 7 (Mobility). The two reductions, and the two reactions of the agents.

theorem red_mob₁ : Red pMob qMob

theorem red_mob₂ : Red qMob rMob

theorem mob_react :
    React piRules (agentπ X01 ρ01 pMob namesMob)
        (agentπ X01 ρ01 qMob (NamesIn.of_red red_mob₁ namesMob)) ∧
      React piRules (agentπ X01 ρ01 qMob (NamesIn.of_red red_mob₁ namesMob))
        (agentπ X01 ρ01 rMob (NamesIn.of_red red_mob₂ (NamesIn.of_red red_mob₁ namesMob)))