Strong free-channel barbed bisimilarity

InductiveFree-channel input and output observables#✓fully proved

A visible input or output subject. Restricted variables are not subjects of these free-channel observations.

inductive Observable where
  | input (channel : ℕ)
  | output (channel : ℕ)
  deriving DecidableEq, Repr

Used by 17

Used byImmediate free-channel barb · Structural congruence preserves immediate barbs · Barbed bisimilar processes have the same barbs · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Labels for reductions and barb observations · Structural congruence is a strong barbed bisimulation · Free-channel input is not barbed bisimilar to nil · Decorated-LTS bisimulations are exactly strong barbed bisimulations · May-barb after finitely many reductions · Barbed bisimilarity preserves may-barbs · Reduction LTS decorated with barb observations · Exposed guards are barbs · Free-channel guard offered without reduction · Barbed bisimilarity matches each reduction by one reduction

InductiveFree-channel guard offered without reduction#✓fully proved

A selected free-channel guard exposed without reduction. Restrictions hide bound subjects but do not hide free constants.

inductive Offer : Proc → Observable → Prop where
  | input {p q : Proc} {a : ℕ} :
      Select p (.inp (.const a) q) → Offer p (.input a)
  | output {p q : Proc} {a : ℕ} {b : Name} :
      Select p (.out (.const a) b q) → Offer p (.output a)
  | parL {p q : Proc} {o : Observable} :
      Offer p o → Offer (.par p q) o
  | parR {p q : Proc} {o : Observable} :
      Offer q o → Offer (.par p q) o
  | nu {p : Proc} {o : Observable} : Offer p o → Offer (.nu p) o

Uses 4 · Used by 8

Statement usesChannel name in the π-calculus · Free-channel input and output observables · Processes of the π-calculus · Guarded-choice resolution in the π-calculus

Used byImmediate free-channel barb · Structural congruence preserves immediate barbs · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Free-channel input is not barbed bisimilar to nil · Exposed guards are barbs

DefinitionImmediate free-channel barb#✓fully proved

Immediate free-channel readiness, up to the existing structural congruence. A witness performs no Step.

def Barb (p : Proc) (o : Observable) : Prop :=
  ∃ q, Cong p q ∧ Offer q o

Uses 4 · Used by 14

Statement usesStructural congruence of π-calculus processes · Free-channel input and output observables · Free-channel guard offered without reduction · Processes of the π-calculus

Used byStructural congruence preserves immediate barbs · Barbed bisimilar processes have the same barbs · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Structural congruence is a strong barbed bisimulation · Free-channel input is not barbed bisimilar to nil · Decorated-LTS bisimulations are exactly strong barbed bisimulations · May-barb after finitely many reductions · Barbed bisimilarity preserves may-barbs · Reduction LTS decorated with barb observations · Exposed guards are barbs · Barbed bisimilarity matches each reduction by one reduction

InductiveLabels for reductions and barb observations#✓fully proved

Labels for reductions and observation-only self-loops.

inductive BehaviourLabel where
  | reduce
  | observe (o : Observable)
  deriving DecidableEq, Repr

Uses 1 · Used by 8

Statement usesFree-channel input and output observables

Used byBarbed bisimilar processes have the same barbs · Strong barbed bisimilarity · Structurally congruent processes are barbed bisimilar · Structural congruence is a strong barbed bisimulation · Decorated-LTS bisimulations are exactly strong barbed bisimulations · Barbed bisimilarity preserves may-barbs · Reduction LTS decorated with barb observations · Barbed bisimilarity matches each reduction by one reduction

DefinitionReduction LTS decorated with barb observations#✓fully proved

The existing reduction semantics decorated with barb tests. The observation transitions do not consume a prefix or transmit a name.

def observedLTS : LTS Proc BehaviourLabel where
  Tr p label q := match label with
    | .reduce => Step p q
    | .observe o => p = q ∧ Barb p o

Uses 5 · Used by 7

Statement usesImmediate free-channel barb · Labels for reductions and barb observations · Free-channel input and output observables · Processes of the π-calculus · Reduction relation of the π-calculus

Used byBarbed bisimilar processes have the same barbs · Strong barbed bisimilarity · Structurally congruent processes are barbed bisimilar · Structural congruence is a strong barbed bisimulation · Decorated-LTS bisimulations are exactly strong barbed bisimulations · Barbed bisimilarity preserves may-barbs · Barbed bisimilarity matches each reduction by one reduction

DefinitionStrong barbed bisimilarity#✓fully proved

