5.1. The calculus and its encoding
Processes P ::= 0 \mid P \mid P \mid \nu P \mid M \mid {!x(z).P} and
guarded sums M ::= \bar{x}y.P \mid x(z).P \mid M + M, with de Bruijn
names. Structural congruence P \equiv Q is the least congruence with
the commutative monoid laws of \mid (unit 0), commutativity and
associativity of + (sums are non-empty), scope extrusion, and the exchange
of two adjacent restrictions. Reduction P \to Q is generated by
(\bar{x}y.P + M) \mid (x(z).Q + N) \to P \mid Q\{y/z\}, \qquad (\bar{x}y.P + M) \mid {!x(z).Q} \to (P \mid Q\{y/z\}) \mid {!x(z).Q}
(either sum may be a single summand) and closed under parallel composition, restriction and structural congruence.
Class: Proc, Pi.Sum, Red FROM SOURCE; SC BRIDGED and UNBRIDGED.
Lean code for Definition5.1.1●4 definitions
-
inductivedefined in Pi/Calculus.leancomplete
inductive Proc : Type
inductive Proc : Type
Constructors
nil : Proc
par : Proc → Proc → Proc
res : Proc → Proc
sum : Pi.Sum → Proc
rep : Shapes.Chan → Proc → Proc
`!x(z).P`: replicated input; `z` is index `0` of `P`.
-
inductivedefined in Pi/Calculus.leancomplete
inductive Sum : Type
inductive Sum : Type
Constructors
snd : Shapes.Chan → Shapes.Chan → Proc → Pi.Sum
`x̄y.P`
rcv : Shapes.Chan → Proc → Pi.Sum
`x(z).P`: `z` is index `0` of `P`.
plus : Pi.Sum → Pi.Sum → Pi.Sum
-
inductivedefined in Pi/Calculus.leancomplete
inductive SC : Proc → Proc → Prop
inductive SC : Proc → Proc → Prop
Structural congruence of processes. Scope extrusion carries the shifted process as a field.
Constructors
refl (p : Proc) : p ≡ p
symm {p q : Proc} : p ≡ q → q ≡ p
trans {p q r : Proc} : p ≡ q → q ≡ r → p ≡ r
parNil (p : Proc) : p.par Proc.nil ≡ p
parComm (p q : Proc) : p.par q ≡ q.par p
parAssoc (p q r : Proc) : (p.par q).par r ≡ p.par (q.par r)
parCong {p p' q q' : Proc} : p ≡ p' → q ≡ q' → p.par q ≡ p'.par q'
resCong {p p' : Proc} : p ≡ p' → p.res ≡ p'.res
sumCong {m m' : Pi.Sum} : SCS m m' → Proc.sum m ≡ Proc.sum m'
repCong (x : Shapes.Chan) {p p' : Proc} : p ≡ p' → Proc.rep x p ≡ Proc.rep x p'
resPar (p q : Proc) {p' : Proc} (h : p' = Proc.shift 0 p) : p.par q.res ≡ (p'.par q).res
resSwap (p : Proc) {p' : Proc} (h : p' = Proc.swap 0 p) : p.res.res ≡ p'.res.res
Two restrictions exchanged (Jensen's `νxνy P ≡ νyνx P`, Thm 7.18).
-
inductivedefined in Pi/Calculus.leancomplete
inductive Red : Proc → Proc → Prop
inductive Red : Proc → Proc → Prop
**Reduction.** The received body, its bound name replaced by the name sent, is a field `q' = q.subst 0 y`, never an index.
Constructors
comm {x y : Shapes.Chan} {p : Proc} {m : Pi.Sum} {q : Proc} {n : Pi.Sum} {q' : Proc} (h₁ : InSnd x y p m) (h₂ : InRcv x q n) (hq : q' = Proc.subst 0 y q) : (Proc.sum m).par (Proc.sum n) ⟶ p.par q'
rep {x y : Shapes.Chan} {p : Proc} {m : Pi.Sum} {q q' : Proc} (h₁ : InSnd x y p m) (hq : q' = Proc.subst 0 y q) : (Proc.sum m).par (Proc.rep x q) ⟶ (p.par q').par (Proc.rep x q)
parL {p p' : Proc} (q : Proc) : p ⟶ p' → p.par q ⟶ p'.par q
res {p p' : Proc} : p ⟶ p' → p.res ⟶ p'.res
struct {p p' q' q : Proc} : p ≡ p' → p' ⟶ q' → q' ≡ q → p ⟶ q
An environment \rho names the indices that escape their binders.
\mathrm{fn}_\rho(P) \subseteq X says that every free name of P under
\rho lies in X. A process is closed when its free names do not depend
on \rho, that is, when no index escapes its binders.
Class: NamesIn FROM SOURCE; Closed NEW.
Lean code for Definition5.1.2●2 definitions
-
defdefined in Pi/Calculus.leancomplete
def NamesIn (X : List Nat) (ρ : Nat → Nat) (p : Proc) : Prop
def NamesIn (X : List Nat) (ρ : Nat → Nat) (p : Proc) : Prop
`p` mentions only names of `X`, under the environment `ρ`.
-
defdefined in Pi/Canon.leancomplete
def Closed (p : Proc) : Prop
def Closed (p : Proc) : Prop
**A closed process**: its free names do not depend on the environment, so no index escapes its binders.
For \mathrm{fn}_\rho(P) \subseteq X, the encoding of P is a ground
bigraph with one root and outer names X, over five controls after
Jensen's (a sum, an output, an input, a replicated input, and the binder of a
restriction), all passive and none atomic (Jensen's restriction control is
atomic); \llbracket P \rrbracket_{X,\rho} is its abstract bigraph. The
rules \mathcal{R}_\pi are the ground instances, for every choice of names,
of Jensen's communication rule and replicated communication rule, over
binding-discrete parameters: every edge a parameter uses is bound in it (by
the port of a restriction or the datum port of an input), every such binding
port lies on an edge, and every edge lies within one region.
Lean code for Definition5.1.3●5 definitions
-
defdefined in Pi/Enc.leancomplete
def encπ (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc) (h : NamesIn X.names ρ p) : Bg sig ε { width := 1, names := X }
def encπ (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc) (h : NamesIn X.names ρ p) : Bg sig ε { width := 1, names := X }
**The encoding of a π process.**
-
defdefined in Pi/Enc.leancomplete
def agentπ (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc) (h : NamesIn X.names ρ p) : Bg.Abstract sig Nat
def agentπ (X : NameSet Nat) (ρ : Nat → Nat) (p : Proc) (h : NamesIn X.names ρ p) : Bg.Abstract sig Nat
**A π process as an abstract agent.**
-
defdefined in Pi/Sound.leancomplete
def commRule : Shapes.PRuleN sig
def commRule : Shapes.PRuleN sig
**Communication**: the send's continuation, and the receive's body with its local name renamed to the reactum's, which is wired to `y`.
-
defdefined in Pi/Sound.leancomplete
def repRule : Shapes.PRuleN sig
def repRule : Shapes.PRuleN sig
**Replicated communication**: the body is copied out, its local name renamed to `w` and wired to `y`; the body inside keeps `z`.
-
defdefined in Pi/Sound.leancomplete
def piRules : Bg.Rules sig Nat
def piRules : Bg.Rules sig Nat
**The ground rules of the π encoding.**