michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
csci8980-f21/versions/20.07/Bisimulation/index.html

715 lines
80 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!DOCTYPE html>
<html lang="en"><head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Bisimulation: Relating reduction systems | Programming Language Foundations in Agda
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
<meta name="generator" content="Jekyll v3.9.0" />
<meta property="og:title" content="Bisimulation: Relating reduction systems" />
<meta property="og:locale" content="en_US" />
<meta name="description" content="Programming Language Foundations in Agda" />
<meta property="og:description" content="Programming Language Foundations in Agda" />
<link rel="canonical" href="https://plfa.github.io/20.07/Bisimulation/" />
<meta property="og:url" content="https://plfa.github.io/20.07/Bisimulation/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/20.07/Bisimulation/","headline":"Bisimulation: Relating reduction systems","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
<!-- End Jekyll SEO tag -->
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
<body><header class="site-header" role="banner">
<div class="wrapper">
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
</a>
<nav class="site-nav">
<span class="menu-icon">
<svg viewBox="0 0 18 15" width="18px" height="15px">
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
</svg>
</span>
<div class="trigger">
<a class="page-link" href="/20.07/">The Book</a>
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
<a class="page-link" href="/20.07/Citing/">Citing</a>
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
</div>
</nav>
</div>
</header>
<main class="page-content" aria-label="Content">
<div class="wrapper">
<article class="post">
<header class="post-header">
<h1 class="post-title">Bisimulation: Relating reduction systems</h1>
</header>
<p style="text-align:center;">
<a alt="Previous chapter" href="/20.07/More/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part2/Bisimulation.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/20.07/Inference/">Next</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="156" class="Keyword">module</a> <a id="163" href="/20.07/Bisimulation/" class="Module">plfa.part2.Bisimulation</a> <a id="187" class="Keyword">where</a>
</pre>
<p>Some constructs can be defined in terms of other constructs. In the
previous chapter, we saw how <em>let</em> 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.</p>
<p>Given two different systems, with different terms and reduction rules,
we define what it means to claim that one <em>simulates</em> the other.
Let’s call our two systems <em>source</em> and <em>target</em>. Let <code class="language-plaintext highlighter-rouge">M</code>, <code class="language-plaintext highlighter-rouge">N</code> range
over terms of the source, and <code class="language-plaintext highlighter-rouge">M†</code>, <code class="language-plaintext highlighter-rouge">N†</code> range over terms of the
target. We define a relation</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M ~ M†
</code></pre></div></div>
<p>between corresponding terms of the two systems. We have a
<em>simulation</em> of the source by the target if every reduction
in the source has a corresponding reduction sequence
in the target:</p>
<p><em>Simulation</em>: For every <code class="language-plaintext highlighter-rouge">M</code>, <code class="language-plaintext highlighter-rouge">M†</code>, and <code class="language-plaintext highlighter-rouge">N</code>:
If <code class="language-plaintext highlighter-rouge">M ~ M†</code> and <code class="language-plaintext highlighter-rouge">M —→ N</code>
then <code class="language-plaintext highlighter-rouge">M† —↠ N†</code> and <code class="language-plaintext highlighter-rouge">N ~ N†</code>
for some <code class="language-plaintext highlighter-rouge">N†</code>.</p>
<p>Or, in a diagram:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M --- —→ --- N
| |
| |
~ ~
| |
| |
M† --- —↠ --- N†
</code></pre></div></div>
<p>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:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M --- —→ --- N
| |
| |
~ ~
| |
| |
M† --- —→ --- N†
</code></pre></div></div>
<p>This stronger condition is known as <em>lock-step</em> or <em>on the nose</em> simulation.</p>
<p>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 <em>bisimulation</em>.</p>
<p>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.</p>
<p>For instance, the source might be lambda calculus with <em>let</em>
added, and the target the same system with <code class="language-plaintext highlighter-rouge">let</code> translated out.
The key rule defining our relation will be:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M ~ M†
N ~ N†
--------------------------------
let x = M in N ~ (ƛ x ⇒ N†) · M†
</code></pre></div></div>
<p>All the other rules are congruences: variables relate to
themselves, and abstractions and applications relate if their
components relate:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-----
x ~ x
N ~ N†
------------------
ƛ x ⇒ N ~ ƛ x ⇒ N†
L ~ L†
M ~ M†
---------------
L · M ~ L† · M†
</code></pre></div></div>
<p>Covering the other constructs of our language — naturals,
fixpoints, products, and so on — would add little save length.</p>
<p>In this case, our relation can be specified by a function
from source to target:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(x) † = x
(ƛ x ⇒ N) † = ƛ x ⇒ (N †)
(L · M) † = (L †) · (M †)
(let x = M in N) † = (ƛ x ⇒ (N †)) · (M †)
</code></pre></div></div>
<p>And we have</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M † ≡ N
-------
M ~ N
</code></pre></div></div>
<p>and conversely. But in general we may have a relation without any
corresponding function.</p>
<p>This chapter formalises establishing that <code class="language-plaintext highlighter-rouge">~</code> 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 <a href="/20.07/More/">More</a>
are in bisimulation.</p>
<h2 id="imports">Imports</h2>
<p>We import our source language from
Chapter <a href="/20.07/More/">More</a>:</p>
<pre class="Agda"><a id="3625" class="Keyword">open</a> <a id="3630" class="Keyword">import</a> <a id="3637" href="/20.07/More/" class="Module">plfa.part2.More</a>
</pre>
<h2 id="simulation">Simulation</h2>
<p>The simulation is a straightforward formalisation of the rules
in the introduction:</p>
<pre class="Agda"><a id="3762" class="Keyword">infix</a> <a id="3769" class="Number">4</a> <a id="3771" href="/20.07/Bisimulation/#3808" class="Datatype Operator">_~_</a>
<a id="3775" class="Keyword">infix</a> <a id="3782" class="Number">5</a> <a id="3784" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ_</a>
<a id="3788" class="Keyword">infix</a> <a id="3795" class="Number">7</a> <a id="3797" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">_~·_</a>
<a id="3803" class="Keyword">data</a> <a id="_~_"></a><a id="3808" href="/20.07/Bisimulation/#3808" class="Datatype Operator">_~_</a> <a id="3812" class="Symbol">:</a> <a id="3814" class="Symbol">∀</a> <a id="3816" class="Symbol">{</a><a id="3817" href="/20.07/Bisimulation/#3817" class="Bound">Γ</a> <a id="3819" href="/20.07/Bisimulation/#3819" class="Bound">A</a><a id="3820" class="Symbol">}</a> <a id="3822" class="Symbol">→</a> <a id="3824" class="Symbol">(</a><a id="3825" href="/20.07/Bisimulation/#3817" class="Bound">Γ</a> <a id="3827" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="3829" href="/20.07/Bisimulation/#3819" class="Bound">A</a><a id="3830" class="Symbol">)</a> <a id="3832" class="Symbol">→</a> <a id="3834" class="Symbol">(</a><a id="3835" href="/20.07/Bisimulation/#3817" class="Bound">Γ</a> <a id="3837" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="3839" href="/20.07/Bisimulation/#3819" class="Bound">A</a><a id="3840" class="Symbol">)</a> <a id="3842" class="Symbol">→</a> <a id="3844" class="PrimitiveType">Set</a> <a id="3848" class="Keyword">where</a>
<a id="_~_.~`"></a><a id="3857" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a> <a id="3860" class="Symbol">:</a> <a id="3862" class="Symbol">∀</a> <a id="3864" class="Symbol">{</a><a id="3865" href="/20.07/Bisimulation/#3865" class="Bound">Γ</a> <a id="3867" href="/20.07/Bisimulation/#3867" class="Bound">A</a><a id="3868" class="Symbol">}</a> <a id="3870" class="Symbol">{</a><a id="3871" href="/20.07/Bisimulation/#3871" class="Bound">x</a> <a id="3873" class="Symbol">:</a> <a id="3875" href="/20.07/Bisimulation/#3865" class="Bound">Γ</a> <a id="3877" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="3879" href="/20.07/Bisimulation/#3867" class="Bound">A</a><a id="3880" class="Symbol">}</a>
<a id="3887" class="Comment">---------</a>
<a id="3900" class="Symbol">→</a> <a id="3902" href="/20.07/More/#14967" class="InductiveConstructor Operator">`</a> <a id="3904" href="/20.07/Bisimulation/#3871" class="Bound">x</a> <a id="3906" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="3908" href="/20.07/More/#14967" class="InductiveConstructor Operator">`</a> <a id="3910" href="/20.07/Bisimulation/#3871" class="Bound">x</a>
<a id="_~_.~ƛ_"></a><a id="3915" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ_</a> <a id="3919" class="Symbol">:</a> <a id="3921" class="Symbol">∀</a> <a id="3923" class="Symbol">{</a><a id="3924" href="/20.07/Bisimulation/#3924" class="Bound">Γ</a> <a id="3926" href="/20.07/Bisimulation/#3926" class="Bound">A</a> <a id="3928" href="/20.07/Bisimulation/#3928" class="Bound">B</a><a id="3929" class="Symbol">}</a> <a id="3931" class="Symbol">{</a><a id="3932" href="/20.07/Bisimulation/#3932" class="Bound">N</a> <a id="3934" href="/20.07/Bisimulation/#3934" class="Bound">N†</a> <a id="3937" class="Symbol">:</a> <a id="3939" href="/20.07/Bisimulation/#3924" class="Bound">Γ</a> <a id="3941" href="/20.07/More/#14640" class="InductiveConstructor Operator">,</a> <a id="3943" href="/20.07/Bisimulation/#3926" class="Bound">A</a> <a id="3945" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="3947" href="/20.07/Bisimulation/#3928" class="Bound">B</a><a id="3948" class="Symbol">}</a>
<a id="3954" class="Symbol">→</a> <a id="3956" href="/20.07/Bisimulation/#3932" class="Bound">N</a> <a id="3958" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="3960" href="/20.07/Bisimulation/#3934" class="Bound">N†</a>
<a id="3969" class="Comment">----------</a>
<a id="3984" class="Symbol">→</a> <a id="3986" href="/20.07/More/#15035" class="InductiveConstructor Operator">ƛ</a> <a id="3988" href="/20.07/Bisimulation/#3932" class="Bound">N</a> <a id="3990" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="3992" href="/20.07/More/#15035" class="InductiveConstructor Operator">ƛ</a> <a id="3994" href="/20.07/Bisimulation/#3934" class="Bound">N†</a>
<a id="_~_._~·_"></a><a id="4000" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">_~·_</a> <a id="4005" class="Symbol">:</a> <a id="4007" class="Symbol">∀</a> <a id="4009" class="Symbol">{</a><a id="4010" href="/20.07/Bisimulation/#4010" class="Bound">Γ</a> <a id="4012" href="/20.07/Bisimulation/#4012" class="Bound">A</a> <a id="4014" href="/20.07/Bisimulation/#4014" class="Bound">B</a><a id="4015" class="Symbol">}</a> <a id="4017" class="Symbol">{</a><a id="4018" href="/20.07/Bisimulation/#4018" class="Bound">L</a> <a id="4020" href="/20.07/Bisimulation/#4020" class="Bound">L†</a> <a id="4023" class="Symbol">:</a> <a id="4025" href="/20.07/Bisimulation/#4010" class="Bound">Γ</a> <a id="4027" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="4029" href="/20.07/Bisimulation/#4012" class="Bound">A</a> <a id="4031" href="/20.07/More/#14503" class="InductiveConstructor Operator">⇒</a> <a id="4033" href="/20.07/Bisimulation/#4014" class="Bound">B</a><a id="4034" class="Symbol">}</a> <a id="4036" class="Symbol">{</a><a id="4037" href="/20.07/Bisimulation/#4037" class="Bound">M</a> <a id="4039" href="/20.07/Bisimulation/#4039" class="Bound">M†</a> <a id="4042" class="Symbol">:</a> <a id="4044" href="/20.07/Bisimulation/#4010" class="Bound">Γ</a> <a id="4046" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="4048" href="/20.07/Bisimulation/#4012" class="Bound">A</a><a id="4049" class="Symbol">}</a>
<a id="4055" class="Symbol">→</a> <a id="4057" href="/20.07/Bisimulation/#4018" class="Bound">L</a> <a id="4059" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="4061" href="/20.07/Bisimulation/#4020" class="Bound">L†</a>
<a id="4068" class="Symbol">→</a> <a id="4070" href="/20.07/Bisimulation/#4037" class="Bound">M</a> <a id="4072" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="4074" href="/20.07/Bisimulation/#4039" class="Bound">M†</a>
<a id="4083" class="Comment">---------------</a>
<a id="4103" class="Symbol">→</a> <a id="4105" href="/20.07/Bisimulation/#4018" class="Bound">L</a> <a id="4107" href="/20.07/More/#15103" class="InductiveConstructor Operator">·</a> <a id="4109" href="/20.07/Bisimulation/#4037" class="Bound">M</a> <a id="4111" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="4113" href="/20.07/Bisimulation/#4020" class="Bound">L†</a> <a id="4116" href="/20.07/More/#15103" class="InductiveConstructor Operator">·</a> <a id="4118" href="/20.07/Bisimulation/#4039" class="Bound">M†</a>
<a id="_~_.~let"></a><a id="4124" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="4129" class="Symbol">:</a> <a id="4131" class="Symbol">∀</a> <a id="4133" class="Symbol">{</a><a id="4134" href="/20.07/Bisimulation/#4134" class="Bound">Γ</a> <a id="4136" href="/20.07/Bisimulation/#4136" class="Bound">A</a> <a id="4138" href="/20.07/Bisimulation/#4138" class="Bound">B</a><a id="4139" class="Symbol">}</a> <a id="4141" class="Symbol">{</a><a id="4142" href="/20.07/Bisimulation/#4142" class="Bound">M</a> <a id="4144" href="/20.07/Bisimulation/#4144" class="Bound">M†</a> <a id="4147" class="Symbol">:</a> <a id="4149" href="/20.07/Bisimulation/#4134" class="Bound">Γ</a> <a id="4151" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="4153" href="/20.07/Bisimulation/#4136" class="Bound">A</a><a id="4154" class="Symbol">}</a> <a id="4156" class="Symbol">{</a><a id="4157" href="/20.07/Bisimulation/#4157" class="Bound">N</a> <a id="4159" href="/20.07/Bisimulation/#4159" class="Bound">N†</a> <a id="4162" class="Symbol">:</a> <a id="4164" href="/20.07/Bisimulation/#4134" class="Bound">Γ</a> <a id="4166" href="/20.07/More/#14640" class="InductiveConstructor Operator">,</a> <a id="4168" href="/20.07/Bisimulation/#4136" class="Bound">A</a> <a id="4170" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="4172" href="/20.07/Bisimulation/#4138" class="Bound">B</a><a id="4173" class="Symbol">}</a>
<a id="4179" class="Symbol">→</a> <a id="4181" href="/20.07/Bisimulation/#4142" class="Bound">M</a> <a id="4183" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="4185" href="/20.07/Bisimulation/#4144" class="Bound">M†</a>
<a id="4192" class="Symbol">→</a> <a id="4194" href="/20.07/Bisimulation/#4157" class="Bound">N</a> <a id="4196" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="4198" href="/20.07/Bisimulation/#4159" class="Bound">N†</a>
<a id="4207" class="Comment">----------------------</a>
<a id="4234" class="Symbol">→</a> <a id="4236" href="/20.07/More/#15609" class="InductiveConstructor">`let</a> <a id="4241" href="/20.07/Bisimulation/#4142" class="Bound">M</a> <a id="4243" href="/20.07/Bisimulation/#4157" class="Bound">N</a> <a id="4245" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="4247" class="Symbol">(</a><a id="4248" href="/20.07/More/#15035" class="InductiveConstructor Operator">ƛ</a> <a id="4250" href="/20.07/Bisimulation/#4159" class="Bound">N†</a><a id="4252" class="Symbol">)</a> <a id="4254" href="/20.07/More/#15103" class="InductiveConstructor Operator">·</a> <a id="4256" href="/20.07/Bisimulation/#4144" class="Bound">M†</a>
</pre>
<p>The language in Chapter <a href="/20.07/More/">More</a> 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.</p>
<h4 id="exercise-_-practice">Exercise <code class="language-plaintext highlighter-rouge">_†</code> (practice)</h4>
<p>Formalise the translation from source to target given in the introduction.
Show that <code class="language-plaintext highlighter-rouge">M † ≡ N</code> implies <code class="language-plaintext highlighter-rouge">M ~ N</code>, and conversely.</p>
<pre class="Agda"><a id="4741" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="simulation-commutes-with-values">Simulation commutes with values</h2>
<p>We need a number of technical results. The first is that simulation
commutes with values. That is, if <code class="language-plaintext highlighter-rouge">M ~ M†</code> and <code class="language-plaintext highlighter-rouge">M</code> is a value then
<code class="language-plaintext highlighter-rouge">M†</code> is also a value:</p>
<pre class="Agda"><a id="~val"></a><a id="4968" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="4973" class="Symbol">:</a> <a id="4975" class="Symbol">∀</a> <a id="4977" class="Symbol">{</a><a id="4978" href="/20.07/Bisimulation/#4978" class="Bound">Γ</a> <a id="4980" href="/20.07/Bisimulation/#4980" class="Bound">A</a><a id="4981" class="Symbol">}</a> <a id="4983" class="Symbol">{</a><a id="4984" href="/20.07/Bisimulation/#4984" class="Bound">M</a> <a id="4986" href="/20.07/Bisimulation/#4986" class="Bound">M†</a> <a id="4989" class="Symbol">:</a> <a id="4991" href="/20.07/Bisimulation/#4978" class="Bound">Γ</a> <a id="4993" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="4995" href="/20.07/Bisimulation/#4980" class="Bound">A</a><a id="4996" class="Symbol">}</a>
<a id="5000" class="Symbol">→</a> <a id="5002" href="/20.07/Bisimulation/#4984" class="Bound">M</a> <a id="5004" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="5006" href="/20.07/Bisimulation/#4986" class="Bound">M†</a>
<a id="5011" class="Symbol">→</a> <a id="5013" href="/20.07/More/#18894" class="Datatype">Value</a> <a id="5019" href="/20.07/Bisimulation/#4984" class="Bound">M</a>
<a id="5025" class="Comment">--------</a>
<a id="5036" class="Symbol">→</a> <a id="5038" href="/20.07/More/#18894" class="Datatype">Value</a> <a id="5044" href="/20.07/Bisimulation/#4986" class="Bound">M†</a>
<a id="5047" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="5052" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a> <a id="5065" class="Symbol">()</a>
<a id="5068" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="5073" class="Symbol">(</a><a id="5074" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ</a> <a id="5077" href="/20.07/Bisimulation/#5077" class="Bound">~N</a><a id="5079" class="Symbol">)</a> <a id="5086" href="/20.07/More/#18949" class="InductiveConstructor">V-ƛ</a> <a id="5091" class="Symbol">=</a> <a id="5094" href="/20.07/More/#18949" class="InductiveConstructor">V-ƛ</a>
<a id="5098" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="5103" class="Symbol">(</a><a id="5104" href="/20.07/Bisimulation/#5104" class="Bound">~L</a> <a id="5107" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="5110" href="/20.07/Bisimulation/#5110" class="Bound">~M</a><a id="5112" class="Symbol">)</a> <a id="5116" class="Symbol">()</a>
<a id="5119" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="5124" class="Symbol">(</a><a id="5125" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="5130" href="/20.07/Bisimulation/#5130" class="Bound">~M</a> <a id="5133" href="/20.07/Bisimulation/#5133" class="Bound">~N</a><a id="5135" class="Symbol">)</a> <a id="5137" class="Symbol">()</a>
</pre>
<p>It is a straightforward case analysis, where here the only value
of interest is a lambda abstraction.</p>
<h4 id="exercise-val-practice">Exercise <code class="language-plaintext highlighter-rouge">~val⁻¹</code> (practice)</h4>
<p>Show that this also holds in the reverse direction: if <code class="language-plaintext highlighter-rouge">M ~ M†</code>
and <code class="language-plaintext highlighter-rouge">Value M†</code> then <code class="language-plaintext highlighter-rouge">Value M</code>.</p>
<pre class="Agda"><a id="5382" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="simulation-commutes-with-renaming">Simulation commutes with renaming</h2>
<p>The next technical result is that simulation commutes with renaming.
That is, if <code class="language-plaintext highlighter-rouge">ρ</code> maps any judgment <code class="language-plaintext highlighter-rouge">Γ ∋ A</code> to a judgment <code class="language-plaintext highlighter-rouge">Δ ∋ A</code>,
and if <code class="language-plaintext highlighter-rouge">M ~ M†</code> then <code class="language-plaintext highlighter-rouge">rename ρ M ~ rename ρ M†</code>:</p>
<pre class="Agda"><a id="~rename"></a><a id="5637" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5645" class="Symbol">:</a> <a id="5647" class="Symbol">∀</a> <a id="5649" class="Symbol">{</a><a id="5650" href="/20.07/Bisimulation/#5650" class="Bound">Γ</a> <a id="5652" href="/20.07/Bisimulation/#5652" class="Bound">Δ</a><a id="5653" class="Symbol">}</a>
<a id="5657" class="Symbol">→</a> <a id="5659" class="Symbol">(</a><a id="5660" href="/20.07/Bisimulation/#5660" class="Bound">ρ</a> <a id="5662" class="Symbol">:</a> <a id="5664" class="Symbol">∀</a> <a id="5666" class="Symbol">{</a><a id="5667" href="/20.07/Bisimulation/#5667" class="Bound">A</a><a id="5668" class="Symbol">}</a> <a id="5670" class="Symbol">→</a> <a id="5672" href="/20.07/Bisimulation/#5650" class="Bound">Γ</a> <a id="5674" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="5676" href="/20.07/Bisimulation/#5667" class="Bound">A</a> <a id="5678" class="Symbol">→</a> <a id="5680" href="/20.07/Bisimulation/#5652" class="Bound">Δ</a> <a id="5682" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="5684" href="/20.07/Bisimulation/#5667" class="Bound">A</a><a id="5685" class="Symbol">)</a>
<a id="5691" class="Comment">----------------------------------------------------------</a>
<a id="5752" class="Symbol">→</a> <a id="5754" class="Symbol">(∀</a> <a id="5757" class="Symbol">{</a><a id="5758" href="/20.07/Bisimulation/#5758" class="Bound">A</a><a id="5759" class="Symbol">}</a> <a id="5761" class="Symbol">{</a><a id="5762" href="/20.07/Bisimulation/#5762" class="Bound">M</a> <a id="5764" href="/20.07/Bisimulation/#5764" class="Bound">M†</a> <a id="5767" class="Symbol">:</a> <a id="5769" href="/20.07/Bisimulation/#5650" class="Bound">Γ</a> <a id="5771" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="5773" href="/20.07/Bisimulation/#5758" class="Bound">A</a><a id="5774" class="Symbol">}</a> <a id="5776" class="Symbol">→</a> <a id="5778" href="/20.07/Bisimulation/#5762" class="Bound">M</a> <a id="5780" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="5782" href="/20.07/Bisimulation/#5764" class="Bound">M†</a> <a id="5785" class="Symbol">→</a> <a id="5787" href="/20.07/More/#16654" class="Function">rename</a> <a id="5794" href="/20.07/Bisimulation/#5660" class="Bound">ρ</a> <a id="5796" href="/20.07/Bisimulation/#5762" class="Bound">M</a> <a id="5798" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="5800" href="/20.07/More/#16654" class="Function">rename</a> <a id="5807" href="/20.07/Bisimulation/#5660" class="Bound">ρ</a> <a id="5809" href="/20.07/Bisimulation/#5764" class="Bound">M†</a><a id="5811" class="Symbol">)</a>
<a id="5813" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5821" href="/20.07/Bisimulation/#5821" class="Bound">ρ</a> <a id="5823" class="Symbol">(</a><a id="5824" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a><a id="5826" class="Symbol">)</a> <a id="5837" class="Symbol">=</a> <a id="5840" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a>
<a id="5843" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5851" href="/20.07/Bisimulation/#5851" class="Bound">ρ</a> <a id="5853" class="Symbol">(</a><a id="5854" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ</a> <a id="5857" href="/20.07/Bisimulation/#5857" class="Bound">~N</a><a id="5859" class="Symbol">)</a> <a id="5867" class="Symbol">=</a> <a id="5870" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ</a> <a id="5873" class="Symbol">(</a><a id="5874" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5882" class="Symbol">(</a><a id="5883" href="/20.07/More/#16535" class="Function">ext</a> <a id="5887" href="/20.07/Bisimulation/#5851" class="Bound">ρ</a><a id="5888" class="Symbol">)</a> <a id="5890" href="/20.07/Bisimulation/#5857" class="Bound">~N</a><a id="5892" class="Symbol">)</a>
<a id="5894" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5902" href="/20.07/Bisimulation/#5902" class="Bound">ρ</a> <a id="5904" class="Symbol">(</a><a id="5905" href="/20.07/Bisimulation/#5905" class="Bound">~L</a> <a id="5908" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="5911" href="/20.07/Bisimulation/#5911" class="Bound">~M</a><a id="5913" class="Symbol">)</a> <a id="5918" class="Symbol">=</a> <a id="5921" class="Symbol">(</a><a id="5922" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5930" href="/20.07/Bisimulation/#5902" class="Bound">ρ</a> <a id="5932" href="/20.07/Bisimulation/#5905" class="Bound">~L</a><a id="5934" class="Symbol">)</a> <a id="5936" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="5939" class="Symbol">(</a><a id="5940" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5948" href="/20.07/Bisimulation/#5902" class="Bound">ρ</a> <a id="5950" href="/20.07/Bisimulation/#5911" class="Bound">~M</a><a id="5952" class="Symbol">)</a>
<a id="5954" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5962" href="/20.07/Bisimulation/#5962" class="Bound">ρ</a> <a id="5964" class="Symbol">(</a><a id="5965" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="5970" href="/20.07/Bisimulation/#5970" class="Bound">~M</a> <a id="5973" href="/20.07/Bisimulation/#5973" class="Bound">~N</a><a id="5975" class="Symbol">)</a> <a id="5978" class="Symbol">=</a> <a id="5981" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="5986" class="Symbol">(</a><a id="5987" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="5995" href="/20.07/Bisimulation/#5962" class="Bound">ρ</a> <a id="5997" href="/20.07/Bisimulation/#5970" class="Bound">~M</a><a id="5999" class="Symbol">)</a> <a id="6001" class="Symbol">(</a><a id="6002" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="6010" class="Symbol">(</a><a id="6011" href="/20.07/More/#16535" class="Function">ext</a> <a id="6015" href="/20.07/Bisimulation/#5962" class="Bound">ρ</a><a id="6016" class="Symbol">)</a> <a id="6018" href="/20.07/Bisimulation/#5973" class="Bound">~N</a><a id="6020" class="Symbol">)</a>
</pre>
<p>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).</p>
<h2 id="simulation-commutes-with-substitution">Simulation commutes with substitution</h2>
<p>The third technical result is that simulation commutes with substitution.
It is more complex than renaming, because where we had one renaming map
<code class="language-plaintext highlighter-rouge">ρ</code> here we need two substitution maps, <code class="language-plaintext highlighter-rouge">σ</code> and <code class="language-plaintext highlighter-rouge">σ†</code>.</p>
<p>The proof first requires we establish an analogue of extension.
If <code class="language-plaintext highlighter-rouge">σ</code> and <code class="language-plaintext highlighter-rouge">σ†</code> both map any judgment <code class="language-plaintext highlighter-rouge">Γ ∋ A</code> to a judgment <code class="language-plaintext highlighter-rouge">Δ ⊢ A</code>,
such that for every <code class="language-plaintext highlighter-rouge">x</code> in <code class="language-plaintext highlighter-rouge">Γ ∋ A</code> we have <code class="language-plaintext highlighter-rouge">σ x ~ σ† x</code>,
then for any <code class="language-plaintext highlighter-rouge">x</code> in <code class="language-plaintext highlighter-rouge">Γ , B ∋ A</code> we have <code class="language-plaintext highlighter-rouge">exts σ x ~ exts σ† x</code>:</p>
<pre class="Agda"><a id="~exts"></a><a id="6750" href="/20.07/Bisimulation/#6750" class="Function">~exts</a> <a id="6756" class="Symbol">:</a> <a id="6758" class="Symbol">∀</a> <a id="6760" class="Symbol">{</a><a id="6761" href="/20.07/Bisimulation/#6761" class="Bound">Γ</a> <a id="6763" href="/20.07/Bisimulation/#6763" class="Bound">Δ</a><a id="6764" class="Symbol">}</a>
<a id="6768" class="Symbol">→</a> <a id="6770" class="Symbol">{</a><a id="6771" href="/20.07/Bisimulation/#6771" class="Bound">σ</a> <a id="6774" class="Symbol">:</a> <a id="6776" class="Symbol">∀</a> <a id="6778" class="Symbol">{</a><a id="6779" href="/20.07/Bisimulation/#6779" class="Bound">A</a><a id="6780" class="Symbol">}</a> <a id="6782" class="Symbol">→</a> <a id="6784" href="/20.07/Bisimulation/#6761" class="Bound">Γ</a> <a id="6786" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="6788" href="/20.07/Bisimulation/#6779" class="Bound">A</a> <a id="6790" class="Symbol">→</a> <a id="6792" href="/20.07/Bisimulation/#6763" class="Bound">Δ</a> <a id="6794" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="6796" href="/20.07/Bisimulation/#6779" class="Bound">A</a><a id="6797" class="Symbol">}</a>
<a id="6801" class="Symbol">→</a> <a id="6803" class="Symbol">{</a><a id="6804" href="/20.07/Bisimulation/#6804" class="Bound">σ†</a> <a id="6807" class="Symbol">:</a> <a id="6809" class="Symbol">∀</a> <a id="6811" class="Symbol">{</a><a id="6812" href="/20.07/Bisimulation/#6812" class="Bound">A</a><a id="6813" class="Symbol">}</a> <a id="6815" class="Symbol">→</a> <a id="6817" href="/20.07/Bisimulation/#6761" class="Bound">Γ</a> <a id="6819" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="6821" href="/20.07/Bisimulation/#6812" class="Bound">A</a> <a id="6823" class="Symbol">→</a> <a id="6825" href="/20.07/Bisimulation/#6763" class="Bound">Δ</a> <a id="6827" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="6829" href="/20.07/Bisimulation/#6812" class="Bound">A</a><a id="6830" class="Symbol">}</a>
<a id="6834" class="Symbol">→</a> <a id="6836" class="Symbol">(∀</a> <a id="6839" class="Symbol">{</a><a id="6840" href="/20.07/Bisimulation/#6840" class="Bound">A</a><a id="6841" class="Symbol">}</a> <a id="6843" class="Symbol">→</a> <a id="6845" class="Symbol">(</a><a id="6846" href="/20.07/Bisimulation/#6846" class="Bound">x</a> <a id="6848" class="Symbol">:</a> <a id="6850" href="/20.07/Bisimulation/#6761" class="Bound">Γ</a> <a id="6852" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="6854" href="/20.07/Bisimulation/#6840" class="Bound">A</a><a id="6855" class="Symbol">)</a> <a id="6857" class="Symbol">→</a> <a id="6859" href="/20.07/Bisimulation/#6771" class="Bound">σ</a> <a id="6861" href="/20.07/Bisimulation/#6846" class="Bound">x</a> <a id="6863" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="6865" href="/20.07/Bisimulation/#6804" class="Bound">σ†</a> <a id="6868" href="/20.07/Bisimulation/#6846" class="Bound">x</a><a id="6869" class="Symbol">)</a>
<a id="6875" class="Comment">--------------------------------------------------</a>
<a id="6928" class="Symbol">→</a> <a id="6930" class="Symbol">(∀</a> <a id="6933" class="Symbol">{</a><a id="6934" href="/20.07/Bisimulation/#6934" class="Bound">A</a> <a id="6936" href="/20.07/Bisimulation/#6936" class="Bound">B</a><a id="6937" class="Symbol">}</a> <a id="6939" class="Symbol">→</a> <a id="6941" class="Symbol">(</a><a id="6942" href="/20.07/Bisimulation/#6942" class="Bound">x</a> <a id="6944" class="Symbol">:</a> <a id="6946" href="/20.07/Bisimulation/#6761" class="Bound">Γ</a> <a id="6948" href="/20.07/More/#14640" class="InductiveConstructor Operator">,</a> <a id="6950" href="/20.07/Bisimulation/#6936" class="Bound">B</a> <a id="6952" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="6954" href="/20.07/Bisimulation/#6934" class="Bound">A</a><a id="6955" class="Symbol">)</a> <a id="6957" class="Symbol">→</a> <a id="6959" href="/20.07/More/#17473" class="Function">exts</a> <a id="6964" href="/20.07/Bisimulation/#6771" class="Bound">σ</a> <a id="6966" href="/20.07/Bisimulation/#6942" class="Bound">x</a> <a id="6968" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="6970" href="/20.07/More/#17473" class="Function">exts</a> <a id="6975" href="/20.07/Bisimulation/#6804" class="Bound">σ†</a> <a id="6978" href="/20.07/Bisimulation/#6942" class="Bound">x</a><a id="6979" class="Symbol">)</a>
<a id="6981" href="/20.07/Bisimulation/#6750" class="Function">~exts</a> <a id="6987" href="/20.07/Bisimulation/#6987" class="Bound">~σ</a> <a id="6990" href="/20.07/More/#14760" class="InductiveConstructor">Z</a> <a id="6997" class="Symbol">=</a> <a id="7000" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a>
<a id="7003" href="/20.07/Bisimulation/#6750" class="Function">~exts</a> <a id="7009" href="/20.07/Bisimulation/#7009" class="Bound">~σ</a> <a id="7012" class="Symbol">(</a><a id="7013" href="/20.07/More/#14807" class="InductiveConstructor Operator">S</a> <a id="7015" href="/20.07/Bisimulation/#7015" class="Bound">x</a><a id="7016" class="Symbol">)</a> <a id="7019" class="Symbol">=</a> <a id="7022" href="/20.07/Bisimulation/#5637" class="Function">~rename</a> <a id="7030" href="/20.07/More/#14807" class="InductiveConstructor Operator">S_</a> <a id="7033" class="Symbol">(</a><a id="7034" href="/20.07/Bisimulation/#7009" class="Bound">~σ</a> <a id="7037" href="/20.07/Bisimulation/#7015" class="Bound">x</a><a id="7038" class="Symbol">)</a>
</pre>
<p>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.</p>
<p>With extension under our belts, it is straightforward to show
substitution commutes. If <code class="language-plaintext highlighter-rouge">σ</code> and <code class="language-plaintext highlighter-rouge">σ†</code> both map any judgment <code class="language-plaintext highlighter-rouge">Γ ∋ A</code>
to a judgment <code class="language-plaintext highlighter-rouge">Δ ⊢ A</code>, such that for every <code class="language-plaintext highlighter-rouge">x</code> in <code class="language-plaintext highlighter-rouge">Γ ∋ A</code> we have <code class="language-plaintext highlighter-rouge">σ
x ~ σ† x</code>, and if <code class="language-plaintext highlighter-rouge">M ~ M†</code>, then <code class="language-plaintext highlighter-rouge">subst σ M ~ subst σ† M†</code>:</p>
<pre class="Agda"><a id="~subst"></a><a id="7496" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7503" class="Symbol">:</a> <a id="7505" class="Symbol">∀</a> <a id="7507" class="Symbol">{</a><a id="7508" href="/20.07/Bisimulation/#7508" class="Bound">Γ</a> <a id="7510" href="/20.07/Bisimulation/#7510" class="Bound">Δ</a><a id="7511" class="Symbol">}</a>
<a id="7515" class="Symbol">→</a> <a id="7517" class="Symbol">{</a><a id="7518" href="/20.07/Bisimulation/#7518" class="Bound">σ</a> <a id="7521" class="Symbol">:</a> <a id="7523" class="Symbol">∀</a> <a id="7525" class="Symbol">{</a><a id="7526" href="/20.07/Bisimulation/#7526" class="Bound">A</a><a id="7527" class="Symbol">}</a> <a id="7529" class="Symbol">→</a> <a id="7531" href="/20.07/Bisimulation/#7508" class="Bound">Γ</a> <a id="7533" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="7535" href="/20.07/Bisimulation/#7526" class="Bound">A</a> <a id="7537" class="Symbol">→</a> <a id="7539" href="/20.07/Bisimulation/#7510" class="Bound">Δ</a> <a id="7541" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="7543" href="/20.07/Bisimulation/#7526" class="Bound">A</a><a id="7544" class="Symbol">}</a>
<a id="7548" class="Symbol">→</a> <a id="7550" class="Symbol">{</a><a id="7551" href="/20.07/Bisimulation/#7551" class="Bound">σ†</a> <a id="7554" class="Symbol">:</a> <a id="7556" class="Symbol">∀</a> <a id="7558" class="Symbol">{</a><a id="7559" href="/20.07/Bisimulation/#7559" class="Bound">A</a><a id="7560" class="Symbol">}</a> <a id="7562" class="Symbol">→</a> <a id="7564" href="/20.07/Bisimulation/#7508" class="Bound">Γ</a> <a id="7566" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="7568" href="/20.07/Bisimulation/#7559" class="Bound">A</a> <a id="7570" class="Symbol">→</a> <a id="7572" href="/20.07/Bisimulation/#7510" class="Bound">Δ</a> <a id="7574" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="7576" href="/20.07/Bisimulation/#7559" class="Bound">A</a><a id="7577" class="Symbol">}</a>
<a id="7581" class="Symbol">→</a> <a id="7583" class="Symbol">(∀</a> <a id="7586" class="Symbol">{</a><a id="7587" href="/20.07/Bisimulation/#7587" class="Bound">A</a><a id="7588" class="Symbol">}</a> <a id="7590" class="Symbol">→</a> <a id="7592" class="Symbol">(</a><a id="7593" href="/20.07/Bisimulation/#7593" class="Bound">x</a> <a id="7595" class="Symbol">:</a> <a id="7597" href="/20.07/Bisimulation/#7508" class="Bound">Γ</a> <a id="7599" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="7601" href="/20.07/Bisimulation/#7587" class="Bound">A</a><a id="7602" class="Symbol">)</a> <a id="7604" class="Symbol">→</a> <a id="7606" href="/20.07/Bisimulation/#7518" class="Bound">σ</a> <a id="7608" href="/20.07/Bisimulation/#7593" class="Bound">x</a> <a id="7610" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="7612" href="/20.07/Bisimulation/#7551" class="Bound">σ†</a> <a id="7615" href="/20.07/Bisimulation/#7593" class="Bound">x</a><a id="7616" class="Symbol">)</a>
<a id="7622" class="Comment">---------------------------------------------------------</a>
<a id="7682" class="Symbol">→</a> <a id="7684" class="Symbol">(∀</a> <a id="7687" class="Symbol">{</a><a id="7688" href="/20.07/Bisimulation/#7688" class="Bound">A</a><a id="7689" class="Symbol">}</a> <a id="7691" class="Symbol">{</a><a id="7692" href="/20.07/Bisimulation/#7692" class="Bound">M</a> <a id="7694" href="/20.07/Bisimulation/#7694" class="Bound">M†</a> <a id="7697" class="Symbol">:</a> <a id="7699" href="/20.07/Bisimulation/#7508" class="Bound">Γ</a> <a id="7701" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="7703" href="/20.07/Bisimulation/#7688" class="Bound">A</a><a id="7704" class="Symbol">}</a> <a id="7706" class="Symbol">→</a> <a id="7708" href="/20.07/Bisimulation/#7692" class="Bound">M</a> <a id="7710" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="7712" href="/20.07/Bisimulation/#7694" class="Bound">M†</a> <a id="7715" class="Symbol">→</a> <a id="7717" href="/20.07/More/#17605" class="Function">subst</a> <a id="7723" href="/20.07/Bisimulation/#7518" class="Bound">σ</a> <a id="7725" href="/20.07/Bisimulation/#7692" class="Bound">M</a> <a id="7727" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="7729" href="/20.07/More/#17605" class="Function">subst</a> <a id="7735" href="/20.07/Bisimulation/#7551" class="Bound">σ†</a> <a id="7738" href="/20.07/Bisimulation/#7694" class="Bound">M†</a><a id="7740" class="Symbol">)</a>
<a id="7742" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7749" href="/20.07/Bisimulation/#7749" class="Bound">~σ</a> <a id="7752" class="Symbol">(</a><a id="7753" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a> <a id="7756" class="Symbol">{</a><a id="7757" class="Argument">x</a> <a id="7759" class="Symbol">=</a> <a id="7761" href="/20.07/Bisimulation/#7761" class="Bound">x</a><a id="7762" class="Symbol">})</a> <a id="7766" class="Symbol">=</a> <a id="7769" href="/20.07/Bisimulation/#7749" class="Bound">~σ</a> <a id="7772" href="/20.07/Bisimulation/#7761" class="Bound">x</a>
<a id="7774" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7781" href="/20.07/Bisimulation/#7781" class="Bound">~σ</a> <a id="7784" class="Symbol">(</a><a id="7785" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ</a> <a id="7788" href="/20.07/Bisimulation/#7788" class="Bound">~N</a><a id="7790" class="Symbol">)</a> <a id="7798" class="Symbol">=</a> <a id="7801" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ</a> <a id="7804" class="Symbol">(</a><a id="7805" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7812" class="Symbol">(</a><a id="7813" href="/20.07/Bisimulation/#6750" class="Function">~exts</a> <a id="7819" href="/20.07/Bisimulation/#7781" class="Bound">~σ</a><a id="7821" class="Symbol">)</a> <a id="7823" href="/20.07/Bisimulation/#7788" class="Bound">~N</a><a id="7825" class="Symbol">)</a>
<a id="7827" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7834" href="/20.07/Bisimulation/#7834" class="Bound">~σ</a> <a id="7837" class="Symbol">(</a><a id="7838" href="/20.07/Bisimulation/#7838" class="Bound">~L</a> <a id="7841" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="7844" href="/20.07/Bisimulation/#7844" class="Bound">~M</a><a id="7846" class="Symbol">)</a> <a id="7851" class="Symbol">=</a> <a id="7854" class="Symbol">(</a><a id="7855" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7862" href="/20.07/Bisimulation/#7834" class="Bound">~σ</a> <a id="7865" href="/20.07/Bisimulation/#7838" class="Bound">~L</a><a id="7867" class="Symbol">)</a> <a id="7869" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="7872" class="Symbol">(</a><a id="7873" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7880" href="/20.07/Bisimulation/#7834" class="Bound">~σ</a> <a id="7883" href="/20.07/Bisimulation/#7844" class="Bound">~M</a><a id="7885" class="Symbol">)</a>
<a id="7887" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7894" href="/20.07/Bisimulation/#7894" class="Bound">~σ</a> <a id="7897" class="Symbol">(</a><a id="7898" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="7903" href="/20.07/Bisimulation/#7903" class="Bound">~M</a> <a id="7906" href="/20.07/Bisimulation/#7906" class="Bound">~N</a><a id="7908" class="Symbol">)</a> <a id="7911" class="Symbol">=</a> <a id="7914" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="7919" class="Symbol">(</a><a id="7920" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7927" href="/20.07/Bisimulation/#7894" class="Bound">~σ</a> <a id="7930" href="/20.07/Bisimulation/#7903" class="Bound">~M</a><a id="7932" class="Symbol">)</a> <a id="7934" class="Symbol">(</a><a id="7935" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="7942" class="Symbol">(</a><a id="7943" href="/20.07/Bisimulation/#6750" class="Function">~exts</a> <a id="7949" href="/20.07/Bisimulation/#7894" class="Bound">~σ</a><a id="7951" class="Symbol">)</a> <a id="7953" href="/20.07/Bisimulation/#7906" class="Bound">~N</a><a id="7955" class="Symbol">)</a>
</pre>
<p>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).</p>
<p>From the general case of substitution, it is also easy to derive
the required special case. If <code class="language-plaintext highlighter-rouge">N ~ N†</code> and <code class="language-plaintext highlighter-rouge">M ~ M†</code>, then
<code class="language-plaintext highlighter-rouge">N [ M ] ~ N† [ M† ]</code>:</p>
<pre class="Agda"><a id="~sub"></a><a id="8345" href="/20.07/Bisimulation/#8345" class="Function">~sub</a> <a id="8350" class="Symbol">:</a> <a id="8352" class="Symbol">∀</a> <a id="8354" class="Symbol">{</a><a id="8355" href="/20.07/Bisimulation/#8355" class="Bound">Γ</a> <a id="8357" href="/20.07/Bisimulation/#8357" class="Bound">A</a> <a id="8359" href="/20.07/Bisimulation/#8359" class="Bound">B</a><a id="8360" class="Symbol">}</a> <a id="8362" class="Symbol">{</a><a id="8363" href="/20.07/Bisimulation/#8363" class="Bound">N</a> <a id="8365" href="/20.07/Bisimulation/#8365" class="Bound">N†</a> <a id="8368" class="Symbol">:</a> <a id="8370" href="/20.07/Bisimulation/#8355" class="Bound">Γ</a> <a id="8372" href="/20.07/More/#14640" class="InductiveConstructor Operator">,</a> <a id="8374" href="/20.07/Bisimulation/#8359" class="Bound">B</a> <a id="8376" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="8378" href="/20.07/Bisimulation/#8357" class="Bound">A</a><a id="8379" class="Symbol">}</a> <a id="8381" class="Symbol">{</a><a id="8382" href="/20.07/Bisimulation/#8382" class="Bound">M</a> <a id="8384" href="/20.07/Bisimulation/#8384" class="Bound">M†</a> <a id="8387" class="Symbol">:</a> <a id="8389" href="/20.07/Bisimulation/#8355" class="Bound">Γ</a> <a id="8391" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="8393" href="/20.07/Bisimulation/#8359" class="Bound">B</a><a id="8394" class="Symbol">}</a>
<a id="8398" class="Symbol">→</a> <a id="8400" href="/20.07/Bisimulation/#8363" class="Bound">N</a> <a id="8402" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="8404" href="/20.07/Bisimulation/#8365" class="Bound">N†</a>
<a id="8409" class="Symbol">→</a> <a id="8411" href="/20.07/Bisimulation/#8382" class="Bound">M</a> <a id="8413" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="8415" href="/20.07/Bisimulation/#8384" class="Bound">M†</a>
<a id="8422" class="Comment">-----------------------</a>
<a id="8448" class="Symbol">→</a> <a id="8450" class="Symbol">(</a><a id="8451" href="/20.07/Bisimulation/#8363" class="Bound">N</a> <a id="8453" href="/20.07/More/#18500" class="Function Operator">[</a> <a id="8455" href="/20.07/Bisimulation/#8382" class="Bound">M</a> <a id="8457" href="/20.07/More/#18500" class="Function Operator">]</a><a id="8458" class="Symbol">)</a> <a id="8460" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="8462" class="Symbol">(</a><a id="8463" href="/20.07/Bisimulation/#8365" class="Bound">N†</a> <a id="8466" href="/20.07/More/#18500" class="Function Operator">[</a> <a id="8468" href="/20.07/Bisimulation/#8384" class="Bound">M†</a> <a id="8471" href="/20.07/More/#18500" class="Function Operator">]</a><a id="8472" class="Symbol">)</a>
<a id="8474" href="/20.07/Bisimulation/#8345" class="Function">~sub</a> <a id="8479" class="Symbol">{</a><a id="8480" href="/20.07/Bisimulation/#8480" class="Bound">Γ</a><a id="8481" class="Symbol">}</a> <a id="8483" class="Symbol">{</a><a id="8484" href="/20.07/Bisimulation/#8484" class="Bound">A</a><a id="8485" class="Symbol">}</a> <a id="8487" class="Symbol">{</a><a id="8488" href="/20.07/Bisimulation/#8488" class="Bound">B</a><a id="8489" class="Symbol">}</a> <a id="8491" href="/20.07/Bisimulation/#8491" class="Bound">~N</a> <a id="8494" href="/20.07/Bisimulation/#8494" class="Bound">~M</a> <a id="8497" class="Symbol">=</a> <a id="8499" href="/20.07/Bisimulation/#7496" class="Function">~subst</a> <a id="8506" class="Symbol">{</a><a id="8507" href="/20.07/Bisimulation/#8480" class="Bound">Γ</a> <a id="8509" href="/20.07/More/#14640" class="InductiveConstructor Operator">,</a> <a id="8511" href="/20.07/Bisimulation/#8488" class="Bound">B</a><a id="8512" class="Symbol">}</a> <a id="8514" class="Symbol">{</a><a id="8515" href="/20.07/Bisimulation/#8480" class="Bound">Γ</a><a id="8516" class="Symbol">}</a> <a id="8518" href="/20.07/Bisimulation/#8538" class="Function">~σ</a> <a id="8521" class="Symbol">{</a><a id="8522" href="/20.07/Bisimulation/#8484" class="Bound">A</a><a id="8523" class="Symbol">}</a> <a id="8525" href="/20.07/Bisimulation/#8491" class="Bound">~N</a>
<a id="8530" class="Keyword">where</a>
<a id="8538" href="/20.07/Bisimulation/#8538" class="Function">~σ</a> <a id="8541" class="Symbol">:</a> <a id="8543" class="Symbol">∀</a> <a id="8545" class="Symbol">{</a><a id="8546" href="/20.07/Bisimulation/#8546" class="Bound">A</a><a id="8547" class="Symbol">}</a> <a id="8549" class="Symbol">→</a> <a id="8551" class="Symbol">(</a><a id="8552" href="/20.07/Bisimulation/#8552" class="Bound">x</a> <a id="8554" class="Symbol">:</a> <a id="8556" href="/20.07/Bisimulation/#8480" class="Bound">Γ</a> <a id="8558" href="/20.07/More/#14640" class="InductiveConstructor Operator">,</a> <a id="8560" href="/20.07/Bisimulation/#8488" class="Bound">B</a> <a id="8562" href="/20.07/More/#14724" class="Datatype Operator">∋</a> <a id="8564" href="/20.07/Bisimulation/#8546" class="Bound">A</a><a id="8565" class="Symbol">)</a> <a id="8567" class="Symbol">→</a> <a id="8569" class="Symbol">_</a> <a id="8571" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="8573" class="Symbol">_</a>
<a id="8577" href="/20.07/Bisimulation/#8538" class="Function">~σ</a> <a id="8580" href="/20.07/More/#14760" class="InductiveConstructor">Z</a> <a id="8587" class="Symbol">=</a> <a id="8590" href="/20.07/Bisimulation/#8494" class="Bound">~M</a>
<a id="8595" href="/20.07/Bisimulation/#8538" class="Function">~σ</a> <a id="8598" class="Symbol">(</a><a id="8599" href="/20.07/More/#14807" class="InductiveConstructor Operator">S</a> <a id="8601" href="/20.07/Bisimulation/#8601" class="Bound">x</a><a id="8602" class="Symbol">)</a> <a id="8605" class="Symbol">=</a> <a id="8608" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a>
</pre>
<p>Once more, the structure of the proof resembles the original.</p>
<h2 id="the-relation-is-a-simulation">The relation is a simulation</h2>
<p>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:</p>
<p><em>Lock-step simulation</em>: For every <code class="language-plaintext highlighter-rouge">M</code>, <code class="language-plaintext highlighter-rouge">M†</code>, and <code class="language-plaintext highlighter-rouge">N</code>:
If <code class="language-plaintext highlighter-rouge">M ~ M†</code> and <code class="language-plaintext highlighter-rouge">M —→ N</code>
then <code class="language-plaintext highlighter-rouge">M† —→ N†</code> and <code class="language-plaintext highlighter-rouge">N ~ N†</code>
for some <code class="language-plaintext highlighter-rouge">N†</code>.</p>
<p>Or, in a diagram:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M --- —→ --- N
| |
| |
~ ~
| |
| |
M† --- —→ --- N†
</code></pre></div></div>
<p>We first formulate a concept corresponding to the lower leg
of the diagram, that is, its right and bottom edges:</p>
<pre class="Agda"><a id="9277" class="Keyword">data</a> <a id="Leg"></a><a id="9282" href="/20.07/Bisimulation/#9282" class="Datatype">Leg</a> <a id="9286" class="Symbol">{</a><a id="9287" href="/20.07/Bisimulation/#9287" class="Bound">Γ</a> <a id="9289" href="/20.07/Bisimulation/#9289" class="Bound">A</a><a id="9290" class="Symbol">}</a> <a id="9292" class="Symbol">(</a><a id="9293" href="/20.07/Bisimulation/#9293" class="Bound">M†</a> <a id="9296" href="/20.07/Bisimulation/#9296" class="Bound">N</a> <a id="9298" class="Symbol">:</a> <a id="9300" href="/20.07/Bisimulation/#9287" class="Bound">Γ</a> <a id="9302" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="9304" href="/20.07/Bisimulation/#9289" class="Bound">A</a><a id="9305" class="Symbol">)</a> <a id="9307" class="Symbol">:</a> <a id="9309" class="PrimitiveType">Set</a> <a id="9313" class="Keyword">where</a>
<a id="Leg.leg"></a><a id="9322" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="9326" class="Symbol">:</a> <a id="9328" class="Symbol">∀</a> <a id="9330" class="Symbol">{</a><a id="9331" href="/20.07/Bisimulation/#9331" class="Bound">N†</a> <a id="9334" class="Symbol">:</a> <a id="9336" href="/20.07/Bisimulation/#9287" class="Bound">Γ</a> <a id="9338" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="9340" href="/20.07/Bisimulation/#9289" class="Bound">A</a><a id="9341" class="Symbol">}</a>
<a id="9347" class="Symbol">→</a> <a id="9349" href="/20.07/Bisimulation/#9296" class="Bound">N</a> <a id="9351" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="9353" href="/20.07/Bisimulation/#9331" class="Bound">N†</a>
<a id="9360" class="Symbol">→</a> <a id="9362" href="/20.07/Bisimulation/#9293" class="Bound">M†</a> <a id="9365" href="/20.07/More/#19551" class="Datatype Operator">—→</a> <a id="9368" href="/20.07/Bisimulation/#9331" class="Bound">N†</a>
<a id="9377" class="Comment">--------</a>
<a id="9390" class="Symbol">→</a> <a id="9392" href="/20.07/Bisimulation/#9282" class="Datatype">Leg</a> <a id="9396" href="/20.07/Bisimulation/#9293" class="Bound">M†</a> <a id="9399" href="/20.07/Bisimulation/#9296" class="Bound">N</a>
</pre>
<p>For our formalisation, in this case, we can use a stronger
relation than <code class="language-plaintext highlighter-rouge">—↠</code>, replacing it by <code class="language-plaintext highlighter-rouge">—→</code>.</p>
<p>We can now state and prove that the relation is a simulation.
Again, in this case, we can use a stronger relation than
<code class="language-plaintext highlighter-rouge">—↠</code>, replacing it by <code class="language-plaintext highlighter-rouge">—→</code>:</p>
<pre class="Agda"><a id="sim"></a><a id="9658" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="9662" class="Symbol">:</a> <a id="9664" class="Symbol">∀</a> <a id="9666" class="Symbol">{</a><a id="9667" href="/20.07/Bisimulation/#9667" class="Bound">Γ</a> <a id="9669" href="/20.07/Bisimulation/#9669" class="Bound">A</a><a id="9670" class="Symbol">}</a> <a id="9672" class="Symbol">{</a><a id="9673" href="/20.07/Bisimulation/#9673" class="Bound">M</a> <a id="9675" href="/20.07/Bisimulation/#9675" class="Bound">M†</a> <a id="9678" href="/20.07/Bisimulation/#9678" class="Bound">N</a> <a id="9680" class="Symbol">:</a> <a id="9682" href="/20.07/Bisimulation/#9667" class="Bound">Γ</a> <a id="9684" href="/20.07/More/#14915" class="Datatype Operator">⊢</a> <a id="9686" href="/20.07/Bisimulation/#9669" class="Bound">A</a><a id="9687" class="Symbol">}</a>
<a id="9691" class="Symbol">→</a> <a id="9693" href="/20.07/Bisimulation/#9673" class="Bound">M</a> <a id="9695" href="/20.07/Bisimulation/#3808" class="Datatype Operator">~</a> <a id="9697" href="/20.07/Bisimulation/#9675" class="Bound">M†</a>
<a id="9702" class="Symbol">→</a> <a id="9704" href="/20.07/Bisimulation/#9673" class="Bound">M</a> <a id="9706" href="/20.07/More/#19551" class="Datatype Operator">—→</a> <a id="9709" href="/20.07/Bisimulation/#9678" class="Bound">N</a>
<a id="9715" class="Comment">---------</a>
<a id="9727" class="Symbol">→</a> <a id="9729" href="/20.07/Bisimulation/#9282" class="Datatype">Leg</a> <a id="9734" href="/20.07/Bisimulation/#9675" class="Bound">M†</a> <a id="9737" href="/20.07/Bisimulation/#9678" class="Bound">N</a>
<a id="9739" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="9743" href="/20.07/Bisimulation/#3857" class="InductiveConstructor">~`</a> <a id="9759" class="Symbol">()</a>
<a id="9762" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="9766" class="Symbol">(</a><a id="9767" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ</a> <a id="9770" href="/20.07/Bisimulation/#9770" class="Bound">~N</a><a id="9772" class="Symbol">)</a> <a id="9782" class="Symbol">()</a>
<a id="9785" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="9789" class="Symbol">(</a><a id="9790" href="/20.07/Bisimulation/#9790" class="Bound">~L</a> <a id="9793" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="9796" href="/20.07/Bisimulation/#9796" class="Bound">~M</a><a id="9798" class="Symbol">)</a> <a id="9805" class="Symbol">(</a><a id="9806" href="/20.07/More/#19617" class="InductiveConstructor">ξ-·₁</a> <a id="9811" href="/20.07/Bisimulation/#9811" class="Bound">L—→</a><a id="9814" class="Symbol">)</a>
<a id="9818" class="Keyword">with</a> <a id="9823" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="9827" href="/20.07/Bisimulation/#9790" class="Bound">~L</a> <a id="9830" href="/20.07/Bisimulation/#9811" class="Bound">L—→</a>
<a id="9834" class="Symbol">...</a> <a id="9839" class="Symbol">|</a> <a id="9841" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="9845" href="/20.07/Bisimulation/#9845" class="Bound">~L′</a> <a id="9849" href="/20.07/Bisimulation/#9849" class="Bound">L†—→</a> <a id="9870" class="Symbol">=</a> <a id="9873" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="9877" class="Symbol">(</a><a id="9878" href="/20.07/Bisimulation/#9845" class="Bound">~L′</a> <a id="9882" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="9885" class="Bound">~M</a><a id="9887" class="Symbol">)</a> <a id="9891" class="Symbol">(</a><a id="9892" href="/20.07/More/#19617" class="InductiveConstructor">ξ-·₁</a> <a id="9897" href="/20.07/Bisimulation/#9849" class="Bound">L†—→</a><a id="9901" class="Symbol">)</a>
<a id="9903" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="9907" class="Symbol">(</a><a id="9908" href="/20.07/Bisimulation/#9908" class="Bound">~V</a> <a id="9911" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="9914" href="/20.07/Bisimulation/#9914" class="Bound">~M</a><a id="9916" class="Symbol">)</a> <a id="9923" class="Symbol">(</a><a id="9924" href="/20.07/More/#19726" class="InductiveConstructor">ξ-·₂</a> <a id="9929" href="/20.07/Bisimulation/#9929" class="Bound">VV</a> <a id="9932" href="/20.07/Bisimulation/#9932" class="Bound">M—→</a><a id="9935" class="Symbol">)</a>
<a id="9939" class="Keyword">with</a> <a id="9944" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="9948" href="/20.07/Bisimulation/#9914" class="Bound">~M</a> <a id="9951" href="/20.07/Bisimulation/#9932" class="Bound">M—→</a>
<a id="9955" class="Symbol">...</a> <a id="9960" class="Symbol">|</a> <a id="9962" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="9966" href="/20.07/Bisimulation/#9966" class="Bound">~M′</a> <a id="9970" href="/20.07/Bisimulation/#9970" class="Bound">M†—→</a> <a id="9991" class="Symbol">=</a> <a id="9994" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="9998" class="Symbol">(</a><a id="9999" class="Bound">~V</a> <a id="10002" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="10005" href="/20.07/Bisimulation/#9966" class="Bound">~M′</a><a id="10008" class="Symbol">)</a> <a id="10012" class="Symbol">(</a><a id="10013" href="/20.07/More/#19726" class="InductiveConstructor">ξ-·₂</a> <a id="10018" class="Symbol">(</a><a id="10019" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="10024" class="Bound">~V</a> <a id="10027" class="Bound">VV</a><a id="10029" class="Symbol">)</a> <a id="10031" href="/20.07/Bisimulation/#9970" class="Bound">M†—→</a><a id="10035" class="Symbol">)</a>
<a id="10037" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="10041" class="Symbol">((</a><a id="10043" href="/20.07/Bisimulation/#3915" class="InductiveConstructor Operator">~ƛ</a> <a id="10046" href="/20.07/Bisimulation/#10046" class="Bound">~N</a><a id="10048" class="Symbol">)</a> <a id="10050" href="/20.07/Bisimulation/#4000" class="InductiveConstructor Operator">~·</a> <a id="10053" href="/20.07/Bisimulation/#10053" class="Bound">~V</a><a id="10055" class="Symbol">)</a> <a id="10057" class="Symbol">(</a><a id="10058" href="/20.07/More/#19849" class="InductiveConstructor">β-ƛ</a> <a id="10062" href="/20.07/Bisimulation/#10062" class="Bound">VV</a><a id="10064" class="Symbol">)</a> <a id="10073" class="Symbol">=</a> <a id="10076" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="10080" class="Symbol">(</a><a id="10081" href="/20.07/Bisimulation/#8345" class="Function">~sub</a> <a id="10086" href="/20.07/Bisimulation/#10046" class="Bound">~N</a> <a id="10089" href="/20.07/Bisimulation/#10053" class="Bound">~V</a><a id="10091" class="Symbol">)</a> <a id="10094" class="Symbol">(</a><a id="10095" href="/20.07/More/#19849" class="InductiveConstructor">β-ƛ</a> <a id="10099" class="Symbol">(</a><a id="10100" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="10105" href="/20.07/Bisimulation/#10053" class="Bound">~V</a> <a id="10108" href="/20.07/Bisimulation/#10062" class="Bound">VV</a><a id="10110" class="Symbol">))</a>
<a id="10113" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="10117" class="Symbol">(</a><a id="10118" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="10123" href="/20.07/Bisimulation/#10123" class="Bound">~M</a> <a id="10126" href="/20.07/Bisimulation/#10126" class="Bound">~N</a><a id="10128" class="Symbol">)</a> <a id="10133" class="Symbol">(</a><a id="10134" href="/20.07/More/#20899" class="InductiveConstructor">ξ-let</a> <a id="10140" href="/20.07/Bisimulation/#10140" class="Bound">M—→</a><a id="10143" class="Symbol">)</a>
<a id="10147" class="Keyword">with</a> <a id="10152" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="10156" href="/20.07/Bisimulation/#10123" class="Bound">~M</a> <a id="10159" href="/20.07/Bisimulation/#10140" class="Bound">M—→</a>
<a id="10163" class="Symbol">...</a> <a id="10168" class="Symbol">|</a> <a id="10170" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="10174" href="/20.07/Bisimulation/#10174" class="Bound">~M′</a> <a id="10178" href="/20.07/Bisimulation/#10178" class="Bound">M†—→</a> <a id="10199" class="Symbol">=</a> <a id="10202" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="10206" class="Symbol">(</a><a id="10207" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="10212" href="/20.07/Bisimulation/#10174" class="Bound">~M′</a> <a id="10216" class="Bound">~N</a><a id="10218" class="Symbol">)</a> <a id="10220" class="Symbol">(</a><a id="10221" href="/20.07/More/#19726" class="InductiveConstructor">ξ-·₂</a> <a id="10226" href="/20.07/More/#18949" class="InductiveConstructor">V-ƛ</a> <a id="10230" href="/20.07/Bisimulation/#10178" class="Bound">M†—→</a><a id="10234" class="Symbol">)</a>
<a id="10236" href="/20.07/Bisimulation/#9658" class="Function">sim</a> <a id="10240" class="Symbol">(</a><a id="10241" href="/20.07/Bisimulation/#4124" class="InductiveConstructor">~let</a> <a id="10246" href="/20.07/Bisimulation/#10246" class="Bound">~V</a> <a id="10249" href="/20.07/Bisimulation/#10249" class="Bound">~N</a><a id="10251" class="Symbol">)</a> <a id="10256" class="Symbol">(</a><a id="10257" href="/20.07/More/#21021" class="InductiveConstructor">β-let</a> <a id="10263" href="/20.07/Bisimulation/#10263" class="Bound">VV</a><a id="10265" class="Symbol">)</a> <a id="10272" class="Symbol">=</a> <a id="10275" href="/20.07/Bisimulation/#9322" class="InductiveConstructor">leg</a> <a id="10279" class="Symbol">(</a><a id="10280" href="/20.07/Bisimulation/#8345" class="Function">~sub</a> <a id="10285" href="/20.07/Bisimulation/#10249" class="Bound">~N</a> <a id="10288" href="/20.07/Bisimulation/#10246" class="Bound">~V</a><a id="10290" class="Symbol">)</a> <a id="10293" class="Symbol">(</a><a id="10294" href="/20.07/More/#19849" class="InductiveConstructor">β-ƛ</a> <a id="10298" class="Symbol">(</a><a id="10299" href="/20.07/Bisimulation/#4968" class="Function">~val</a> <a id="10304" href="/20.07/Bisimulation/#10246" class="Bound">~V</a> <a id="10307" href="/20.07/Bisimulation/#10263" class="Bound">VV</a><a id="10309" class="Symbol">))</a>
</pre>
<p>The proof is by case analysis, examining each possible instance of <code class="language-plaintext highlighter-rouge">M ~ M†</code>
and each possible instance of <code class="language-plaintext highlighter-rouge">M —→ M†</code>, using recursive invocation whenever
the reduction is by a <code class="language-plaintext highlighter-rouge">ξ</code> rule, and hence contains another reduction.
In its structure, it looks a little bit like a proof of progress:</p>
<ul>
<li>If the related terms are variables, no reduction applies.</li>
<li>If the related terms are abstractions, no reduction applies.</li>
<li>If the related terms are applications, there are three subcases:
<ul>
<li>
<p>The source term reduces via <code class="language-plaintext highlighter-rouge">ξ-·₁</code>, in which case the target term does as well.
Recursive invocation gives us</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>L --- —→ --- L′
| |
| |
~ ~
| |
| |
L† --- —→ --- L′†
</code></pre></div> </div>
<p>from which follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> L · M --- —→ --- L′ · M
| |
| |
~ ~
| |
| |
L† · M† --- —→ --- L′† · M†
</code></pre></div> </div>
</li>
<li>
<p>The source term reduces via <code class="language-plaintext highlighter-rouge">ξ-·₂</code>, in which case the target term does as well.
Recursive invocation gives us</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M --- —→ --- M′
| |
| |
~ ~
| |
| |
M† --- —→ --- M′†
</code></pre></div> </div>
<p>from which follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> V · M --- —→ --- V · M′
| |
| |
~ ~
| |
| |
V† · M† --- —→ --- V† · M′†
</code></pre></div> </div>
<p>Since simulation commutes with values and <code class="language-plaintext highlighter-rouge">V</code> is a value, <code class="language-plaintext highlighter-rouge">V†</code> is also a value.</p>
</li>
<li>
<p>The source term reduces via <code class="language-plaintext highlighter-rouge">β-ƛ</code>, in which case the target term does as well:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> (ƛ x ⇒ N) · V --- —→ --- N [ x := V ]
| |
| |
~ ~
| |
| |
(ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V† ]
</code></pre></div> </div>
<p>Since simulation commutes with values and <code class="language-plaintext highlighter-rouge">V</code> is a value, <code class="language-plaintext highlighter-rouge">V†</code> is also a value.
Since simulation commutes with substitution and <code class="language-plaintext highlighter-rouge">N ~ N†</code> and <code class="language-plaintext highlighter-rouge">V ~ V†</code>,
we have <code class="language-plaintext highlighter-rouge">N [ x := V ] ~ N† [ x := V† ]</code>.</p>
</li>
</ul>
</li>
<li>
<p>If the related terms are a let and an application of an abstraction,
there are two subcases:</p>
<ul>
<li>
<p>The source term reduces via <code class="language-plaintext highlighter-rouge">ξ-let</code>, in which case the target term
reduces via <code class="language-plaintext highlighter-rouge">ξ-·₂</code>. Recursive invocation gives us</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M --- —→ --- M′
| |
| |
~ ~
| |
| |
M† --- —→ --- M′†
</code></pre></div> </div>
<p>from which follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>let x = M in N --- —→ --- let x = M′ in N
| |
| |
~ ~
| |
| |
(ƛ x ⇒ N) · M --- —→ --- (ƛ x ⇒ N) · M′
</code></pre></div> </div>
</li>
<li>
<p>The source term reduces via <code class="language-plaintext highlighter-rouge">β-let</code>, in which case the target
term reduces via <code class="language-plaintext highlighter-rouge">β-ƛ</code>:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>let x = V in N --- —→ --- N [ x := V ]
| |
| |
~ ~
| |
| |
(ƛ x ⇒ N†) · V† --- —→ --- N† [ x := V† ]
</code></pre></div> </div>
<p>Since simulation commutes with values and <code class="language-plaintext highlighter-rouge">V</code> is a value, <code class="language-plaintext highlighter-rouge">V†</code> is also a value.
Since simulation commutes with substitution and <code class="language-plaintext highlighter-rouge">N ~ N†</code> and <code class="language-plaintext highlighter-rouge">V ~ V†</code>,
we have <code class="language-plaintext highlighter-rouge">N [ x := V ] ~ N† [ x := V† ]</code>.</p>
</li>
</ul>
</li>
</ul>
<h4 id="exercise-sim-practice">Exercise <code class="language-plaintext highlighter-rouge">sim⁻¹</code> (practice)</h4>
<p>Show that we also have a simulation in the other direction, and hence that we have
a bisimulation.</p>
<pre class="Agda"><a id="14091" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-products-practice">Exercise <code class="language-plaintext highlighter-rouge">products</code> (practice)</h4>
<p>Show that the two formulations of products in
Chapter <a href="/20.07/More/">More</a>
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 <em>not</em> lock-step.</p>
<pre class="Agda"><a id="14421" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="unicode">Unicode</h2>
<p>This chapter uses the following unicode:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>† U+2020 DAGGER (\dag)
⁻ U+207B SUPERSCRIPT MINUS (\^-)
¹ U+00B9 SUPERSCRIPT ONE (\^1)
</code></pre></div></div>
</div>
<p style="text-align:center;">
<a alt="Previous chapter" href="/20.07/More/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part2/Bisimulation.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/20.07/Inference/">Next</a>
</p>
</article>
</div>
</main><footer class="site-footer h-card">
<data class="u-url" href="/20.07/"></data>
<div class="wrapper">
<h2 class="footer-heading">Programming Language Foundations in Agda
</h2><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Philip Wadler</li>
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Wen Kokke</li>
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Jeremy G. Siek</li>
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
</div>
</footer>
<!-- Import jQuery -->
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
<script type="text/javascript">
anchors.add();
</script>
<script type="text/javascript">
// Makes sandwhich menu works
$('.menu-icon').click(function(){
$('.trigger').toggle();
});
// Script which allows for foldable code blocks
$('div.foldable pre').each(function(){
var autoHeight = $(this).height();
var lineHeight = parseFloat($(this).css('line-height'));
var plus = $("<div></div>");
var horLine = $("<div></div>");
var verLine = $("<div></div>");
$(this).prepend(plus);
plus.css({
'position' : 'relative',
'float' : 'right',
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'width' : lineHeight,
'height' : lineHeight});
verLine.css({
'position' : 'relative',
'height' : lineHeight,
'width' : '3px',
'background-color' : '#C1E0FF'});
horLine.css({
'position' : 'relative',
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'height' : '3px',
'width' : lineHeight,
'background-color' : '#C1E0FF'});
plus.append(verLine);
plus.append(horLine);
$(this).height(2.0 * lineHeight);
$(this).css('overflow','hidden');
$(this).click(function(){
if ($(this).height() == autoHeight) {
$(this).height(2.0 * lineHeight);
plus.show();
}
else {
$(this).height('auto');
plus.hide();
}
});
});
</script>
<!-- Import KaTeX -->
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
<!-- Script which renders TeX using KaTeX -->
<script type="text/javascript">
$("script[type='math/tex']").replaceWith(
function(){
var tex = $(this).text();
return "<span class=\"inline-equation\">" +
katex.renderToString(tex) +
"</span>";
});
$("script[type='math/tex; mode=display']").replaceWith(
function(){
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
return "<div class=\"equation\">" +
katex.renderToString("\\displaystyle "+tex) +
"</div>";
});
</script>
</body>
</html>
Reference in a new issue View git blame Copy permalink