Strong barbed bisimilarity, using the canonical CSLib bisimulation API. No context closure is built into this relation.

def BarbedBisimilar : Proc → Proc → Prop :=
  LTS.HomBisimilarity observedLTS

Uses 3 · Used by 10

Statement usesLabels for reductions and barb observations · Processes of the π-calculus · Reduction LTS decorated with barb observations

Used byBarbed bisimilar processes have the same barbs · Structurally congruent processes are barbed bisimilar · Free-channel input is not barbed bisimilar to nil · Barbed bisimilarity preserves may-barbs · Barbed bisimilarity transfers finite reduction paths · Barbed bisimilarity matches each reduction by one reduction · Contextual barbed equivalence implies barbed bisimilarity · Contextual strong barbed equivalence · Contextual barbed equivalence is closed under contexts · Structural laws are barbed sound in capture-avoiding contexts

TheoremDecorated-LTS bisimulations are exactly strong barbed bisimulations#✓fully proved

The decorated LTS has precisely the strong reduction-matching and immediate-barb-preservation clauses of a strong barbed bisimulation.

theorem isBisimulation_observedLTS_iff (r : Proc → Proc → Prop) :
    LTS.IsHomBisimulation observedLTS r ↔
      ∀ ⦃p q⦄, r p q →
        (∀ p', Step p p' → ∃ q', Step q q' ∧ r p' q') ∧
        (∀ q', Step q q' → ∃ p', Step p p' ∧ r p' q') ∧
        (∀ o, Barb p o ↔ Barb q o)

Uses 6 · Used by 3

Statement usesImmediate free-channel barb · Labels for reductions and barb observations · Free-channel input and output observables · Processes of the π-calculus · Reduction relation of the π-calculus · Reduction LTS decorated with barb observations

Used byBarbed bisimilar processes have the same barbs · Structural congruence is a strong barbed bisimulation · Barbed bisimilarity matches each reduction by one reduction

TheoremStructural congruence preserves immediate barbs#✓fully proved

Structural congruence preserves immediate barbs.

theorem Cong.barb_iff {p q : Proc} (h : Cong p q) (o : Observable) :
    Barb p o ↔ Barb q o

Uses 5 · Used by 1

Statement usesImmediate free-channel barb · Structural congruence of π-calculus processes · Free-channel input and output observables · Processes of the π-calculus

Proof usesFree-channel guard offered without reduction

Used byStructural congruence is a strong barbed bisimulation

TheoremStructural congruence is a strong barbed bisimulation#✓fully proved

Structural congruence is a strong barbed bisimulation: reductions match one for one, while free-channel observations match immediately.

theorem cong_isBarbedBisimulation :
    LTS.IsHomBisimulation observedLTS Cong

Uses 9 · Used by 1

Statement usesLabels for reductions and barb observations · Structural congruence of π-calculus processes · Processes of the π-calculus · Reduction LTS decorated with barb observations

Proof usesImmediate free-channel barb · Structural congruence preserves immediate barbs · Free-channel input and output observables · Reduction relation of the π-calculus · Decorated-LTS bisimulations are exactly strong barbed bisimulations

Used byStructurally congruent processes are barbed bisimilar

TheoremStructurally congruent processes are barbed bisimilar#✓fully proved

Every structural law of Basic is sound for strong barbed bisimilarity, including scope extrusion and replication unfolding.

theorem Cong.barbedBisimilar {p q : Proc} (h : Cong p q) :
    BarbedBisimilar p q

Uses 6 · Used by 1

Statement usesStrong barbed bisimilarity · Structural congruence of π-calculus processes · Processes of the π-calculus

Proof usesLabels for reductions and barb observations · Structural congruence is a strong barbed bisimulation · Reduction LTS decorated with barb observations

Used byStructural congruence implies contextual barbed equivalence

DefinitionUnguarded output in a process#✓fully proved

An output not behind a prefix, on any subject (including bound names). This is an overapproximation for arbitrary unguarded sums, not a barb.

def HasUnguardedOutput : Proc → Prop
  | .nil => False
  | .out _ _ _ => True
  | .inp _ _ => False
  | .par p q => HasUnguardedOutput p ∨ HasUnguardedOutput q
  | .nu p => HasUnguardedOutput p
  | .repl p => HasUnguardedOutput p
  | .sum p q => HasUnguardedOutput p ∨ HasUnguardedOutput q

Uses 2 · Used by 6

Statement usesChannel name in the π-calculus · Processes of the π-calculus

