module plfa.part2.Bisimulation where
Some constructs can be defined in terms of other constructs. In the
previous chapter, we saw how let terms can be rewritten as an
application of an abstraction, and how two alternative formulations of
products — one with projections and one with case — can be formulated
in terms of each other. In this chapter, we look at how to formalise
such claims.
Given two different systems, with different terms and reduction rules,
we define what it means to claim that one simulates the other.
Let’s call our two systems source and target. Let M, N range
over terms of the source, and M†, N† range over terms of the
target. We define a relation
M ~ M†
between corresponding terms of the two systems. We have a
simulation of the source by the target if every reduction
in the source has a corresponding reduction sequence
in the target:
Simulation: For every M, M†, and N:
If M ~ M† and M —→ N
then M† —↠ N† and N ~ N†
for some N†.
Or, in a diagram:
M --- —→ --- N
| |
| |
~ ~
| |
| |
M† --- —↠ --- N†
Sometimes we will have a stronger condition, where each reduction in the source
corresponds to a reduction (rather than a reduction sequence)
in the target:
M --- —→ --- N
| |
| |
~ ~
| |
| |
M† --- —→ --- N†
This stronger condition is known as lock-step or on the nose simulation.
We are particularly interested in the situation where there is also
a simulation from the target to the source: every reduction in the
target has a corresponding reduction sequence in the source. This
situation is called a bisimulation.
Simulation is established by case analysis over all possible
reductions and all possible terms to which they are related. For each
reduction step in the source we must show a corresponding reduction
sequence in the target.
For instance, the source might be lambda calculus with let
added, and the target the same system with let translated out.
The key rule defining our relation will be:
M ~ M†
N ~ N†
--------------------------------
let x = M in N ~ (ƛ x ⇒ N†) · M†
All the other rules are congruences: variables relate to
themselves, and abstractions and applications relate if their
components relate:
-----
x ~ x
N ~ N†
------------------
ƛ x ⇒ N ~ ƛ x ⇒ N†
L ~ L†
M ~ M†
---------------
L · M ~ L† · M†
Covering the other constructs of our language — naturals,
fixpoints, products, and so on — would add little save length.
In this case, our relation can be specified by a function
from source to target:
(x) † = x
(ƛ x ⇒ N) † = ƛ x ⇒ (N †)
(L · M) † = (L †) · (M †)
(let x = M in N) † = (ƛ x ⇒ (N †)) · (M †)
And we have
M † ≡ N
-------
M ~ N
and conversely. But in general we may have a relation without any
corresponding function.
This chapter formalises establishing that ~ as defined
above is a simulation from source to target. We leave
establishing it in the reverse direction as an exercise.
Another exercise is to show the alternative formulations
of products in
Chapter More
are in bisimulation.
Imports
We import our source language from
Chapter More:
open import plfa.part2.More
Simulation
The simulation is a straightforward formalisation of the rules
in the introduction:
infix 4 _~_ infix 5 ~ƛ_ infix 7 _~·_ data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where ~` : ∀ {Γ A} {x : Γ ∋ A} --------- → ` x ~ ` x ~ƛ_ : ∀ {Γ A B} {N N† : Γ , A ⊢ B} → N ~ N† ---------- → ƛ N ~ ƛ N† _~·_ : ∀ {Γ A B} {L L† : Γ ⊢ A ⇒ B} {M M† : Γ ⊢ A} → L ~ L† → M ~ M† --------------- → L · M ~ L† · M† ~let : ∀ {Γ A B} {M M† : Γ ⊢ A} {N N† : Γ , A ⊢ B} → M ~ M† → N ~ N† ---------------------- → `let M N ~ (ƛ N†) · M†
The language in Chapter More has more constructs, which we could easily add.
However, leaving the simulation small let’s us focus on the essence.
It’s a handy technical trick that we can have a large source language,
but only bother to include in the simulation the terms of interest.
Exercise _† (practice)
Formalise the translation from source to target given in the introduction.
Show that M † ≡ N implies M ~ N, and conversely.
-- Your code goes here
Simulation commutes with values
We need a number of technical results. The first is that simulation
commutes with values. That is, if M ~ M† and M is a value then
M† is also a value:
~val : ∀ {Γ A} {M M† : Γ ⊢ A} → M ~ M† → Value M -------- → Value M† ~val ~` () ~val (~ƛ ~N) V-ƛ = V-ƛ ~val (~L ~· ~M) () ~val (~let ~M ~N) ()
It is a straightforward case analysis, where here the only value
of interest is a lambda abstraction.
Exercise ~val⁻¹ (practice)
Show that this also holds in the reverse direction: if M ~ M†
and Value M† then Value M.
-- Your code goes here
Simulation commutes with renaming
The next technical result is that simulation commutes with renaming.
That is, if ρ maps any judgment Γ ∋ A to a judgment Δ ∋ A,
and if M ~ M† then rename ρ M ~ rename ρ M†:
~rename : ∀ {Γ Δ} → (ρ : ∀ {A} → Γ ∋ A → Δ ∋ A) ---------------------------------------------------------- → (∀ {A} {M M† : Γ ⊢ A} → M ~ M† → rename ρ M ~ rename ρ M†) ~rename ρ (~`) = ~` ~rename ρ (~ƛ ~N) = ~ƛ (~rename (ext ρ) ~N) ~rename ρ (~L ~· ~M) = (~rename ρ ~L) ~· (~rename ρ ~M) ~rename ρ (~let ~M ~N) = ~let (~rename ρ ~M) (~rename (ext ρ) ~N)
The structure of the proof is similar to the structure of renaming itself:
reconstruct each term with recursive invocation, extending the environment
where appropriate (in this case, only for the body of an abstraction).
Simulation commutes with substitution
The third technical result is that simulation commutes with substitution.
It is more complex than renaming, because where we had one renaming map
ρ here we need two substitution maps, σ and σ†.
The proof first requires we establish an analogue of extension.
If σ and σ† both map any judgment Γ ∋ A to a judgment Δ ⊢ A,
such that for every x in Γ ∋ A we have σ x ~ σ† x,
then for any x in Γ , B ∋ A we have exts σ x ~ exts σ† x:
~exts : ∀ {Γ Δ} → {σ : ∀ {A} → Γ ∋ A → Δ ⊢ A} → {σ† : ∀ {A} → Γ ∋ A → Δ ⊢ A} → (∀ {A} → (x : Γ ∋ A) → σ x ~ σ† x) -------------------------------------------------- → (∀ {A B} → (x : Γ , B ∋ A) → exts σ x ~ exts σ† x) ~exts ~σ Z = ~` ~exts ~σ (S x) = ~rename S_ (~σ x)
The structure of the proof is similar to the structure of extension itself.
The newly introduced variable trivially relates to itself, and otherwise
we apply renaming to the hypothesis.
With extension under our belts, it is straightforward to show
substitution commutes. If σ and σ† both map any judgment Γ ∋ A
to a judgment Δ ⊢ A, such that for every x in Γ ∋ A we have σ, and if
x ~ σ† xM ~ M†, then subst σ M ~ subst σ† M†:
~subst : ∀ {Γ Δ} → {σ : ∀ {A} → Γ ∋ A → Δ ⊢ A} → {σ† : ∀ {A} → Γ ∋ A → Δ ⊢ A} → (∀ {A} → (x : Γ ∋ A) → σ x ~ σ† x) --------------------------------------------------------- → (∀ {A} {M M† : Γ ⊢ A} → M ~ M† → subst σ M ~ subst σ† M†) ~subst ~σ (~` {x = x}) = ~σ x ~subst ~σ (~ƛ ~N) = ~ƛ (~subst (~exts ~σ) ~N) ~subst ~σ (~L ~· ~M) = (~subst ~σ ~L) ~· (~subst ~σ ~M) ~subst ~σ (~let ~M ~N) = ~let (~subst ~σ ~M) (~subst (~exts ~σ) ~N)
Again, the structure of the proof is similar to the structure of
substitution itself: reconstruct each term with recursive invocation,
extending the environment where appropriate (in this case, only for
the body of an abstraction).
From the general case of substitution, it is also easy to derive
the required special case. If N ~ N† and M ~ M†, then
N [ M ] ~ N† [ M† ]:
~sub : ∀ {Γ A B} {N N† : Γ , B ⊢ A} {M M† : Γ ⊢ B} → N ~ N† → M ~ M† ----------------------- → (N [ M ]) ~ (N† [ M† ]) ~sub {Γ} {A} {B} ~N ~M = ~subst {Γ , B} {Γ} ~σ {A} ~N where ~σ : ∀ {A} → (x : Γ , B ∋ A) → _ ~ _ ~σ Z = ~M ~σ (S x) = ~`
Once more, the structure of the proof resembles the original.
The relation is a simulation
Finally, we can show that the relation actually is a simulation.
In fact, we will show the stronger condition of a lock-step simulation.
What we wish to show is:
Lock-step simulation: For every M, M†, and N:
If M ~ M† and M —→ N
then M† —→ N† and N ~ N†
for some N†.
Or, in a diagram:
M --- —→ --- N
| |
| |
~ ~
| |
| |
M† --- —→ --- N†
We first formulate a concept corresponding to the lower leg
of the diagram, that is, its right and bottom edges:
data Leg {Γ A} (M† N : Γ ⊢ A) : Set where leg : ∀ {N† : Γ ⊢ A} → N ~ N† → M† —→ N† -------- → Leg M† N
For our formalisation, in this case, we can use a stronger
relation than —↠, replacing it by —→.
We can now state and prove that the relation is a simulation.
Again, in this case, we can use a stronger relation than
—↠, replacing it by —→:
sim : ∀ {Γ A} {M M† N : Γ ⊢ A} → M ~ M† → M —→ N --------- → Leg M† N sim ~` () sim (~ƛ ~N) () sim (~L ~· ~M) (ξ-·₁ L—→) with sim ~L L—→ ... | leg ~L′ L†—→ = leg (~L′ ~· ~M) (ξ-·₁ L†—→) sim (~V ~· ~M) (ξ-·₂ VV M—→) with sim ~M M—→ ... | leg ~M′ M†—→ = leg (~V ~· ~M′) (ξ-·₂ (~val ~V VV) M†—→) sim ((~ƛ ~N) ~· ~V) (β-ƛ VV) = leg (~sub ~N ~V) (β-ƛ (~val ~V VV)) sim (~let ~M ~N) (ξ-let M—→) with sim ~M M—→ ... | leg ~M′ M†—→ = leg (~let ~M′ ~N) (ξ-·₂ V-ƛ M†—→) sim (~let ~V ~N) (β-let VV) = leg (~sub ~N ~V) (β-ƛ (~val ~V VV))
The proof is by case analysis, examining each possible instance of M ~ M†
and each possible instance of M —→ M†, using recursive invocation whenever
the reduction is by a ξ rule, and hence contains another reduction.
In its structure, it looks a little bit like a proof of progress:
- If the related terms are variables, no reduction applies.
- If the related terms are abstractions, no reduction applies.
- If the related terms are applications, there are three subcases:
-
The source term reduces via
ξ-·₁, in which case the target term does as well.
Recursive invocation gives usL --- —→ --- L′ | | | | ~ ~ | | | | L† --- —→ --- L′†from which follows:
L · M --- —→ --- L′ · M | | | | ~ ~ | | | | L† · M† --- —→ --- L′† · M† -
The source term reduces via
ξ-·₂, in which case the target term does as well.
Recursive invocation gives usM --- —→ --- M′ | | | | ~ ~ | | | | M† --- —→ --- M′†from which follows:
V · M --- —→ --- V · M′ | | | | ~ ~ | | | | V† · M† --- —→ --- V† · M′†Since simulation commutes with values and
Vis a value,V†is also a value. -
The source term reduces via
β-ƛ, in which case the target term does as well:(ƛ x ⇒ N) · V --- —→ --- N [ x := V ] | | | | ~ ~ | | | | (ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V† ]Since simulation commutes with values and
Vis a value,V†is also a value.
Since simulation commutes with substitution andN ~ N†andV ~ V†,
we haveN [ x := V ] ~ N† [ x := V† ].
-
-
If the related terms are a let and an application of an abstraction,
there are two subcases:-
The source term reduces via
ξ-let, in which case the target term
reduces viaξ-·₂. Recursive invocation gives usM --- —→ --- M′ | | | | ~ ~ | | | | M† --- —→ --- M′†from which follows:
let x = M in N --- —→ --- let x = M′ in N | | | | ~ ~ | | | | (ƛ x ⇒ N) · M --- —→ --- (ƛ x ⇒ N) · M′ -
The source term reduces via
β-let, in which case the target
term reduces viaβ-ƛ:let x = V in N --- —→ --- N [ x := V ] | | | | ~ ~ | | | | (ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V† ]Since simulation commutes with values and
Vis a value,V†is also a value.
Since simulation commutes with substitution andN ~ N†andV ~ V†,
we haveN [ x := V ] ~ N† [ x := V† ].
-
Exercise sim⁻¹ (practice)
Show that we also have a simulation in the other direction, and hence that we have
a bisimulation.
-- Your code goes here
Exercise products (practice)
Show that the two formulations of products in
Chapter More
are in bisimulation. The only constructs you need to include are
variables, and those connected to functions and products.
In this case, the simulation is not lock-step.
-- Your code goes here
Unicode
This chapter uses the following unicode:
† U+2020 DAGGER (dag)
⁻ U+207B SUPERSCRIPT MINUS (^-)
¹ U+00B9 SUPERSCRIPT ONE (^1)
近期评论