715 lines
80 KiB
HTML
715 lines
80 KiB
HTML
<!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>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part2/Bisimulation.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<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>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part2/Bisimulation.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<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>
|