Used byEvery reduction source has an unguarded output · Structural congruence preserves unguarded outputs · Processes without unguarded output cannot reduce · Every phase of the restricted repeated session can step · Idle processes have no unguarded output · Every phase of the repeated session can step

TheoremStructural congruence preserves unguarded outputs#✓fully proved

Structural rearrangement cannot expose an output from an input-guarded process. This includes arbitrary uses of replication and scope laws.

theorem Cong.hasUnguardedOutput_iff {p q : Proc} (h : Cong p q) :
    HasUnguardedOutput p ↔ HasUnguardedOutput q

Uses 8 · Used by 1

Statement usesStructural congruence of π-calculus processes · Unguarded output in a process · Processes of the π-calculus

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process

Used byEvery reduction source has an unguarded output

TheoremEvery reduction source has an unguarded output#✓fully proved

Every reduction needs an unguarded output in its source, even when communication is private or structural congruence is used arbitrarily.

theorem Step.hasUnguardedOutput {p q : Proc} (h : Step p q) :
    HasUnguardedOutput p

Uses 8 · Used by 2

Statement usesUnguarded output in a process · Processes of the π-calculus · Reduction relation of the π-calculus

Proof usesStructural congruence of π-calculus processes · Structural congruence preserves unguarded outputs · Channel name in the π-calculus · Guarded-choice resolution in the π-calculus · Substitution for the innermost bound variable of a process

Used byProcesses without unguarded output cannot reduce · Idle processes cannot step

TheoremProcesses without unguarded output cannot reduce#✓fully proved

Outputless processes cannot reduce. Input guards may still have observable input barbs; this theorem does not identify them with nil.

theorem not_step_of_no_output {p : Proc}
    (h : ¬ HasUnguardedOutput p) (q : Proc) : ¬ Step p q

Uses 4

Statement usesUnguarded output in a process · Processes of the π-calculus · Reduction relation of the π-calculus

Proof usesEvery reduction source has an unguarded output

TheoremExposed guards are barbs#✓fully proved

A directly exposed guard is a barb, with the reflexive structural representative as witness.

theorem Barb.of_offer {p : Proc} {o : Observable} (h : Offer p o) :
    Barb p o

Uses 5 · Used by 4

Statement usesImmediate free-channel barb · Free-channel input and output observables · Free-channel guard offered without reduction · Processes of the π-calculus

Proof usesStructural congruence of π-calculus processes

Used byBarbs of an input prefix · Barbs of a restricted output prefix · Barbs of an output prefix · Free-channel input is not barbed bisimilar to nil

TheoremThe inactive process has no barbs#✓fully proved

The inactive process has no barb, even after structural rearrangement.

@[simp] theorem barb_nil (o : Observable) : ¬ Barb .nil o

Uses 11 · Used by 1

Statement usesImmediate free-channel barb · Free-channel input and output observables · Processes of the π-calculus

Proof usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Free-channel guard offered without reduction · Guarded-choice resolution in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process

Used byFree-channel input is not barbed bisimilar to nil

TheoremBarbs of an output prefix#✓fully proved

Output readiness sees only its free subject and direction, not its object or guarded continuation.

@[simp] theorem barb_out_iff (a b : Name) (p : Proc) (o : Observable) :
    Barb (.out a b p) o ↔ ∃ n, a = .const n ∧ o = .output n

Uses 12

Statement usesImmediate free-channel barb · Channel name in the π-calculus · Free-channel input and output observables · Processes of the π-calculus

Proof usesExposed guards are barbs · Structural congruence of π-calculus processes · Free-channel guard offered without reduction · Guarded-choice resolution in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process

TheoremBarbs of an input prefix#✓fully proved

Waiting inputs are observable, despite being unable to reduce alone.

@[simp] theorem barb_inp_iff (a : Name) (p : Proc) (o : Observable) :
    Barb (.inp a p) o ↔ ∃ n, a = .const n ∧ o = .input n

Uses 12

Statement usesImmediate free-channel barb · Channel name in the π-calculus · Free-channel input and output observables · Processes of the π-calculus

Proof usesExposed guards are barbs · Structural congruence of π-calculus processes · Free-channel guard offered without reduction · Guarded-choice resolution in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process

TheoremBarbs of a restricted output prefix#✓fully proved

A restricted output is visible exactly when its subject is free. Sending the private name on a free subject remains observable.

@[simp] theorem barb_nu_out_iff (a b : Name) (p : Proc) (o : Observable) :
    Barb (.nu (.out a b p)) o ↔ ∃ n, a = .const n ∧ o = .output n

Uses 12

Statement usesImmediate free-channel barb · Channel name in the π-calculus · Free-channel input and output observables · Processes of the π-calculus

Proof usesExposed guards are barbs · Structural congruence of π-calculus processes · Free-channel guard offered without reduction · Guarded-choice resolution in the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process

TheoremBarbed bisimilar processes have the same barbs#✓fully proved

Bisimilar processes have the same immediate free-channel barbs.

theorem BarbedBisimilar.barb_iff {p q : Proc}
    (h : BarbedBisimilar p q) (o : Observable) : Barb p o ↔ Barb q o

Uses 8 · Used by 2

Statement usesImmediate free-channel barb · Strong barbed bisimilarity · Free-channel input and output observables · Processes of the π-calculus

Proof usesLabels for reductions and barb observations · Reduction relation of the π-calculus · Decorated-LTS bisimulations are exactly strong barbed bisimulations · Reduction LTS decorated with barb observations

Used byFree-channel input is not barbed bisimilar to nil · Barbed bisimilarity preserves may-barbs

TheoremBarbed bisimilarity matches each reduction by one reduction#✓fully proved

A reduction from the first process is matched by one reduction, with strong barbed bisimilar derivatives.

theorem BarbedBisimilar.step {p q p' : Proc}
    (h : BarbedBisimilar p q) (hs : Step p p') :
    ∃ q', Step q q' ∧ BarbedBisimilar p' q'

Uses 8 · Used by 1

Statement usesStrong barbed bisimilarity · Processes of the π-calculus · Reduction relation of the π-calculus

Proof usesImmediate free-channel barb · Labels for reductions and barb observations · Free-channel input and output observables · Decorated-LTS bisimulations are exactly strong barbed bisimulations · Reduction LTS decorated with barb observations

Used byBarbed bisimilarity transfers finite reduction paths

TheoremFree-channel input is not barbed bisimilar to nil#✓fully proved

Waiting for input is not equivalent to doing nothing. Reduction-only bisimilarity would miss this distinction.

theorem input_not_barbedBisimilar_nil (a : ℕ) (p : Proc) :
    ¬ BarbedBisimilar (.inp (.const a) p) .nil

Uses 10

Statement usesStrong barbed bisimilarity · Channel name in the π-calculus · Processes of the π-calculus

Proof usesImmediate free-channel barb · Exposed guards are barbs · Barbed bisimilar processes have the same barbs · Free-channel input and output observables · Free-channel guard offered without reduction · Guarded-choice resolution in the π-calculus · The inactive process has no barbs

DefinitionMay-barb after finitely many reductions#✓fully proved

A free-channel barb reachable by finitely many existing reductions, possibly zero. This is a may observation, not a weak equivalence.

def MayBarb (p : Proc) (o : Observable) : Prop :=
  ∃ p', Relation.ReflTransGen Step p p' ∧ Barb p' o

Uses 4 · Used by 1

Statement usesImmediate free-channel barb · Free-channel input and output observables · Processes of the π-calculus · Reduction relation of the π-calculus

Used byBarbed bisimilarity preserves may-barbs

TheoremBarbed bisimilarity transfers finite reduction paths#✓fully proved

A finite reduction path transfers across strong barbed bisimilarity.

theorem BarbedBisimilar.reductionPath {p q p' : Proc}
    (h : BarbedBisimilar p q) (hs : Relation.ReflTransGen Step p p') :
    ∃ q', Relation.ReflTransGen Step q q' ∧ BarbedBisimilar p' q'

Uses 4 · Used by 1

Statement usesStrong barbed bisimilarity · Processes of the π-calculus · Reduction relation of the π-calculus

Proof usesBarbed bisimilarity matches each reduction by one reduction

Used byBarbed bisimilarity preserves may-barbs

TheoremBarbed bisimilarity preserves may-barbs#✓fully proved

Strong barbed bisimilarity preserves finite may observations.

theorem BarbedBisimilar.mayBarb_iff {p q : Proc}
    (h : BarbedBisimilar p q) (o : Observable) :
    MayBarb p o ↔ MayBarb q o

Uses 10

Statement usesStrong barbed bisimilarity · May-barb after finitely many reductions · Free-channel input and output observables · Processes of the π-calculus

Proof usesImmediate free-channel barb · Barbed bisimilar processes have the same barbs · Barbed bisimilarity transfers finite reduction paths · Labels for reductions and barb observations · Reduction relation of the π-calculus · Reduction LTS decorated with barb observations

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.