828 lines
168 KiB
HTML
828 lines
168 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>Confluence: Confluence of untyped lambda calculus 🚧 | 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="Confluence: Confluence of untyped lambda calculus 🚧" />
|
||
<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/Confluence/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/Confluence/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/Confluence/","headline":"Confluence: Confluence of untyped lambda calculus 🚧","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">Confluence: Confluence of untyped lambda calculus 🚧</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Untyped/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part2/Confluence.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/BigStep/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<pre class="Agda"><a id="166" class="Keyword">module</a> <a id="173" href="/20.07/Confluence/" class="Module">plfa.part2.Confluence</a> <a id="195" class="Keyword">where</a>
|
||
</pre>
|
||
<h2 id="introduction">Introduction</h2>
|
||
|
||
<p>In this chapter we prove that beta reduction is <em>confluent</em>, a
|
||
property also known as <em>Church-Rosser</em>. That is, if there are
|
||
reduction sequences from any term <code class="language-plaintext highlighter-rouge">L</code> to two different terms <code class="language-plaintext highlighter-rouge">M₁</code> and
|
||
<code class="language-plaintext highlighter-rouge">M₂</code>, then there exist reduction sequences from those two terms to
|
||
some common term <code class="language-plaintext highlighter-rouge">N</code>. In pictures:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> L
|
||
/ \
|
||
/ \
|
||
/ \
|
||
M₁ M₂
|
||
\ /
|
||
\ /
|
||
\ /
|
||
N
|
||
</code></pre></div></div>
|
||
|
||
<p>where downward lines are instances of <code class="language-plaintext highlighter-rouge">—↠</code>.</p>
|
||
|
||
<p>Confluence is studied in many other kinds of rewrite systems besides
|
||
the lambda calculus, and it is well known how to prove confluence in
|
||
rewrite systems that enjoy the <em>diamond property</em>, a single-step
|
||
version of confluence. Let <code class="language-plaintext highlighter-rouge">⇛</code> be a relation. Then <code class="language-plaintext highlighter-rouge">⇛</code> has the
|
||
diamond property if whenever <code class="language-plaintext highlighter-rouge">L ⇛ M₁</code> and <code class="language-plaintext highlighter-rouge">L ⇛ M₂</code>, then there exists
|
||
an <code class="language-plaintext highlighter-rouge">N</code> such that <code class="language-plaintext highlighter-rouge">M₁ ⇛ N</code> and <code class="language-plaintext highlighter-rouge">M₂ ⇛ N</code>. This is just an instance of
|
||
the same picture above, where downward lines are now instance of <code class="language-plaintext highlighter-rouge">⇛</code>.
|
||
If we write <code class="language-plaintext highlighter-rouge">⇛*</code> for the reflexive and transitive closure of <code class="language-plaintext highlighter-rouge">⇛</code>, then
|
||
confluence of <code class="language-plaintext highlighter-rouge">⇛*</code> follows immediately from the diamond property.</p>
|
||
|
||
<p>Unfortunately, reduction in the lambda calculus does not satisfy the
|
||
diamond property. Here is a counter example.</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(λ x. x x)((λ x. x) a) —→ (λ x. x x) a
|
||
(λ x. x x)((λ x. x) a) —→ ((λ x. x) a) ((λ x. x) a)
|
||
</code></pre></div></div>
|
||
|
||
<p>Both terms can reduce to <code class="language-plaintext highlighter-rouge">a a</code>, but the second term requires two steps
|
||
to get there, not one.</p>
|
||
|
||
<p>To side-step this problem, we’ll define an auxilliary reduction
|
||
relation, called <em>parallel reduction</em>, that can perform many
|
||
reductions simultaneously and thereby satisfy the diamond property.
|
||
Furthermore, we show that a parallel reduction sequence exists between
|
||
any two terms if and only if a beta reduction sequence exists between them.
|
||
Thus, we can reduce the proof of confluence for beta reduction to
|
||
confluence for parallel reduction.</p>
|
||
|
||
<h2 id="imports">Imports</h2>
|
||
|
||
<pre class="Agda"><a id="2056" class="Keyword">open</a> <a id="2061" class="Keyword">import</a> <a id="2068" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="2106" class="Keyword">using</a> <a id="2112" class="Symbol">(</a><a id="2113" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="2116" class="Symbol">;</a> <a id="2118" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="2122" class="Symbol">)</a>
|
||
<a id="2124" class="Keyword">open</a> <a id="2129" class="Keyword">import</a> <a id="2136" href="https://agda.github.io/agda-stdlib/v1.1/Function.html" class="Module">Function</a> <a id="2145" class="Keyword">using</a> <a id="2151" class="Symbol">(</a><a id="2152" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">_∘_</a><a id="2155" class="Symbol">)</a>
|
||
<a id="2157" class="Keyword">open</a> <a id="2162" class="Keyword">import</a> <a id="2169" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="2182" class="Keyword">using</a> <a id="2188" class="Symbol">(</a><a id="2189" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="2192" class="Symbol">;</a> <a id="2194" href="Agda.Builtin.Sigma.html#139" class="Record">Σ</a><a id="2195" class="Symbol">;</a> <a id="2197" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ-syntax</a><a id="2205" class="Symbol">;</a> <a id="2207" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1364" class="Function">∃</a><a id="2208" class="Symbol">;</a> <a id="2210" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃-syntax</a><a id="2218" class="Symbol">;</a> <a id="2220" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a><a id="2225" class="Symbol">;</a> <a id="2227" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a><a id="2232" class="Symbol">)</a>
|
||
<a id="2236" class="Keyword">renaming</a> <a id="2245" class="Symbol">(</a><a id="2246" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="2250" class="Symbol">to</a> <a id="2253" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="2258" class="Symbol">)</a>
|
||
<a id="2260" class="Keyword">open</a> <a id="2265" class="Keyword">import</a> <a id="2272" href="/20.07/Substitution/" class="Module">plfa.part2.Substitution</a> <a id="2296" class="Keyword">using</a> <a id="2302" class="Symbol">(</a><a id="2303" href="/20.07/Substitution/#2192" class="Function">Rename</a><a id="2309" class="Symbol">;</a> <a id="2311" href="/20.07/Substitution/#2405" class="Function">Subst</a><a id="2316" class="Symbol">)</a>
|
||
<a id="2318" class="Keyword">open</a> <a id="2323" class="Keyword">import</a> <a id="2330" href="/20.07/Untyped/" class="Module">plfa.part2.Untyped</a>
|
||
<a id="2351" class="Keyword">using</a> <a id="2357" class="Symbol">(</a><a id="2358" href="/20.07/Untyped/#9948" class="Datatype Operator">_—→_</a><a id="2362" class="Symbol">;</a> <a id="2364" href="/20.07/Untyped/#10178" class="InductiveConstructor">β</a><a id="2365" class="Symbol">;</a> <a id="2367" href="/20.07/Untyped/#9998" class="InductiveConstructor">ξ₁</a><a id="2369" class="Symbol">;</a> <a id="2371" href="/20.07/Untyped/#10088" class="InductiveConstructor">ξ₂</a><a id="2373" class="Symbol">;</a> <a id="2375" href="/20.07/Untyped/#10286" class="InductiveConstructor">ζ</a><a id="2376" class="Symbol">;</a> <a id="2378" href="/20.07/Untyped/#11068" class="Datatype Operator">_—↠_</a><a id="2382" class="Symbol">;</a> <a id="2384" href="/20.07/Untyped/#11274" class="Function Operator">begin_</a><a id="2390" class="Symbol">;</a> <a id="2392" href="/20.07/Untyped/#11174" class="InductiveConstructor Operator">_—→⟨_⟩_</a><a id="2399" class="Symbol">;</a> <a id="2401" href="/20.07/Untyped/#21991" class="Function Operator">_—↠⟨_⟩_</a><a id="2408" class="Symbol">;</a> <a id="2410" href="/20.07/Untyped/#11118" class="InductiveConstructor Operator">_∎</a><a id="2412" class="Symbol">;</a>
|
||
<a id="2416" href="/20.07/Untyped/#23902" class="Function">abs-cong</a><a id="2424" class="Symbol">;</a> <a id="2426" href="/20.07/Untyped/#22905" class="Function">appL-cong</a><a id="2435" class="Symbol">;</a> <a id="2437" href="/20.07/Untyped/#23674" class="Function">appR-cong</a><a id="2446" class="Symbol">;</a> <a id="2448" href="/20.07/Untyped/#21721" class="Function">—↠-trans</a><a id="2456" class="Symbol">;</a>
|
||
<a id="2460" href="/20.07/Untyped/#4294" class="Datatype Operator">_⊢_</a><a id="2463" class="Symbol">;</a> <a id="2465" href="/20.07/Untyped/#3521" class="Datatype Operator">_∋_</a><a id="2468" class="Symbol">;</a> <a id="2470" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`_</a><a id="2472" class="Symbol">;</a> <a id="2474" href="/20.07/Untyped/#5111" class="Function Operator">#_</a><a id="2476" class="Symbol">;</a> <a id="2478" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">_,_</a><a id="2481" class="Symbol">;</a> <a id="2483" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="2484" class="Symbol">;</a> <a id="2486" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ_</a><a id="2488" class="Symbol">;</a> <a id="2490" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">_·_</a><a id="2493" class="Symbol">;</a> <a id="2495" href="/20.07/Untyped/#7491" class="Function Operator">_[_]</a><a id="2499" class="Symbol">;</a>
|
||
<a id="2503" href="/20.07/Untyped/#6235" class="Function">rename</a><a id="2509" class="Symbol">;</a> <a id="2511" href="/20.07/Untyped/#5925" class="Function">ext</a><a id="2514" class="Symbol">;</a> <a id="2516" href="/20.07/Untyped/#6671" class="Function">exts</a><a id="2520" class="Symbol">;</a> <a id="2522" href="/20.07/Untyped/#3557" class="InductiveConstructor">Z</a><a id="2523" class="Symbol">;</a> <a id="2525" href="/20.07/Untyped/#3602" class="InductiveConstructor Operator">S_</a><a id="2527" class="Symbol">;</a> <a id="2529" href="/20.07/Untyped/#6963" class="Function">subst</a><a id="2534" class="Symbol">;</a> <a id="2536" href="/20.07/Untyped/#7375" class="Function">subst-zero</a><a id="2546" class="Symbol">)</a>
|
||
</pre>
|
||
<h2 id="parallel-reduction">Parallel Reduction</h2>
|
||
|
||
<p>The parallel reduction relation is defined as follows.</p>
|
||
|
||
<pre class="Agda"><a id="2636" class="Keyword">infix</a> <a id="2642" class="Number">2</a> <a id="2644" href="/20.07/Confluence/#2654" class="Datatype Operator">_⇛_</a>
|
||
|
||
<a id="2649" class="Keyword">data</a> <a id="_⇛_"></a><a id="2654" href="/20.07/Confluence/#2654" class="Datatype Operator">_⇛_</a> <a id="2658" class="Symbol">:</a> <a id="2660" class="Symbol">∀</a> <a id="2662" class="Symbol">{</a><a id="2663" href="/20.07/Confluence/#2663" class="Bound">Γ</a> <a id="2665" href="/20.07/Confluence/#2665" class="Bound">A</a><a id="2666" class="Symbol">}</a> <a id="2668" class="Symbol">→</a> <a id="2670" class="Symbol">(</a><a id="2671" href="/20.07/Confluence/#2663" class="Bound">Γ</a> <a id="2673" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2675" href="/20.07/Confluence/#2665" class="Bound">A</a><a id="2676" class="Symbol">)</a> <a id="2678" class="Symbol">→</a> <a id="2680" class="Symbol">(</a><a id="2681" href="/20.07/Confluence/#2663" class="Bound">Γ</a> <a id="2683" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2685" href="/20.07/Confluence/#2665" class="Bound">A</a><a id="2686" class="Symbol">)</a> <a id="2688" class="Symbol">→</a> <a id="2690" class="PrimitiveType">Set</a> <a id="2694" class="Keyword">where</a>
|
||
|
||
<a id="_⇛_.pvar"></a><a id="2703" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a> <a id="2708" class="Symbol">:</a> <a id="2710" class="Symbol">∀{</a><a id="2712" href="/20.07/Confluence/#2712" class="Bound">Γ</a> <a id="2714" href="/20.07/Confluence/#2714" class="Bound">A</a><a id="2715" class="Symbol">}{</a><a id="2717" href="/20.07/Confluence/#2717" class="Bound">x</a> <a id="2719" class="Symbol">:</a> <a id="2721" href="/20.07/Confluence/#2712" class="Bound">Γ</a> <a id="2723" href="/20.07/Untyped/#3521" class="Datatype Operator">∋</a> <a id="2725" href="/20.07/Confluence/#2714" class="Bound">A</a><a id="2726" class="Symbol">}</a>
|
||
<a id="2734" class="Comment">---------</a>
|
||
<a id="2748" class="Symbol">→</a> <a id="2750" class="Symbol">(</a><a id="2751" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="2753" href="/20.07/Confluence/#2717" class="Bound">x</a><a id="2754" class="Symbol">)</a> <a id="2756" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="2758" class="Symbol">(</a><a id="2759" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="2761" href="/20.07/Confluence/#2717" class="Bound">x</a><a id="2762" class="Symbol">)</a>
|
||
|
||
<a id="_⇛_.pabs"></a><a id="2767" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="2772" class="Symbol">:</a> <a id="2774" class="Symbol">∀{</a><a id="2776" href="/20.07/Confluence/#2776" class="Bound">Γ</a><a id="2777" class="Symbol">}{</a><a id="2779" href="/20.07/Confluence/#2779" class="Bound">N</a> <a id="2781" href="/20.07/Confluence/#2781" class="Bound">N′</a> <a id="2784" class="Symbol">:</a> <a id="2786" href="/20.07/Confluence/#2776" class="Bound">Γ</a> <a id="2788" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="2790" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a> <a id="2792" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2794" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="2795" class="Symbol">}</a>
|
||
<a id="2801" class="Symbol">→</a> <a id="2803" href="/20.07/Confluence/#2779" class="Bound">N</a> <a id="2805" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="2807" href="/20.07/Confluence/#2781" class="Bound">N′</a>
|
||
<a id="2816" class="Comment">----------</a>
|
||
<a id="2831" class="Symbol">→</a> <a id="2833" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="2835" href="/20.07/Confluence/#2779" class="Bound">N</a> <a id="2837" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="2839" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="2841" href="/20.07/Confluence/#2781" class="Bound">N′</a>
|
||
|
||
<a id="_⇛_.papp"></a><a id="2847" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="2852" class="Symbol">:</a> <a id="2854" class="Symbol">∀{</a><a id="2856" href="/20.07/Confluence/#2856" class="Bound">Γ</a><a id="2857" class="Symbol">}{</a><a id="2859" href="/20.07/Confluence/#2859" class="Bound">L</a> <a id="2861" href="/20.07/Confluence/#2861" class="Bound">L′</a> <a id="2864" href="/20.07/Confluence/#2864" class="Bound">M</a> <a id="2866" href="/20.07/Confluence/#2866" class="Bound">M′</a> <a id="2869" class="Symbol">:</a> <a id="2871" href="/20.07/Confluence/#2856" class="Bound">Γ</a> <a id="2873" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2875" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="2876" class="Symbol">}</a>
|
||
<a id="2882" class="Symbol">→</a> <a id="2884" href="/20.07/Confluence/#2859" class="Bound">L</a> <a id="2886" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="2888" href="/20.07/Confluence/#2861" class="Bound">L′</a>
|
||
<a id="2895" class="Symbol">→</a> <a id="2897" href="/20.07/Confluence/#2864" class="Bound">M</a> <a id="2899" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="2901" href="/20.07/Confluence/#2866" class="Bound">M′</a>
|
||
<a id="2910" class="Comment">-----------------</a>
|
||
<a id="2932" class="Symbol">→</a> <a id="2934" href="/20.07/Confluence/#2859" class="Bound">L</a> <a id="2936" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="2938" href="/20.07/Confluence/#2864" class="Bound">M</a> <a id="2940" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="2942" href="/20.07/Confluence/#2861" class="Bound">L′</a> <a id="2945" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="2947" href="/20.07/Confluence/#2866" class="Bound">M′</a>
|
||
|
||
<a id="_⇛_.pbeta"></a><a id="2953" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="2959" class="Symbol">:</a> <a id="2961" class="Symbol">∀{</a><a id="2963" href="/20.07/Confluence/#2963" class="Bound">Γ</a><a id="2964" class="Symbol">}{</a><a id="2966" href="/20.07/Confluence/#2966" class="Bound">N</a> <a id="2968" href="/20.07/Confluence/#2968" class="Bound">N′</a> <a id="2972" class="Symbol">:</a> <a id="2974" href="/20.07/Confluence/#2963" class="Bound">Γ</a> <a id="2976" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="2978" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a> <a id="2980" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2982" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="2983" class="Symbol">}{</a><a id="2985" href="/20.07/Confluence/#2985" class="Bound">M</a> <a id="2987" href="/20.07/Confluence/#2987" class="Bound">M′</a> <a id="2990" class="Symbol">:</a> <a id="2992" href="/20.07/Confluence/#2963" class="Bound">Γ</a> <a id="2994" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2996" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="2997" class="Symbol">}</a>
|
||
<a id="3003" class="Symbol">→</a> <a id="3005" href="/20.07/Confluence/#2966" class="Bound">N</a> <a id="3007" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="3009" href="/20.07/Confluence/#2968" class="Bound">N′</a>
|
||
<a id="3016" class="Symbol">→</a> <a id="3018" href="/20.07/Confluence/#2985" class="Bound">M</a> <a id="3020" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="3022" href="/20.07/Confluence/#2987" class="Bound">M′</a>
|
||
<a id="3031" class="Comment">-----------------------</a>
|
||
<a id="3059" class="Symbol">→</a> <a id="3061" class="Symbol">(</a><a id="3062" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="3064" href="/20.07/Confluence/#2966" class="Bound">N</a><a id="3065" class="Symbol">)</a> <a id="3067" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="3069" href="/20.07/Confluence/#2985" class="Bound">M</a> <a id="3072" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="3075" href="/20.07/Confluence/#2968" class="Bound">N′</a> <a id="3078" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="3080" href="/20.07/Confluence/#2987" class="Bound">M′</a> <a id="3083" href="/20.07/Untyped/#7491" class="Function Operator">]</a>
|
||
</pre>
|
||
<p>The first three rules are congruences that reduce each of their
|
||
parts simultaneously. The last rule reduces a lambda term and
|
||
term in parallel followed by a beta step.</p>
|
||
|
||
<p>We remark that the <code class="language-plaintext highlighter-rouge">pabs</code>, <code class="language-plaintext highlighter-rouge">papp</code>, and <code class="language-plaintext highlighter-rouge">pbeta</code> rules perform reduction
|
||
on all their subexpressions simultaneously. Also, the <code class="language-plaintext highlighter-rouge">pabs</code> rule is
|
||
akin to the <code class="language-plaintext highlighter-rouge">ζ</code> rule and <code class="language-plaintext highlighter-rouge">pbeta</code> is akin to <code class="language-plaintext highlighter-rouge">β</code>.</p>
|
||
|
||
<p>Parallel reduction is reflexive.</p>
|
||
|
||
<pre class="Agda"><a id="par-refl"></a><a id="3486" href="/20.07/Confluence/#3486" class="Function">par-refl</a> <a id="3495" class="Symbol">:</a> <a id="3497" class="Symbol">∀{</a><a id="3499" href="/20.07/Confluence/#3499" class="Bound">Γ</a> <a id="3501" href="/20.07/Confluence/#3501" class="Bound">A</a><a id="3502" class="Symbol">}{</a><a id="3504" href="/20.07/Confluence/#3504" class="Bound">M</a> <a id="3506" class="Symbol">:</a> <a id="3508" href="/20.07/Confluence/#3499" class="Bound">Γ</a> <a id="3510" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3512" href="/20.07/Confluence/#3501" class="Bound">A</a><a id="3513" class="Symbol">}</a> <a id="3515" class="Symbol">→</a> <a id="3517" href="/20.07/Confluence/#3504" class="Bound">M</a> <a id="3519" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="3521" href="/20.07/Confluence/#3504" class="Bound">M</a>
|
||
<a id="3523" href="/20.07/Confluence/#3486" class="Function">par-refl</a> <a id="3532" class="Symbol">{</a><a id="3533" href="/20.07/Confluence/#3533" class="Bound">Γ</a><a id="3534" class="Symbol">}</a> <a id="3536" class="Symbol">{</a><a id="3537" href="/20.07/Confluence/#3537" class="Bound">A</a><a id="3538" class="Symbol">}</a> <a id="3540" class="Symbol">{</a><a id="3541" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="3543" href="/20.07/Confluence/#3543" class="Bound">x</a><a id="3544" class="Symbol">}</a> <a id="3546" class="Symbol">=</a> <a id="3548" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a>
|
||
<a id="3553" href="/20.07/Confluence/#3486" class="Function">par-refl</a> <a id="3562" class="Symbol">{</a><a id="3563" href="/20.07/Confluence/#3563" class="Bound">Γ</a><a id="3564" class="Symbol">}</a> <a id="3566" class="Symbol">{</a><a id="3567" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="3568" class="Symbol">}</a> <a id="3570" class="Symbol">{</a><a id="3571" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="3573" href="/20.07/Confluence/#3573" class="Bound">N</a><a id="3574" class="Symbol">}</a> <a id="3576" class="Symbol">=</a> <a id="3578" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="3583" href="/20.07/Confluence/#3486" class="Function">par-refl</a>
|
||
<a id="3592" href="/20.07/Confluence/#3486" class="Function">par-refl</a> <a id="3601" class="Symbol">{</a><a id="3602" href="/20.07/Confluence/#3602" class="Bound">Γ</a><a id="3603" class="Symbol">}</a> <a id="3605" class="Symbol">{</a><a id="3606" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="3607" class="Symbol">}</a> <a id="3609" class="Symbol">{</a><a id="3610" href="/20.07/Confluence/#3610" class="Bound">L</a> <a id="3612" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="3614" href="/20.07/Confluence/#3614" class="Bound">M</a><a id="3615" class="Symbol">}</a> <a id="3617" class="Symbol">=</a> <a id="3619" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="3624" href="/20.07/Confluence/#3486" class="Function">par-refl</a> <a id="3633" href="/20.07/Confluence/#3486" class="Function">par-refl</a>
|
||
</pre>
|
||
<p>We define the sequences of parallel reduction as follows.</p>
|
||
|
||
<pre class="Agda"><a id="3709" class="Keyword">infix</a> <a id="3716" class="Number">2</a> <a id="3718" href="/20.07/Confluence/#3757" class="Datatype Operator">_⇛*_</a>
|
||
<a id="3723" class="Keyword">infixr</a> <a id="3730" class="Number">2</a> <a id="3732" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">_⇛⟨_⟩_</a>
|
||
<a id="3739" class="Keyword">infix</a> <a id="3746" class="Number">3</a> <a id="3748" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">_∎</a>
|
||
|
||
<a id="3752" class="Keyword">data</a> <a id="_⇛*_"></a><a id="3757" href="/20.07/Confluence/#3757" class="Datatype Operator">_⇛*_</a> <a id="3762" class="Symbol">:</a> <a id="3764" class="Symbol">∀</a> <a id="3766" class="Symbol">{</a><a id="3767" href="/20.07/Confluence/#3767" class="Bound">Γ</a> <a id="3769" href="/20.07/Confluence/#3769" class="Bound">A</a><a id="3770" class="Symbol">}</a> <a id="3772" class="Symbol">→</a> <a id="3774" class="Symbol">(</a><a id="3775" href="/20.07/Confluence/#3767" class="Bound">Γ</a> <a id="3777" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3779" href="/20.07/Confluence/#3769" class="Bound">A</a><a id="3780" class="Symbol">)</a> <a id="3782" class="Symbol">→</a> <a id="3784" class="Symbol">(</a><a id="3785" href="/20.07/Confluence/#3767" class="Bound">Γ</a> <a id="3787" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3789" href="/20.07/Confluence/#3769" class="Bound">A</a><a id="3790" class="Symbol">)</a> <a id="3792" class="Symbol">→</a> <a id="3794" class="PrimitiveType">Set</a> <a id="3798" class="Keyword">where</a>
|
||
|
||
<a id="_⇛*_._∎"></a><a id="3807" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">_∎</a> <a id="3810" class="Symbol">:</a> <a id="3812" class="Symbol">∀</a> <a id="3814" class="Symbol">{</a><a id="3815" href="/20.07/Confluence/#3815" class="Bound">Γ</a> <a id="3817" href="/20.07/Confluence/#3817" class="Bound">A</a><a id="3818" class="Symbol">}</a> <a id="3820" class="Symbol">(</a><a id="3821" href="/20.07/Confluence/#3821" class="Bound">M</a> <a id="3823" class="Symbol">:</a> <a id="3825" href="/20.07/Confluence/#3815" class="Bound">Γ</a> <a id="3827" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3829" href="/20.07/Confluence/#3817" class="Bound">A</a><a id="3830" class="Symbol">)</a>
|
||
<a id="3838" class="Comment">--------</a>
|
||
<a id="3851" class="Symbol">→</a> <a id="3853" href="/20.07/Confluence/#3821" class="Bound">M</a> <a id="3855" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="3858" href="/20.07/Confluence/#3821" class="Bound">M</a>
|
||
|
||
<a id="_⇛*_._⇛⟨_⟩_"></a><a id="3863" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">_⇛⟨_⟩_</a> <a id="3870" class="Symbol">:</a> <a id="3872" class="Symbol">∀</a> <a id="3874" class="Symbol">{</a><a id="3875" href="/20.07/Confluence/#3875" class="Bound">Γ</a> <a id="3877" href="/20.07/Confluence/#3877" class="Bound">A</a><a id="3878" class="Symbol">}</a> <a id="3880" class="Symbol">(</a><a id="3881" href="/20.07/Confluence/#3881" class="Bound">L</a> <a id="3883" class="Symbol">:</a> <a id="3885" href="/20.07/Confluence/#3875" class="Bound">Γ</a> <a id="3887" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3889" href="/20.07/Confluence/#3877" class="Bound">A</a><a id="3890" class="Symbol">)</a> <a id="3892" class="Symbol">{</a><a id="3893" href="/20.07/Confluence/#3893" class="Bound">M</a> <a id="3895" href="/20.07/Confluence/#3895" class="Bound">N</a> <a id="3897" class="Symbol">:</a> <a id="3899" href="/20.07/Confluence/#3875" class="Bound">Γ</a> <a id="3901" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3903" href="/20.07/Confluence/#3877" class="Bound">A</a><a id="3904" class="Symbol">}</a>
|
||
<a id="3910" class="Symbol">→</a> <a id="3912" href="/20.07/Confluence/#3881" class="Bound">L</a> <a id="3914" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="3916" href="/20.07/Confluence/#3893" class="Bound">M</a>
|
||
<a id="3922" class="Symbol">→</a> <a id="3924" href="/20.07/Confluence/#3893" class="Bound">M</a> <a id="3926" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="3929" href="/20.07/Confluence/#3895" class="Bound">N</a>
|
||
<a id="3937" class="Comment">---------</a>
|
||
<a id="3951" class="Symbol">→</a> <a id="3953" href="/20.07/Confluence/#3881" class="Bound">L</a> <a id="3955" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="3958" href="/20.07/Confluence/#3895" class="Bound">N</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise-par-diamond-eg-practice">Exercise <code class="language-plaintext highlighter-rouge">par-diamond-eg</code> (practice)</h4>
|
||
|
||
<p>Revisit the counter example to the diamond property for reduction by
|
||
showing that the diamond property holds for parallel reduction in that
|
||
case.</p>
|
||
|
||
<pre class="Agda"><a id="4160" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h2 id="equivalence-between-parallel-reduction-and-reduction">Equivalence between parallel reduction and reduction</h2>
|
||
|
||
<p>Here we prove that for any <code class="language-plaintext highlighter-rouge">M</code> and <code class="language-plaintext highlighter-rouge">N</code>, <code class="language-plaintext highlighter-rouge">M ⇛* N</code> if and only if <code class="language-plaintext highlighter-rouge">M —↠ N</code>.
|
||
The only-if direction is particularly easy. We start by showing
|
||
that if <code class="language-plaintext highlighter-rouge">M —→ N</code>, then <code class="language-plaintext highlighter-rouge">M ⇛ N</code>. The proof is by induction on
|
||
the reduction <code class="language-plaintext highlighter-rouge">M —→ N</code>.</p>
|
||
|
||
<pre class="Agda"><a id="beta-par"></a><a id="4474" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4483" class="Symbol">:</a> <a id="4485" class="Symbol">∀{</a><a id="4487" href="/20.07/Confluence/#4487" class="Bound">Γ</a> <a id="4489" href="/20.07/Confluence/#4489" class="Bound">A</a><a id="4490" class="Symbol">}{</a><a id="4492" href="/20.07/Confluence/#4492" class="Bound">M</a> <a id="4494" href="/20.07/Confluence/#4494" class="Bound">N</a> <a id="4496" class="Symbol">:</a> <a id="4498" href="/20.07/Confluence/#4487" class="Bound">Γ</a> <a id="4500" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="4502" href="/20.07/Confluence/#4489" class="Bound">A</a><a id="4503" class="Symbol">}</a>
|
||
<a id="4507" class="Symbol">→</a> <a id="4509" href="/20.07/Confluence/#4492" class="Bound">M</a> <a id="4511" href="/20.07/Untyped/#9948" class="Datatype Operator">—→</a> <a id="4514" href="/20.07/Confluence/#4494" class="Bound">N</a>
|
||
<a id="4520" class="Comment">------</a>
|
||
<a id="4529" class="Symbol">→</a> <a id="4531" href="/20.07/Confluence/#4492" class="Bound">M</a> <a id="4533" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="4535" href="/20.07/Confluence/#4494" class="Bound">N</a>
|
||
<a id="4537" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4546" class="Symbol">{</a><a id="4547" href="/20.07/Confluence/#4547" class="Bound">Γ</a><a id="4548" class="Symbol">}</a> <a id="4550" class="Symbol">{</a><a id="4551" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="4552" class="Symbol">}</a> <a id="4554" class="Symbol">{</a><a id="4555" href="/20.07/Confluence/#4555" class="Bound">L</a> <a id="4557" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="4559" href="/20.07/Confluence/#4559" class="Bound">M</a><a id="4560" class="Symbol">}</a> <a id="4562" class="Symbol">(</a><a id="4563" href="/20.07/Untyped/#9998" class="InductiveConstructor">ξ₁</a> <a id="4566" href="/20.07/Confluence/#4566" class="Bound">r</a><a id="4567" class="Symbol">)</a> <a id="4569" class="Symbol">=</a> <a id="4571" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="4576" class="Symbol">(</a><a id="4577" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4586" class="Symbol">{</a><a id="4587" class="Argument">M</a> <a id="4589" class="Symbol">=</a> <a id="4591" href="/20.07/Confluence/#4555" class="Bound">L</a><a id="4592" class="Symbol">}</a> <a id="4594" href="/20.07/Confluence/#4566" class="Bound">r</a><a id="4595" class="Symbol">)</a> <a id="4597" href="/20.07/Confluence/#3486" class="Function">par-refl</a>
|
||
<a id="4606" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4615" class="Symbol">{</a><a id="4616" href="/20.07/Confluence/#4616" class="Bound">Γ</a><a id="4617" class="Symbol">}</a> <a id="4619" class="Symbol">{</a><a id="4620" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="4621" class="Symbol">}</a> <a id="4623" class="Symbol">{</a><a id="4624" href="/20.07/Confluence/#4624" class="Bound">L</a> <a id="4626" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="4628" href="/20.07/Confluence/#4628" class="Bound">M</a><a id="4629" class="Symbol">}</a> <a id="4631" class="Symbol">(</a><a id="4632" href="/20.07/Untyped/#10088" class="InductiveConstructor">ξ₂</a> <a id="4635" href="/20.07/Confluence/#4635" class="Bound">r</a><a id="4636" class="Symbol">)</a> <a id="4638" class="Symbol">=</a> <a id="4640" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="4645" href="/20.07/Confluence/#3486" class="Function">par-refl</a> <a id="4654" class="Symbol">(</a><a id="4655" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4664" class="Symbol">{</a><a id="4665" class="Argument">M</a> <a id="4667" class="Symbol">=</a> <a id="4669" href="/20.07/Confluence/#4628" class="Bound">M</a><a id="4670" class="Symbol">}</a> <a id="4672" href="/20.07/Confluence/#4635" class="Bound">r</a><a id="4673" class="Symbol">)</a>
|
||
<a id="4675" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4684" class="Symbol">{</a><a id="4685" href="/20.07/Confluence/#4685" class="Bound">Γ</a><a id="4686" class="Symbol">}</a> <a id="4688" class="Symbol">{</a><a id="4689" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="4690" class="Symbol">}</a> <a id="4692" class="Symbol">{(</a><a id="4694" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="4696" href="/20.07/Confluence/#4696" class="Bound">N</a><a id="4697" class="Symbol">)</a> <a id="4699" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="4701" href="/20.07/Confluence/#4701" class="Bound">M</a><a id="4702" class="Symbol">}</a> <a id="4704" href="/20.07/Untyped/#10178" class="InductiveConstructor">β</a> <a id="4706" class="Symbol">=</a> <a id="4708" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="4714" href="/20.07/Confluence/#3486" class="Function">par-refl</a> <a id="4723" href="/20.07/Confluence/#3486" class="Function">par-refl</a>
|
||
<a id="4732" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4741" class="Symbol">{</a><a id="4742" href="/20.07/Confluence/#4742" class="Bound">Γ</a><a id="4743" class="Symbol">}</a> <a id="4745" class="Symbol">{</a><a id="4746" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="4747" class="Symbol">}</a> <a id="4749" class="Symbol">{</a><a id="4750" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="4752" href="/20.07/Confluence/#4752" class="Bound">N</a><a id="4753" class="Symbol">}</a> <a id="4755" class="Symbol">(</a><a id="4756" href="/20.07/Untyped/#10286" class="InductiveConstructor">ζ</a> <a id="4758" href="/20.07/Confluence/#4758" class="Bound">r</a><a id="4759" class="Symbol">)</a> <a id="4761" class="Symbol">=</a> <a id="4763" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="4768" class="Symbol">(</a><a id="4769" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="4778" href="/20.07/Confluence/#4758" class="Bound">r</a><a id="4779" class="Symbol">)</a>
|
||
</pre>
|
||
<p>With this lemma in hand we complete the only-if direction,
|
||
that <code class="language-plaintext highlighter-rouge">M —↠ N</code> implies <code class="language-plaintext highlighter-rouge">M ⇛* N</code>. The proof is a straightforward
|
||
induction on the reduction sequence <code class="language-plaintext highlighter-rouge">M —↠ N</code>.</p>
|
||
|
||
<pre class="Agda"><a id="betas-pars"></a><a id="4959" href="/20.07/Confluence/#4959" class="Function">betas-pars</a> <a id="4970" class="Symbol">:</a> <a id="4972" class="Symbol">∀{</a><a id="4974" href="/20.07/Confluence/#4974" class="Bound">Γ</a> <a id="4976" href="/20.07/Confluence/#4976" class="Bound">A</a><a id="4977" class="Symbol">}</a> <a id="4979" class="Symbol">{</a><a id="4980" href="/20.07/Confluence/#4980" class="Bound">M</a> <a id="4982" href="/20.07/Confluence/#4982" class="Bound">N</a> <a id="4984" class="Symbol">:</a> <a id="4986" href="/20.07/Confluence/#4974" class="Bound">Γ</a> <a id="4988" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="4990" href="/20.07/Confluence/#4976" class="Bound">A</a><a id="4991" class="Symbol">}</a>
|
||
<a id="4995" class="Symbol">→</a> <a id="4997" href="/20.07/Confluence/#4980" class="Bound">M</a> <a id="4999" href="/20.07/Untyped/#11068" class="Datatype Operator">—↠</a> <a id="5002" href="/20.07/Confluence/#4982" class="Bound">N</a>
|
||
<a id="5008" class="Comment">------</a>
|
||
<a id="5017" class="Symbol">→</a> <a id="5019" href="/20.07/Confluence/#4980" class="Bound">M</a> <a id="5021" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="5024" href="/20.07/Confluence/#4982" class="Bound">N</a>
|
||
<a id="5026" href="/20.07/Confluence/#4959" class="Function">betas-pars</a> <a id="5037" class="Symbol">{</a><a id="5038" href="/20.07/Confluence/#5038" class="Bound">Γ</a><a id="5039" class="Symbol">}</a> <a id="5041" class="Symbol">{</a><a id="5042" href="/20.07/Confluence/#5042" class="Bound">A</a><a id="5043" class="Symbol">}</a> <a id="5045" class="Symbol">{</a><a id="5046" href="/20.07/Confluence/#5046" class="Bound">M₁</a><a id="5048" class="Symbol">}</a> <a id="5050" class="Symbol">{</a><a id="5051" class="DottedPattern Symbol">.</a><a id="5052" href="/20.07/Confluence/#5046" class="DottedPattern Bound">M₁</a><a id="5054" class="Symbol">}</a> <a id="5056" class="Symbol">(</a><a id="5057" href="/20.07/Confluence/#5046" class="Bound">M₁</a> <a id="5060" href="/20.07/Untyped/#11118" class="InductiveConstructor Operator">∎</a><a id="5061" class="Symbol">)</a> <a id="5063" class="Symbol">=</a> <a id="5065" href="/20.07/Confluence/#5046" class="Bound">M₁</a> <a id="5068" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">∎</a>
|
||
<a id="5070" href="/20.07/Confluence/#4959" class="Function">betas-pars</a> <a id="5081" class="Symbol">{</a><a id="5082" href="/20.07/Confluence/#5082" class="Bound">Γ</a><a id="5083" class="Symbol">}</a> <a id="5085" class="Symbol">{</a><a id="5086" href="/20.07/Confluence/#5086" class="Bound">A</a><a id="5087" class="Symbol">}</a> <a id="5089" class="Symbol">{</a><a id="5090" class="DottedPattern Symbol">.</a><a id="5091" href="/20.07/Confluence/#5099" class="DottedPattern Bound">L</a><a id="5092" class="Symbol">}</a> <a id="5094" class="Symbol">{</a><a id="5095" href="/20.07/Confluence/#5095" class="Bound">N</a><a id="5096" class="Symbol">}</a> <a id="5098" class="Symbol">(</a><a id="5099" href="/20.07/Confluence/#5099" class="Bound">L</a> <a id="5101" href="/20.07/Untyped/#11174" class="InductiveConstructor Operator">—→⟨</a> <a id="5105" href="/20.07/Confluence/#5105" class="Bound">b</a> <a id="5107" href="/20.07/Untyped/#11174" class="InductiveConstructor Operator">⟩</a> <a id="5109" href="/20.07/Confluence/#5109" class="Bound">bs</a><a id="5111" class="Symbol">)</a> <a id="5113" class="Symbol">=</a>
|
||
<a id="5118" href="/20.07/Confluence/#5099" class="Bound">L</a> <a id="5120" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⇛⟨</a> <a id="5123" href="/20.07/Confluence/#4474" class="Function">beta-par</a> <a id="5132" href="/20.07/Confluence/#5105" class="Bound">b</a> <a id="5134" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⟩</a> <a id="5136" href="/20.07/Confluence/#4959" class="Function">betas-pars</a> <a id="5147" href="/20.07/Confluence/#5109" class="Bound">bs</a>
|
||
</pre>
|
||
<p>Now for the other direction, that <code class="language-plaintext highlighter-rouge">M ⇛* N</code> implies <code class="language-plaintext highlighter-rouge">M —↠ N</code>. The
|
||
proof of this direction is a bit different because it’s not the case
|
||
that <code class="language-plaintext highlighter-rouge">M ⇛ N</code> implies <code class="language-plaintext highlighter-rouge">M —→ N</code>. After all, <code class="language-plaintext highlighter-rouge">M ⇛ N</code> performs many
|
||
reductions. So instead we shall prove that <code class="language-plaintext highlighter-rouge">M ⇛ N</code> implies <code class="language-plaintext highlighter-rouge">M —↠ N</code>.</p>
|
||
|
||
<pre class="Agda"><a id="par-betas"></a><a id="5428" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5438" class="Symbol">:</a> <a id="5440" class="Symbol">∀{</a><a id="5442" href="/20.07/Confluence/#5442" class="Bound">Γ</a> <a id="5444" href="/20.07/Confluence/#5444" class="Bound">A</a><a id="5445" class="Symbol">}{</a><a id="5447" href="/20.07/Confluence/#5447" class="Bound">M</a> <a id="5449" href="/20.07/Confluence/#5449" class="Bound">N</a> <a id="5451" class="Symbol">:</a> <a id="5453" href="/20.07/Confluence/#5442" class="Bound">Γ</a> <a id="5455" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="5457" href="/20.07/Confluence/#5444" class="Bound">A</a><a id="5458" class="Symbol">}</a>
|
||
<a id="5462" class="Symbol">→</a> <a id="5464" href="/20.07/Confluence/#5447" class="Bound">M</a> <a id="5466" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="5468" href="/20.07/Confluence/#5449" class="Bound">N</a>
|
||
<a id="5474" class="Comment">------</a>
|
||
<a id="5483" class="Symbol">→</a> <a id="5485" href="/20.07/Confluence/#5447" class="Bound">M</a> <a id="5487" href="/20.07/Untyped/#11068" class="Datatype Operator">—↠</a> <a id="5490" href="/20.07/Confluence/#5449" class="Bound">N</a>
|
||
<a id="5492" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5502" class="Symbol">{</a><a id="5503" href="/20.07/Confluence/#5503" class="Bound">Γ</a><a id="5504" class="Symbol">}</a> <a id="5506" class="Symbol">{</a><a id="5507" href="/20.07/Confluence/#5507" class="Bound">A</a><a id="5508" class="Symbol">}</a> <a id="5510" class="Symbol">{</a><a id="5511" class="DottedPattern Symbol">.(</a><a id="5513" href="/20.07/Untyped/#4330" class="DottedPattern InductiveConstructor Operator">`</a> <a id="5515" class="DottedPattern Symbol">_)</a><a id="5517" class="Symbol">}</a> <a id="5519" class="Symbol">(</a><a id="5520" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a><a id="5524" class="Symbol">{</a><a id="5525" class="Argument">x</a> <a id="5527" class="Symbol">=</a> <a id="5529" href="/20.07/Confluence/#5529" class="Bound">x</a><a id="5530" class="Symbol">})</a> <a id="5533" class="Symbol">=</a> <a id="5535" class="Symbol">(</a><a id="5536" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="5538" href="/20.07/Confluence/#5529" class="Bound">x</a><a id="5539" class="Symbol">)</a> <a id="5541" href="/20.07/Untyped/#11118" class="InductiveConstructor Operator">∎</a>
|
||
<a id="5543" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5553" class="Symbol">{</a><a id="5554" href="/20.07/Confluence/#5554" class="Bound">Γ</a><a id="5555" class="Symbol">}</a> <a id="5557" class="Symbol">{</a><a id="5558" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="5559" class="Symbol">}</a> <a id="5561" class="Symbol">{</a><a id="5562" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5564" href="/20.07/Confluence/#5564" class="Bound">N</a><a id="5565" class="Symbol">}</a> <a id="5567" class="Symbol">(</a><a id="5568" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="5573" href="/20.07/Confluence/#5573" class="Bound">p</a><a id="5574" class="Symbol">)</a> <a id="5576" class="Symbol">=</a> <a id="5578" href="/20.07/Untyped/#23902" class="Function">abs-cong</a> <a id="5587" class="Symbol">(</a><a id="5588" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5598" href="/20.07/Confluence/#5573" class="Bound">p</a><a id="5599" class="Symbol">)</a>
|
||
<a id="5601" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5611" class="Symbol">{</a><a id="5612" href="/20.07/Confluence/#5612" class="Bound">Γ</a><a id="5613" class="Symbol">}</a> <a id="5615" class="Symbol">{</a><a id="5616" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="5617" class="Symbol">}</a> <a id="5619" class="Symbol">{</a><a id="5620" href="/20.07/Confluence/#5620" class="Bound">L</a> <a id="5622" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="5624" href="/20.07/Confluence/#5624" class="Bound">M</a><a id="5625" class="Symbol">}</a> <a id="5627" class="Symbol">(</a><a id="5628" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="5633" class="Symbol">{</a><a id="5634" class="Argument">L</a> <a id="5636" class="Symbol">=</a> <a id="5638" href="/20.07/Confluence/#5620" class="Bound">L</a><a id="5639" class="Symbol">}{</a><a id="5641" href="/20.07/Confluence/#5641" class="Bound">L′</a><a id="5643" class="Symbol">}{</a><a id="5645" href="/20.07/Confluence/#5624" class="Bound">M</a><a id="5646" class="Symbol">}{</a><a id="5648" href="/20.07/Confluence/#5648" class="Bound">M′</a><a id="5650" class="Symbol">}</a> <a id="5652" href="/20.07/Confluence/#5652" class="Bound">p₁</a> <a id="5655" href="/20.07/Confluence/#5655" class="Bound">p₂</a><a id="5657" class="Symbol">)</a> <a id="5659" class="Symbol">=</a>
|
||
<a id="5665" href="/20.07/Untyped/#11274" class="Function Operator">begin</a>
|
||
<a id="5675" href="/20.07/Confluence/#5620" class="Bound">L</a> <a id="5677" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="5679" href="/20.07/Confluence/#5624" class="Bound">M</a> <a id="5683" href="/20.07/Untyped/#21991" class="Function Operator">—↠⟨</a> <a id="5687" href="/20.07/Untyped/#22905" class="Function">appL-cong</a><a id="5696" class="Symbol">{</a><a id="5697" class="Argument">M</a> <a id="5699" class="Symbol">=</a> <a id="5701" href="/20.07/Confluence/#5624" class="Bound">M</a><a id="5702" class="Symbol">}</a> <a id="5704" class="Symbol">(</a><a id="5705" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5715" href="/20.07/Confluence/#5652" class="Bound">p₁</a><a id="5717" class="Symbol">)</a> <a id="5719" href="/20.07/Untyped/#21991" class="Function Operator">⟩</a>
|
||
<a id="5725" href="/20.07/Confluence/#5641" class="Bound">L′</a> <a id="5728" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="5730" href="/20.07/Confluence/#5624" class="Bound">M</a> <a id="5733" href="/20.07/Untyped/#21991" class="Function Operator">—↠⟨</a> <a id="5737" href="/20.07/Untyped/#23674" class="Function">appR-cong</a> <a id="5747" class="Symbol">(</a><a id="5748" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5758" href="/20.07/Confluence/#5655" class="Bound">p₂</a><a id="5760" class="Symbol">)</a> <a id="5762" href="/20.07/Untyped/#21991" class="Function Operator">⟩</a>
|
||
<a id="5768" href="/20.07/Confluence/#5641" class="Bound">L′</a> <a id="5771" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="5773" href="/20.07/Confluence/#5648" class="Bound">M′</a>
|
||
<a id="5780" href="/20.07/Untyped/#11118" class="InductiveConstructor Operator">∎</a>
|
||
<a id="5782" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5792" class="Symbol">{</a><a id="5793" href="/20.07/Confluence/#5793" class="Bound">Γ</a><a id="5794" class="Symbol">}</a> <a id="5796" class="Symbol">{</a><a id="5797" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="5798" class="Symbol">}</a> <a id="5800" class="Symbol">{(</a><a id="5802" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5804" href="/20.07/Confluence/#5804" class="Bound">N</a><a id="5805" class="Symbol">)</a> <a id="5807" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="5809" href="/20.07/Confluence/#5809" class="Bound">M</a><a id="5810" class="Symbol">}</a> <a id="5812" class="Symbol">(</a><a id="5813" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a><a id="5818" class="Symbol">{</a><a id="5819" class="Argument">N′</a> <a id="5822" class="Symbol">=</a> <a id="5824" href="/20.07/Confluence/#5824" class="Bound">N′</a><a id="5826" class="Symbol">}{</a><a id="5828" class="Argument">M′</a> <a id="5831" class="Symbol">=</a> <a id="5833" href="/20.07/Confluence/#5833" class="Bound">M′</a><a id="5835" class="Symbol">}</a> <a id="5837" href="/20.07/Confluence/#5837" class="Bound">p₁</a> <a id="5840" href="/20.07/Confluence/#5840" class="Bound">p₂</a><a id="5842" class="Symbol">)</a> <a id="5844" class="Symbol">=</a>
|
||
<a id="5850" href="/20.07/Untyped/#11274" class="Function Operator">begin</a>
|
||
<a id="5860" class="Symbol">(</a><a id="5861" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5863" href="/20.07/Confluence/#5804" class="Bound">N</a><a id="5864" class="Symbol">)</a> <a id="5866" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="5868" href="/20.07/Confluence/#5809" class="Bound">M</a> <a id="5889" href="/20.07/Untyped/#21991" class="Function Operator">—↠⟨</a> <a id="5893" href="/20.07/Untyped/#22905" class="Function">appL-cong</a><a id="5902" class="Symbol">{</a><a id="5903" class="Argument">M</a> <a id="5905" class="Symbol">=</a> <a id="5907" href="/20.07/Confluence/#5809" class="Bound">M</a><a id="5908" class="Symbol">}</a> <a id="5910" class="Symbol">(</a><a id="5911" href="/20.07/Untyped/#23902" class="Function">abs-cong</a> <a id="5920" class="Symbol">(</a><a id="5921" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="5931" href="/20.07/Confluence/#5837" class="Bound">p₁</a><a id="5933" class="Symbol">))</a> <a id="5936" href="/20.07/Untyped/#21991" class="Function Operator">⟩</a>
|
||
<a id="5942" class="Symbol">(</a><a id="5943" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5945" href="/20.07/Confluence/#5824" class="Bound">N′</a><a id="5947" class="Symbol">)</a> <a id="5949" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="5951" href="/20.07/Confluence/#5809" class="Bound">M</a> <a id="5971" href="/20.07/Untyped/#21991" class="Function Operator">—↠⟨</a> <a id="5975" href="/20.07/Untyped/#23674" class="Function">appR-cong</a><a id="5984" class="Symbol">{</a><a id="5985" class="Argument">L</a> <a id="5987" class="Symbol">=</a> <a id="5989" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5991" href="/20.07/Confluence/#5824" class="Bound">N′</a><a id="5993" class="Symbol">}</a> <a id="5995" class="Symbol">(</a><a id="5996" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="6006" href="/20.07/Confluence/#5840" class="Bound">p₂</a><a id="6008" class="Symbol">)</a> <a id="6011" href="/20.07/Untyped/#21991" class="Function Operator">⟩</a>
|
||
<a id="6017" class="Symbol">(</a><a id="6018" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="6020" href="/20.07/Confluence/#5824" class="Bound">N′</a><a id="6022" class="Symbol">)</a> <a id="6024" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="6026" href="/20.07/Confluence/#5833" class="Bound">M′</a> <a id="6046" href="/20.07/Untyped/#11174" class="InductiveConstructor Operator">—→⟨</a> <a id="6050" href="/20.07/Untyped/#10178" class="InductiveConstructor">β</a> <a id="6052" href="/20.07/Untyped/#11174" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="6059" href="/20.07/Confluence/#5824" class="Bound">N′</a> <a id="6062" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="6064" href="/20.07/Confluence/#5833" class="Bound">M′</a> <a id="6067" href="/20.07/Untyped/#7491" class="Function Operator">]</a>
|
||
<a id="6073" href="/20.07/Untyped/#11118" class="InductiveConstructor Operator">∎</a>
|
||
</pre>
|
||
<p>The proof is by induction on <code class="language-plaintext highlighter-rouge">M ⇛ N</code>.</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">x ⇛ x</code>. We immediately have <code class="language-plaintext highlighter-rouge">x —↠ x</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">ƛ N ⇛ ƛ N′</code> because <code class="language-plaintext highlighter-rouge">N ⇛ N′</code>. By the induction hypothesis
|
||
we have <code class="language-plaintext highlighter-rouge">N —↠ N′</code>. We conclude that <code class="language-plaintext highlighter-rouge">ƛ N —↠ ƛ N′</code> because
|
||
<code class="language-plaintext highlighter-rouge">—↠</code> is a congruence.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">L · M ⇛ L′ · M′</code> because <code class="language-plaintext highlighter-rouge">L ⇛ L′</code> and <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>.
|
||
By the induction hypothesis, we have <code class="language-plaintext highlighter-rouge">L —↠ L′</code> and <code class="language-plaintext highlighter-rouge">M —↠ M′</code>.
|
||
So <code class="language-plaintext highlighter-rouge">L · M —↠ L′ · M</code> and then <code class="language-plaintext highlighter-rouge">L′ · M —↠ L′ · M′</code>
|
||
because <code class="language-plaintext highlighter-rouge">—↠</code> is a congruence.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ N′ [ M′ ]</code> because <code class="language-plaintext highlighter-rouge">N ⇛ N′</code> and <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>.
|
||
By similar reasoning, we have
|
||
<code class="language-plaintext highlighter-rouge">(ƛ N) · M —↠ (ƛ N′) · M′</code>
|
||
which we can following with the β reduction
|
||
<code class="language-plaintext highlighter-rouge">(ƛ N′) · M′ —→ N′ [ M′ ]</code>.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<p>With this lemma in hand, we complete the proof that <code class="language-plaintext highlighter-rouge">M ⇛* N</code> implies
|
||
<code class="language-plaintext highlighter-rouge">M —↠ N</code> with a simple induction on <code class="language-plaintext highlighter-rouge">M ⇛* N</code>.</p>
|
||
|
||
<pre class="Agda"><a id="pars-betas"></a><a id="6858" href="/20.07/Confluence/#6858" class="Function">pars-betas</a> <a id="6869" class="Symbol">:</a> <a id="6871" class="Symbol">∀{</a><a id="6873" href="/20.07/Confluence/#6873" class="Bound">Γ</a> <a id="6875" href="/20.07/Confluence/#6875" class="Bound">A</a><a id="6876" class="Symbol">}</a> <a id="6878" class="Symbol">{</a><a id="6879" href="/20.07/Confluence/#6879" class="Bound">M</a> <a id="6881" href="/20.07/Confluence/#6881" class="Bound">N</a> <a id="6883" class="Symbol">:</a> <a id="6885" href="/20.07/Confluence/#6873" class="Bound">Γ</a> <a id="6887" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="6889" href="/20.07/Confluence/#6875" class="Bound">A</a><a id="6890" class="Symbol">}</a>
|
||
<a id="6894" class="Symbol">→</a> <a id="6896" href="/20.07/Confluence/#6879" class="Bound">M</a> <a id="6898" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="6901" href="/20.07/Confluence/#6881" class="Bound">N</a>
|
||
<a id="6907" class="Comment">------</a>
|
||
<a id="6916" class="Symbol">→</a> <a id="6918" href="/20.07/Confluence/#6879" class="Bound">M</a> <a id="6920" href="/20.07/Untyped/#11068" class="Datatype Operator">—↠</a> <a id="6923" href="/20.07/Confluence/#6881" class="Bound">N</a>
|
||
<a id="6925" href="/20.07/Confluence/#6858" class="Function">pars-betas</a> <a id="6936" class="Symbol">(</a><a id="6937" href="/20.07/Confluence/#6937" class="Bound">M₁</a> <a id="6940" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">∎</a><a id="6941" class="Symbol">)</a> <a id="6943" class="Symbol">=</a> <a id="6945" href="/20.07/Confluence/#6937" class="Bound">M₁</a> <a id="6948" href="/20.07/Untyped/#11118" class="InductiveConstructor Operator">∎</a>
|
||
<a id="6950" href="/20.07/Confluence/#6858" class="Function">pars-betas</a> <a id="6961" class="Symbol">(</a><a id="6962" href="/20.07/Confluence/#6962" class="Bound">L</a> <a id="6964" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⇛⟨</a> <a id="6967" href="/20.07/Confluence/#6967" class="Bound">p</a> <a id="6969" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⟩</a> <a id="6971" href="/20.07/Confluence/#6971" class="Bound">ps</a><a id="6973" class="Symbol">)</a> <a id="6975" class="Symbol">=</a> <a id="6977" href="/20.07/Untyped/#21721" class="Function">—↠-trans</a> <a id="6986" class="Symbol">(</a><a id="6987" href="/20.07/Confluence/#5428" class="Function">par-betas</a> <a id="6997" href="/20.07/Confluence/#6967" class="Bound">p</a><a id="6998" class="Symbol">)</a> <a id="7000" class="Symbol">(</a><a id="7001" href="/20.07/Confluence/#6858" class="Function">pars-betas</a> <a id="7012" href="/20.07/Confluence/#6971" class="Bound">ps</a><a id="7014" class="Symbol">)</a>
|
||
</pre>
|
||
|
||
<h2 id="substitution-lemma-for-parallel-reduction">Substitution lemma for parallel reduction</h2>
|
||
|
||
<p>Our next goal is the prove the diamond property for parallel
|
||
reduction. But to do that, we need to prove that substitution
|
||
respects parallel reduction. That is, 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>.
|
||
We cannot prove this directly by induction, so we
|
||
generalize it to: if <code class="language-plaintext highlighter-rouge">N ⇛ N′</code> and
|
||
the substitution <code class="language-plaintext highlighter-rouge">σ</code> pointwise parallel reduces to <code class="language-plaintext highlighter-rouge">τ</code>,
|
||
then <code class="language-plaintext highlighter-rouge">subst σ N ⇛ subst τ N′</code>. We define the notion
|
||
of pointwise parallel reduction as follows.</p>
|
||
|
||
<pre class="Agda"><a id="par-subst"></a><a id="7524" href="/20.07/Confluence/#7524" class="Function">par-subst</a> <a id="7534" class="Symbol">:</a> <a id="7536" class="Symbol">∀{</a><a id="7538" href="/20.07/Confluence/#7538" class="Bound">Γ</a> <a id="7540" href="/20.07/Confluence/#7540" class="Bound">Δ</a><a id="7541" class="Symbol">}</a> <a id="7543" class="Symbol">→</a> <a id="7545" href="/20.07/Substitution/#2405" class="Function">Subst</a> <a id="7551" href="/20.07/Confluence/#7538" class="Bound">Γ</a> <a id="7553" href="/20.07/Confluence/#7540" class="Bound">Δ</a> <a id="7555" class="Symbol">→</a> <a id="7557" href="/20.07/Substitution/#2405" class="Function">Subst</a> <a id="7563" href="/20.07/Confluence/#7538" class="Bound">Γ</a> <a id="7565" href="/20.07/Confluence/#7540" class="Bound">Δ</a> <a id="7567" class="Symbol">→</a> <a id="7569" class="PrimitiveType">Set</a>
|
||
<a id="7573" href="/20.07/Confluence/#7524" class="Function">par-subst</a> <a id="7583" class="Symbol">{</a><a id="7584" href="/20.07/Confluence/#7584" class="Bound">Γ</a><a id="7585" class="Symbol">}{</a><a id="7587" href="/20.07/Confluence/#7587" class="Bound">Δ</a><a id="7588" class="Symbol">}</a> <a id="7590" href="/20.07/Confluence/#7590" class="Bound">σ</a> <a id="7592" href="/20.07/Confluence/#7592" class="Bound">σ′</a> <a id="7595" class="Symbol">=</a> <a id="7597" class="Symbol">∀{</a><a id="7599" href="/20.07/Confluence/#7599" class="Bound">A</a><a id="7600" class="Symbol">}{</a><a id="7602" href="/20.07/Confluence/#7602" class="Bound">x</a> <a id="7604" class="Symbol">:</a> <a id="7606" href="/20.07/Confluence/#7584" class="Bound">Γ</a> <a id="7608" href="/20.07/Untyped/#3521" class="Datatype Operator">∋</a> <a id="7610" href="/20.07/Confluence/#7599" class="Bound">A</a><a id="7611" class="Symbol">}</a> <a id="7613" class="Symbol">→</a> <a id="7615" href="/20.07/Confluence/#7590" class="Bound">σ</a> <a id="7617" href="/20.07/Confluence/#7602" class="Bound">x</a> <a id="7619" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="7621" href="/20.07/Confluence/#7592" class="Bound">σ′</a> <a id="7624" href="/20.07/Confluence/#7602" class="Bound">x</a>
|
||
</pre>
|
||
<p>Because substitution depends on the extension function <code class="language-plaintext highlighter-rouge">exts</code>, which
|
||
in turn relies on <code class="language-plaintext highlighter-rouge">rename</code>, we start with a version of the
|
||
substitution lemma, called <code class="language-plaintext highlighter-rouge">par-rename</code>, that is specialized to
|
||
renamings. The proof of <code class="language-plaintext highlighter-rouge">par-rename</code> relies on the fact that renaming
|
||
and substitution commute with one another, which is a lemma that we
|
||
import from Chapter <a href="/20.07/Substitution/">Substitution</a>
|
||
and restate here.</p>
|
||
|
||
<pre class="Agda"><a id="rename-subst-commute"></a><a id="8054" href="/20.07/Confluence/#8054" class="Function">rename-subst-commute</a> <a id="8075" class="Symbol">:</a> <a id="8077" class="Symbol">∀{</a><a id="8079" href="/20.07/Confluence/#8079" class="Bound">Γ</a> <a id="8081" href="/20.07/Confluence/#8081" class="Bound">Δ</a><a id="8082" class="Symbol">}{</a><a id="8084" href="/20.07/Confluence/#8084" class="Bound">N</a> <a id="8086" class="Symbol">:</a> <a id="8088" href="/20.07/Confluence/#8079" class="Bound">Γ</a> <a id="8090" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="8092" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a> <a id="8094" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="8096" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="8097" class="Symbol">}{</a><a id="8099" href="/20.07/Confluence/#8099" class="Bound">M</a> <a id="8101" class="Symbol">:</a> <a id="8103" href="/20.07/Confluence/#8079" class="Bound">Γ</a> <a id="8105" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="8107" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="8108" class="Symbol">}{</a><a id="8110" href="/20.07/Confluence/#8110" class="Bound">ρ</a> <a id="8112" class="Symbol">:</a> <a id="8114" href="/20.07/Substitution/#2192" class="Function">Rename</a> <a id="8121" href="/20.07/Confluence/#8079" class="Bound">Γ</a> <a id="8123" href="/20.07/Confluence/#8081" class="Bound">Δ</a> <a id="8125" class="Symbol">}</a>
|
||
<a id="8131" class="Symbol">→</a> <a id="8133" class="Symbol">(</a><a id="8134" href="/20.07/Untyped/#6235" class="Function">rename</a> <a id="8141" class="Symbol">(</a><a id="8142" href="/20.07/Untyped/#5925" class="Function">ext</a> <a id="8146" href="/20.07/Confluence/#8110" class="Bound">ρ</a><a id="8147" class="Symbol">)</a> <a id="8149" href="/20.07/Confluence/#8084" class="Bound">N</a><a id="8150" class="Symbol">)</a> <a id="8152" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="8154" href="/20.07/Untyped/#6235" class="Function">rename</a> <a id="8161" href="/20.07/Confluence/#8110" class="Bound">ρ</a> <a id="8163" href="/20.07/Confluence/#8099" class="Bound">M</a> <a id="8165" href="/20.07/Untyped/#7491" class="Function Operator">]</a> <a id="8167" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="8169" href="/20.07/Untyped/#6235" class="Function">rename</a> <a id="8176" href="/20.07/Confluence/#8110" class="Bound">ρ</a> <a id="8178" class="Symbol">(</a><a id="8179" href="/20.07/Confluence/#8084" class="Bound">N</a> <a id="8181" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="8183" href="/20.07/Confluence/#8099" class="Bound">M</a> <a id="8185" href="/20.07/Untyped/#7491" class="Function Operator">]</a><a id="8186" class="Symbol">)</a>
|
||
<a id="8188" href="/20.07/Confluence/#8054" class="Function">rename-subst-commute</a> <a id="8209" class="Symbol">{</a><a id="8210" class="Argument">N</a> <a id="8212" class="Symbol">=</a> <a id="8214" href="/20.07/Confluence/#8214" class="Bound">N</a><a id="8215" class="Symbol">}</a> <a id="8217" class="Symbol">=</a> <a id="8219" href="/20.07/Substitution/#27893" class="Function">plfa.part2.Substitution.rename-subst-commute</a> <a id="8264" class="Symbol">{</a><a id="8265" class="Argument">N</a> <a id="8267" class="Symbol">=</a> <a id="8269" href="/20.07/Confluence/#8214" class="Bound">N</a><a id="8270" class="Symbol">}</a>
|
||
</pre>
|
||
<p>Now for the <code class="language-plaintext highlighter-rouge">par-rename</code> lemma.</p>
|
||
|
||
<pre class="Agda"><a id="par-rename"></a><a id="8314" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8325" class="Symbol">:</a> <a id="8327" class="Symbol">∀{</a><a id="8329" href="/20.07/Confluence/#8329" class="Bound">Γ</a> <a id="8331" href="/20.07/Confluence/#8331" class="Bound">Δ</a> <a id="8333" href="/20.07/Confluence/#8333" class="Bound">A</a><a id="8334" class="Symbol">}</a> <a id="8336" class="Symbol">{</a><a id="8337" href="/20.07/Confluence/#8337" class="Bound">ρ</a> <a id="8339" class="Symbol">:</a> <a id="8341" href="/20.07/Substitution/#2192" class="Function">Rename</a> <a id="8348" href="/20.07/Confluence/#8329" class="Bound">Γ</a> <a id="8350" href="/20.07/Confluence/#8331" class="Bound">Δ</a><a id="8351" class="Symbol">}</a> <a id="8353" class="Symbol">{</a><a id="8354" href="/20.07/Confluence/#8354" class="Bound">M</a> <a id="8356" href="/20.07/Confluence/#8356" class="Bound">M′</a> <a id="8359" class="Symbol">:</a> <a id="8361" href="/20.07/Confluence/#8329" class="Bound">Γ</a> <a id="8363" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="8365" href="/20.07/Confluence/#8333" class="Bound">A</a><a id="8366" class="Symbol">}</a>
|
||
<a id="8370" class="Symbol">→</a> <a id="8372" href="/20.07/Confluence/#8354" class="Bound">M</a> <a id="8374" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="8376" href="/20.07/Confluence/#8356" class="Bound">M′</a>
|
||
<a id="8383" class="Comment">------------------------</a>
|
||
<a id="8410" class="Symbol">→</a> <a id="8412" href="/20.07/Untyped/#6235" class="Function">rename</a> <a id="8419" href="/20.07/Confluence/#8337" class="Bound">ρ</a> <a id="8421" href="/20.07/Confluence/#8354" class="Bound">M</a> <a id="8423" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="8425" href="/20.07/Untyped/#6235" class="Function">rename</a> <a id="8432" href="/20.07/Confluence/#8337" class="Bound">ρ</a> <a id="8434" href="/20.07/Confluence/#8356" class="Bound">M′</a>
|
||
<a id="8437" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8448" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a> <a id="8453" class="Symbol">=</a> <a id="8455" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a>
|
||
<a id="8460" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8471" class="Symbol">(</a><a id="8472" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="8477" href="/20.07/Confluence/#8477" class="Bound">p</a><a id="8478" class="Symbol">)</a> <a id="8480" class="Symbol">=</a> <a id="8482" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="8487" class="Symbol">(</a><a id="8488" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8499" href="/20.07/Confluence/#8477" class="Bound">p</a><a id="8500" class="Symbol">)</a>
|
||
<a id="8502" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8513" class="Symbol">(</a><a id="8514" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="8519" href="/20.07/Confluence/#8519" class="Bound">p₁</a> <a id="8522" href="/20.07/Confluence/#8522" class="Bound">p₂</a><a id="8524" class="Symbol">)</a> <a id="8526" class="Symbol">=</a> <a id="8528" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="8533" class="Symbol">(</a><a id="8534" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8545" href="/20.07/Confluence/#8519" class="Bound">p₁</a><a id="8547" class="Symbol">)</a> <a id="8549" class="Symbol">(</a><a id="8550" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8561" href="/20.07/Confluence/#8522" class="Bound">p₂</a><a id="8563" class="Symbol">)</a>
|
||
<a id="8565" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="8576" class="Symbol">{</a><a id="8577" href="/20.07/Confluence/#8577" class="Bound">Γ</a><a id="8578" class="Symbol">}{</a><a id="8580" href="/20.07/Confluence/#8580" class="Bound">Δ</a><a id="8581" class="Symbol">}{</a><a id="8583" href="/20.07/Confluence/#8583" class="Bound">A</a><a id="8584" class="Symbol">}{</a><a id="8586" href="/20.07/Confluence/#8586" class="Bound">ρ</a><a id="8587" class="Symbol">}</a> <a id="8589" class="Symbol">(</a><a id="8590" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a><a id="8595" class="Symbol">{</a><a id="8596" href="/20.07/Confluence/#8577" class="Bound">Γ</a><a id="8597" class="Symbol">}{</a><a id="8599" href="/20.07/Confluence/#8599" class="Bound">N</a><a id="8600" class="Symbol">}{</a><a id="8602" href="/20.07/Confluence/#8602" class="Bound">N′</a><a id="8604" class="Symbol">}{</a><a id="8606" href="/20.07/Confluence/#8606" class="Bound">M</a><a id="8607" class="Symbol">}{</a><a id="8609" href="/20.07/Confluence/#8609" class="Bound">M′</a><a id="8611" class="Symbol">}</a> <a id="8613" href="/20.07/Confluence/#8613" class="Bound">p₁</a> <a id="8616" href="/20.07/Confluence/#8616" class="Bound">p₂</a><a id="8618" class="Symbol">)</a>
|
||
<a id="8624" class="Keyword">with</a> <a id="8629" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="8635" class="Symbol">(</a><a id="8636" href="/20.07/Confluence/#8314" class="Function">par-rename</a><a id="8646" class="Symbol">{</a><a id="8647" class="Argument">ρ</a> <a id="8649" class="Symbol">=</a> <a id="8651" href="/20.07/Untyped/#5925" class="Function">ext</a> <a id="8655" href="/20.07/Confluence/#8586" class="Bound">ρ</a><a id="8656" class="Symbol">}</a> <a id="8658" href="/20.07/Confluence/#8613" class="Bound">p₁</a><a id="8660" class="Symbol">)</a> <a id="8662" class="Symbol">(</a><a id="8663" href="/20.07/Confluence/#8314" class="Function">par-rename</a><a id="8673" class="Symbol">{</a><a id="8674" class="Argument">ρ</a> <a id="8676" class="Symbol">=</a> <a id="8678" href="/20.07/Confluence/#8586" class="Bound">ρ</a><a id="8679" class="Symbol">}</a> <a id="8681" href="/20.07/Confluence/#8616" class="Bound">p₂</a><a id="8683" class="Symbol">)</a>
|
||
<a id="8685" class="Symbol">...</a> <a id="8689" class="Symbol">|</a> <a id="8691" href="/20.07/Confluence/#8691" class="Bound">G</a> <a id="8693" class="Keyword">rewrite</a> <a id="8701" href="/20.07/Confluence/#8054" class="Function">rename-subst-commute</a><a id="8721" class="Symbol">{</a><a id="8722" class="Bound">Γ</a><a id="8723" class="Symbol">}{</a><a id="8725" class="Bound">Δ</a><a id="8726" class="Symbol">}{</a><a id="8728" class="Bound">N′</a><a id="8730" class="Symbol">}{</a><a id="8732" class="Bound">M′</a><a id="8734" class="Symbol">}{</a><a id="8736" class="Bound">ρ</a><a id="8737" class="Symbol">}</a> <a id="8739" class="Symbol">=</a> <a id="8741" href="/20.07/Confluence/#8691" class="Bound">G</a>
|
||
|
||
</pre>
|
||
<p>The proof is by induction on <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>. The first four cases
|
||
are straightforward so we just consider the last one for <code class="language-plaintext highlighter-rouge">pbeta</code>.</p>
|
||
|
||
<ul>
|
||
<li>Suppose <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ N′ [ M′ ]</code> because <code class="language-plaintext highlighter-rouge">N ⇛ N′</code> and <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>.
|
||
By the induction hypothesis, we have
|
||
<code class="language-plaintext highlighter-rouge">rename (ext ρ) N ⇛ rename (ext ρ) N′</code> and
|
||
<code class="language-plaintext highlighter-rouge">rename ρ M ⇛ rename ρ M′</code>.
|
||
So by <code class="language-plaintext highlighter-rouge">pbeta</code> we have
|
||
<code class="language-plaintext highlighter-rouge">(ƛ rename (ext ρ) N) · (rename ρ M) ⇛ (rename (ext ρ) N) [ rename ρ M ]</code>.
|
||
However, to conclude we instead need parallel reduction to
|
||
<code class="language-plaintext highlighter-rouge">rename ρ (N [ M ])</code>. But thankfully, renaming and substitution
|
||
commute with one another.</li>
|
||
</ul>
|
||
|
||
<p>With the <code class="language-plaintext highlighter-rouge">par-rename</code> lemma in hand, it is straightforward to show
|
||
that extending substitutions preserves the pointwise parallel
|
||
reduction relation.</p>
|
||
|
||
<pre class="Agda"><a id="par-subst-exts"></a><a id="9469" href="/20.07/Confluence/#9469" class="Function">par-subst-exts</a> <a id="9484" class="Symbol">:</a> <a id="9486" class="Symbol">∀{</a><a id="9488" href="/20.07/Confluence/#9488" class="Bound">Γ</a> <a id="9490" href="/20.07/Confluence/#9490" class="Bound">Δ</a><a id="9491" class="Symbol">}</a> <a id="9493" class="Symbol">{</a><a id="9494" href="/20.07/Confluence/#9494" class="Bound">σ</a> <a id="9496" href="/20.07/Confluence/#9496" class="Bound">τ</a> <a id="9498" class="Symbol">:</a> <a id="9500" href="/20.07/Substitution/#2405" class="Function">Subst</a> <a id="9506" href="/20.07/Confluence/#9488" class="Bound">Γ</a> <a id="9508" href="/20.07/Confluence/#9490" class="Bound">Δ</a><a id="9509" class="Symbol">}</a>
|
||
<a id="9513" class="Symbol">→</a> <a id="9515" href="/20.07/Confluence/#7524" class="Function">par-subst</a> <a id="9525" href="/20.07/Confluence/#9494" class="Bound">σ</a> <a id="9527" href="/20.07/Confluence/#9496" class="Bound">τ</a>
|
||
<a id="9533" class="Comment">------------------------------------------</a>
|
||
<a id="9578" class="Symbol">→</a> <a id="9580" class="Symbol">∀{</a><a id="9582" href="/20.07/Confluence/#9582" class="Bound">B</a><a id="9583" class="Symbol">}</a> <a id="9585" class="Symbol">→</a> <a id="9587" href="/20.07/Confluence/#7524" class="Function">par-subst</a> <a id="9597" class="Symbol">(</a><a id="9598" href="/20.07/Untyped/#6671" class="Function">exts</a> <a id="9603" href="/20.07/Confluence/#9494" class="Bound">σ</a> <a id="9605" class="Symbol">{</a><a id="9606" class="Argument">B</a> <a id="9608" class="Symbol">=</a> <a id="9610" href="/20.07/Confluence/#9582" class="Bound">B</a><a id="9611" class="Symbol">})</a> <a id="9614" class="Symbol">(</a><a id="9615" href="/20.07/Untyped/#6671" class="Function">exts</a> <a id="9620" href="/20.07/Confluence/#9496" class="Bound">τ</a><a id="9621" class="Symbol">)</a>
|
||
<a id="9623" href="/20.07/Confluence/#9469" class="Function">par-subst-exts</a> <a id="9638" href="/20.07/Confluence/#9638" class="Bound">s</a> <a id="9640" class="Symbol">{</a><a id="9641" class="Argument">x</a> <a id="9643" class="Symbol">=</a> <a id="9645" href="/20.07/Untyped/#3557" class="InductiveConstructor">Z</a><a id="9646" class="Symbol">}</a> <a id="9648" class="Symbol">=</a> <a id="9650" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a>
|
||
<a id="9655" href="/20.07/Confluence/#9469" class="Function">par-subst-exts</a> <a id="9670" href="/20.07/Confluence/#9670" class="Bound">s</a> <a id="9672" class="Symbol">{</a><a id="9673" class="Argument">x</a> <a id="9675" class="Symbol">=</a> <a id="9677" href="/20.07/Untyped/#3602" class="InductiveConstructor Operator">S</a> <a id="9679" href="/20.07/Confluence/#9679" class="Bound">x</a><a id="9680" class="Symbol">}</a> <a id="9682" class="Symbol">=</a> <a id="9684" href="/20.07/Confluence/#8314" class="Function">par-rename</a> <a id="9695" href="/20.07/Confluence/#9670" class="Bound">s</a>
|
||
</pre>
|
||
<p>The next lemma that we need for proving that substitution respects
|
||
parallel reduction is the following which states that
|
||
simultaneoous substitution commutes with single substitution. We import this
|
||
lemma from Chapter <a href="/20.07/Substitution/">Substitution</a>
|
||
and restate it below.</p>
|
||
|
||
<pre class="Agda"><a id="subst-commute"></a><a id="9995" href="/20.07/Confluence/#9995" class="Function">subst-commute</a> <a id="10009" class="Symbol">:</a> <a id="10011" class="Symbol">∀{</a><a id="10013" href="/20.07/Confluence/#10013" class="Bound">Γ</a> <a id="10015" href="/20.07/Confluence/#10015" class="Bound">Δ</a><a id="10016" class="Symbol">}{</a><a id="10018" href="/20.07/Confluence/#10018" class="Bound">N</a> <a id="10020" class="Symbol">:</a> <a id="10022" href="/20.07/Confluence/#10013" class="Bound">Γ</a> <a id="10024" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="10026" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a> <a id="10028" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="10030" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="10031" class="Symbol">}{</a><a id="10033" href="/20.07/Confluence/#10033" class="Bound">M</a> <a id="10035" class="Symbol">:</a> <a id="10037" href="/20.07/Confluence/#10013" class="Bound">Γ</a> <a id="10039" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="10041" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="10042" class="Symbol">}{</a><a id="10044" href="/20.07/Confluence/#10044" class="Bound">σ</a> <a id="10046" class="Symbol">:</a> <a id="10048" href="/20.07/Substitution/#2405" class="Function">Subst</a> <a id="10054" href="/20.07/Confluence/#10013" class="Bound">Γ</a> <a id="10056" href="/20.07/Confluence/#10015" class="Bound">Δ</a> <a id="10058" class="Symbol">}</a>
|
||
<a id="10062" class="Symbol">→</a> <a id="10064" href="/20.07/Untyped/#6963" class="Function">subst</a> <a id="10070" class="Symbol">(</a><a id="10071" href="/20.07/Untyped/#6671" class="Function">exts</a> <a id="10076" href="/20.07/Confluence/#10044" class="Bound">σ</a><a id="10077" class="Symbol">)</a> <a id="10079" href="/20.07/Confluence/#10018" class="Bound">N</a> <a id="10081" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="10083" href="/20.07/Untyped/#6963" class="Function">subst</a> <a id="10089" href="/20.07/Confluence/#10044" class="Bound">σ</a> <a id="10091" href="/20.07/Confluence/#10033" class="Bound">M</a> <a id="10093" href="/20.07/Untyped/#7491" class="Function Operator">]</a> <a id="10095" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="10097" href="/20.07/Untyped/#6963" class="Function">subst</a> <a id="10103" href="/20.07/Confluence/#10044" class="Bound">σ</a> <a id="10105" class="Symbol">(</a><a id="10106" href="/20.07/Confluence/#10018" class="Bound">N</a> <a id="10108" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="10110" href="/20.07/Confluence/#10033" class="Bound">M</a> <a id="10112" href="/20.07/Untyped/#7491" class="Function Operator">]</a><a id="10113" class="Symbol">)</a>
|
||
<a id="10115" href="/20.07/Confluence/#9995" class="Function">subst-commute</a> <a id="10129" class="Symbol">{</a><a id="10130" class="Argument">N</a> <a id="10132" class="Symbol">=</a> <a id="10134" href="/20.07/Confluence/#10134" class="Bound">N</a><a id="10135" class="Symbol">}</a> <a id="10137" class="Symbol">=</a> <a id="10139" href="/20.07/Substitution/#26352" class="Function">plfa.part2.Substitution.subst-commute</a> <a id="10177" class="Symbol">{</a><a id="10178" class="Argument">N</a> <a id="10180" class="Symbol">=</a> <a id="10182" href="/20.07/Confluence/#10134" class="Bound">N</a><a id="10183" class="Symbol">}</a>
|
||
</pre>
|
||
<p>We are ready to prove that substitution respects parallel reduction.</p>
|
||
|
||
<pre class="Agda"><a id="subst-par"></a><a id="10264" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10274" class="Symbol">:</a> <a id="10276" class="Symbol">∀{</a><a id="10278" href="/20.07/Confluence/#10278" class="Bound">Γ</a> <a id="10280" href="/20.07/Confluence/#10280" class="Bound">Δ</a> <a id="10282" href="/20.07/Confluence/#10282" class="Bound">A</a><a id="10283" class="Symbol">}</a> <a id="10285" class="Symbol">{</a><a id="10286" href="/20.07/Confluence/#10286" class="Bound">σ</a> <a id="10288" href="/20.07/Confluence/#10288" class="Bound">τ</a> <a id="10290" class="Symbol">:</a> <a id="10292" href="/20.07/Substitution/#2405" class="Function">Subst</a> <a id="10298" href="/20.07/Confluence/#10278" class="Bound">Γ</a> <a id="10300" href="/20.07/Confluence/#10280" class="Bound">Δ</a><a id="10301" class="Symbol">}</a> <a id="10303" class="Symbol">{</a><a id="10304" href="/20.07/Confluence/#10304" class="Bound">M</a> <a id="10306" href="/20.07/Confluence/#10306" class="Bound">M′</a> <a id="10309" class="Symbol">:</a> <a id="10311" href="/20.07/Confluence/#10278" class="Bound">Γ</a> <a id="10313" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="10315" href="/20.07/Confluence/#10282" class="Bound">A</a><a id="10316" class="Symbol">}</a>
|
||
<a id="10320" class="Symbol">→</a> <a id="10322" href="/20.07/Confluence/#7524" class="Function">par-subst</a> <a id="10332" href="/20.07/Confluence/#10286" class="Bound">σ</a> <a id="10334" href="/20.07/Confluence/#10288" class="Bound">τ</a> <a id="10337" class="Symbol">→</a> <a id="10340" href="/20.07/Confluence/#10304" class="Bound">M</a> <a id="10342" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="10344" href="/20.07/Confluence/#10306" class="Bound">M′</a>
|
||
<a id="10351" class="Comment">--------------------------</a>
|
||
<a id="10380" class="Symbol">→</a> <a id="10382" href="/20.07/Untyped/#6963" class="Function">subst</a> <a id="10388" href="/20.07/Confluence/#10286" class="Bound">σ</a> <a id="10390" href="/20.07/Confluence/#10304" class="Bound">M</a> <a id="10392" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="10394" href="/20.07/Untyped/#6963" class="Function">subst</a> <a id="10400" href="/20.07/Confluence/#10288" class="Bound">τ</a> <a id="10402" href="/20.07/Confluence/#10306" class="Bound">M′</a>
|
||
<a id="10405" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10415" class="Symbol">{</a><a id="10416" href="/20.07/Confluence/#10416" class="Bound">Γ</a><a id="10417" class="Symbol">}</a> <a id="10419" class="Symbol">{</a><a id="10420" href="/20.07/Confluence/#10420" class="Bound">Δ</a><a id="10421" class="Symbol">}</a> <a id="10423" class="Symbol">{</a><a id="10424" href="/20.07/Confluence/#10424" class="Bound">A</a><a id="10425" class="Symbol">}</a> <a id="10427" class="Symbol">{</a><a id="10428" href="/20.07/Confluence/#10428" class="Bound">σ</a><a id="10429" class="Symbol">}</a> <a id="10431" class="Symbol">{</a><a id="10432" href="/20.07/Confluence/#10432" class="Bound">τ</a><a id="10433" class="Symbol">}</a> <a id="10435" class="Symbol">{</a><a id="10436" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="10438" href="/20.07/Confluence/#10438" class="Bound">x</a><a id="10439" class="Symbol">}</a> <a id="10441" href="/20.07/Confluence/#10441" class="Bound">s</a> <a id="10443" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a> <a id="10448" class="Symbol">=</a> <a id="10450" href="/20.07/Confluence/#10441" class="Bound">s</a>
|
||
<a id="10452" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10462" class="Symbol">{</a><a id="10463" href="/20.07/Confluence/#10463" class="Bound">Γ</a><a id="10464" class="Symbol">}</a> <a id="10466" class="Symbol">{</a><a id="10467" href="/20.07/Confluence/#10467" class="Bound">Δ</a><a id="10468" class="Symbol">}</a> <a id="10470" class="Symbol">{</a><a id="10471" href="/20.07/Confluence/#10471" class="Bound">A</a><a id="10472" class="Symbol">}</a> <a id="10474" class="Symbol">{</a><a id="10475" href="/20.07/Confluence/#10475" class="Bound">σ</a><a id="10476" class="Symbol">}</a> <a id="10478" class="Symbol">{</a><a id="10479" href="/20.07/Confluence/#10479" class="Bound">τ</a><a id="10480" class="Symbol">}</a> <a id="10482" class="Symbol">{</a><a id="10483" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="10485" href="/20.07/Confluence/#10485" class="Bound">N</a><a id="10486" class="Symbol">}</a> <a id="10488" href="/20.07/Confluence/#10488" class="Bound">s</a> <a id="10490" class="Symbol">(</a><a id="10491" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="10496" href="/20.07/Confluence/#10496" class="Bound">p</a><a id="10497" class="Symbol">)</a> <a id="10499" class="Symbol">=</a>
|
||
<a id="10503" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="10508" class="Symbol">(</a><a id="10509" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10519" class="Symbol">{</a><a id="10520" class="Argument">σ</a> <a id="10522" class="Symbol">=</a> <a id="10524" href="/20.07/Untyped/#6671" class="Function">exts</a> <a id="10529" href="/20.07/Confluence/#10475" class="Bound">σ</a><a id="10530" class="Symbol">}</a> <a id="10532" class="Symbol">{</a><a id="10533" class="Argument">τ</a> <a id="10535" class="Symbol">=</a> <a id="10537" href="/20.07/Untyped/#6671" class="Function">exts</a> <a id="10542" href="/20.07/Confluence/#10479" class="Bound">τ</a><a id="10543" class="Symbol">}</a>
|
||
<a id="10553" class="Symbol">(λ</a> <a id="10556" class="Symbol">{</a><a id="10557" href="/20.07/Confluence/#10557" class="Bound">A</a><a id="10558" class="Symbol">}{</a><a id="10560" href="/20.07/Confluence/#10560" class="Bound">x</a><a id="10561" class="Symbol">}</a> <a id="10563" class="Symbol">→</a> <a id="10565" href="/20.07/Confluence/#9469" class="Function">par-subst-exts</a> <a id="10580" href="/20.07/Confluence/#10488" class="Bound">s</a> <a id="10582" class="Symbol">{</a><a id="10583" class="Argument">x</a> <a id="10585" class="Symbol">=</a> <a id="10587" href="/20.07/Confluence/#10560" class="Bound">x</a><a id="10588" class="Symbol">})</a> <a id="10591" href="/20.07/Confluence/#10496" class="Bound">p</a><a id="10592" class="Symbol">)</a>
|
||
<a id="10594" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10604" class="Symbol">{</a><a id="10605" href="/20.07/Confluence/#10605" class="Bound">Γ</a><a id="10606" class="Symbol">}</a> <a id="10608" class="Symbol">{</a><a id="10609" href="/20.07/Confluence/#10609" class="Bound">Δ</a><a id="10610" class="Symbol">}</a> <a id="10612" class="Symbol">{</a><a id="10613" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="10614" class="Symbol">}</a> <a id="10616" class="Symbol">{</a><a id="10617" href="/20.07/Confluence/#10617" class="Bound">σ</a><a id="10618" class="Symbol">}</a> <a id="10620" class="Symbol">{</a><a id="10621" href="/20.07/Confluence/#10621" class="Bound">τ</a><a id="10622" class="Symbol">}</a> <a id="10624" class="Symbol">{</a><a id="10625" href="/20.07/Confluence/#10625" class="Bound">L</a> <a id="10627" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="10629" href="/20.07/Confluence/#10629" class="Bound">M</a><a id="10630" class="Symbol">}</a> <a id="10632" href="/20.07/Confluence/#10632" class="Bound">s</a> <a id="10634" class="Symbol">(</a><a id="10635" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="10640" href="/20.07/Confluence/#10640" class="Bound">p₁</a> <a id="10643" href="/20.07/Confluence/#10643" class="Bound">p₂</a><a id="10645" class="Symbol">)</a> <a id="10647" class="Symbol">=</a>
|
||
<a id="10651" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="10656" class="Symbol">(</a><a id="10657" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10667" href="/20.07/Confluence/#10632" class="Bound">s</a> <a id="10669" href="/20.07/Confluence/#10640" class="Bound">p₁</a><a id="10671" class="Symbol">)</a> <a id="10673" class="Symbol">(</a><a id="10674" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10684" href="/20.07/Confluence/#10632" class="Bound">s</a> <a id="10686" href="/20.07/Confluence/#10643" class="Bound">p₂</a><a id="10688" class="Symbol">)</a>
|
||
<a id="10690" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10700" class="Symbol">{</a><a id="10701" href="/20.07/Confluence/#10701" class="Bound">Γ</a><a id="10702" class="Symbol">}</a> <a id="10704" class="Symbol">{</a><a id="10705" href="/20.07/Confluence/#10705" class="Bound">Δ</a><a id="10706" class="Symbol">}</a> <a id="10708" class="Symbol">{</a><a id="10709" href="/20.07/Untyped/#2888" class="InductiveConstructor">★</a><a id="10710" class="Symbol">}</a> <a id="10712" class="Symbol">{</a><a id="10713" href="/20.07/Confluence/#10713" class="Bound">σ</a><a id="10714" class="Symbol">}</a> <a id="10716" class="Symbol">{</a><a id="10717" href="/20.07/Confluence/#10717" class="Bound">τ</a><a id="10718" class="Symbol">}</a> <a id="10720" class="Symbol">{(</a><a id="10722" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="10724" href="/20.07/Confluence/#10724" class="Bound">N</a><a id="10725" class="Symbol">)</a> <a id="10727" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="10729" href="/20.07/Confluence/#10729" class="Bound">M</a><a id="10730" class="Symbol">}</a> <a id="10732" href="/20.07/Confluence/#10732" class="Bound">s</a> <a id="10734" class="Symbol">(</a><a id="10735" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a><a id="10740" class="Symbol">{</a><a id="10741" class="Argument">N′</a> <a id="10744" class="Symbol">=</a> <a id="10746" href="/20.07/Confluence/#10746" class="Bound">N′</a><a id="10748" class="Symbol">}{</a><a id="10750" class="Argument">M′</a> <a id="10753" class="Symbol">=</a> <a id="10755" href="/20.07/Confluence/#10755" class="Bound">M′</a><a id="10757" class="Symbol">}</a> <a id="10759" href="/20.07/Confluence/#10759" class="Bound">p₁</a> <a id="10762" href="/20.07/Confluence/#10762" class="Bound">p₂</a><a id="10764" class="Symbol">)</a>
|
||
<a id="10770" class="Keyword">with</a> <a id="10775" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="10781" class="Symbol">(</a><a id="10782" href="/20.07/Confluence/#10264" class="Function">subst-par</a><a id="10791" class="Symbol">{</a><a id="10792" class="Argument">σ</a> <a id="10794" class="Symbol">=</a> <a id="10796" href="/20.07/Untyped/#6671" class="Function">exts</a> <a id="10801" href="/20.07/Confluence/#10713" class="Bound">σ</a><a id="10802" class="Symbol">}{</a><a id="10804" class="Argument">τ</a> <a id="10806" class="Symbol">=</a> <a id="10808" href="/20.07/Untyped/#6671" class="Function">exts</a> <a id="10813" href="/20.07/Confluence/#10717" class="Bound">τ</a><a id="10814" class="Symbol">}{</a><a id="10816" class="Argument">M</a> <a id="10818" class="Symbol">=</a> <a id="10820" href="/20.07/Confluence/#10724" class="Bound">N</a><a id="10821" class="Symbol">}</a>
|
||
<a id="10847" class="Symbol">(λ{</a><a id="10850" href="/20.07/Confluence/#10850" class="Bound">A</a><a id="10851" class="Symbol">}{</a><a id="10853" href="/20.07/Confluence/#10853" class="Bound">x</a><a id="10854" class="Symbol">}</a> <a id="10856" class="Symbol">→</a> <a id="10858" href="/20.07/Confluence/#9469" class="Function">par-subst-exts</a> <a id="10873" href="/20.07/Confluence/#10732" class="Bound">s</a> <a id="10875" class="Symbol">{</a><a id="10876" class="Argument">x</a> <a id="10878" class="Symbol">=</a> <a id="10880" href="/20.07/Confluence/#10853" class="Bound">x</a><a id="10881" class="Symbol">})</a> <a id="10884" href="/20.07/Confluence/#10759" class="Bound">p₁</a><a id="10886" class="Symbol">)</a>
|
||
<a id="10903" class="Symbol">(</a><a id="10904" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="10914" class="Symbol">{</a><a id="10915" class="Argument">σ</a> <a id="10917" class="Symbol">=</a> <a id="10919" href="/20.07/Confluence/#10713" class="Bound">σ</a><a id="10920" class="Symbol">}</a> <a id="10922" href="/20.07/Confluence/#10732" class="Bound">s</a> <a id="10924" href="/20.07/Confluence/#10762" class="Bound">p₂</a><a id="10926" class="Symbol">)</a>
|
||
<a id="10928" class="Symbol">...</a> <a id="10932" class="Symbol">|</a> <a id="10934" href="/20.07/Confluence/#10934" class="Bound">G</a> <a id="10936" class="Keyword">rewrite</a> <a id="10944" href="/20.07/Confluence/#9995" class="Function">subst-commute</a><a id="10957" class="Symbol">{</a><a id="10958" class="Argument">N</a> <a id="10960" class="Symbol">=</a> <a id="10962" class="Bound">N′</a><a id="10964" class="Symbol">}{</a><a id="10966" class="Argument">M</a> <a id="10968" class="Symbol">=</a> <a id="10970" class="Bound">M′</a><a id="10972" class="Symbol">}{</a><a id="10974" class="Argument">σ</a> <a id="10976" class="Symbol">=</a> <a id="10978" class="Bound">τ</a><a id="10979" class="Symbol">}</a> <a id="10981" class="Symbol">=</a> <a id="10983" href="/20.07/Confluence/#10934" class="Bound">G</a>
|
||
</pre>
|
||
<p>We proceed by induction on <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>.</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">x ⇛ x</code>. We conclude that <code class="language-plaintext highlighter-rouge">σ x ⇛ τ x</code> using
|
||
the premise <code class="language-plaintext highlighter-rouge">par-subst σ τ</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">ƛ N ⇛ ƛ N′</code> because <code class="language-plaintext highlighter-rouge">N ⇛ N′</code>.
|
||
To use the induction hypothesis, we need <code class="language-plaintext highlighter-rouge">par-subst (exts σ) (exts τ)</code>,
|
||
which we obtain by <code class="language-plaintext highlighter-rouge">par-subst-exts</code>.
|
||
So we have <code class="language-plaintext highlighter-rouge">subst (exts σ) N ⇛ subst (exts τ) N′</code>
|
||
and conclude by rule <code class="language-plaintext highlighter-rouge">pabs</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">L · M ⇛ L′ · M′</code> because <code class="language-plaintext highlighter-rouge">L ⇛ L′</code> and <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>.
|
||
By the induction hypothesis we have
|
||
<code class="language-plaintext highlighter-rouge">subst σ L ⇛ subst τ L′</code> and <code class="language-plaintext highlighter-rouge">subst σ M ⇛ subst τ M′</code>, so
|
||
we conclude by rule <code class="language-plaintext highlighter-rouge">papp</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ N′ [ M′ ]</code> because <code class="language-plaintext highlighter-rouge">N ⇛ N′</code> and <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>.
|
||
Again we obtain <code class="language-plaintext highlighter-rouge">par-subst (exts σ) (exts τ)</code> by <code class="language-plaintext highlighter-rouge">par-subst-exts</code>.
|
||
So by the induction hypothesis, we have
|
||
<code class="language-plaintext highlighter-rouge">subst (exts σ) N ⇛ subst (exts τ) N′</code> and
|
||
<code class="language-plaintext highlighter-rouge">subst σ M ⇛ subst τ M′</code>. Then by rule <code class="language-plaintext highlighter-rouge">pbeta</code>, we have parallel reduction
|
||
to <code class="language-plaintext highlighter-rouge">subst (exts τ) N′ [ subst τ M′ ]</code>.
|
||
Substitution commutes with itself in the following sense.
|
||
For any σ, N, and M, we have</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> (subst (exts σ) N) [ subst σ M ] ≡ subst σ (N [ M ])
|
||
</code></pre></div> </div>
|
||
|
||
<p>So we have parallel reduction to <code class="language-plaintext highlighter-rouge">subst τ (N′ [ M′ ])</code>.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<p>Of course, if <code class="language-plaintext highlighter-rouge">M ⇛ M′</code>, then <code class="language-plaintext highlighter-rouge">subst-zero M</code> pointwise parallel reduces
|
||
to <code class="language-plaintext highlighter-rouge">subst-zero M′</code>.</p>
|
||
|
||
<pre class="Agda"><a id="par-subst-zero"></a><a id="12191" href="/20.07/Confluence/#12191" class="Function">par-subst-zero</a> <a id="12206" class="Symbol">:</a> <a id="12208" class="Symbol">∀{</a><a id="12210" href="/20.07/Confluence/#12210" class="Bound">Γ</a><a id="12211" class="Symbol">}{</a><a id="12213" href="/20.07/Confluence/#12213" class="Bound">A</a><a id="12214" class="Symbol">}{</a><a id="12216" href="/20.07/Confluence/#12216" class="Bound">M</a> <a id="12218" href="/20.07/Confluence/#12218" class="Bound">M′</a> <a id="12221" class="Symbol">:</a> <a id="12223" href="/20.07/Confluence/#12210" class="Bound">Γ</a> <a id="12225" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="12227" href="/20.07/Confluence/#12213" class="Bound">A</a><a id="12228" class="Symbol">}</a>
|
||
<a id="12237" class="Symbol">→</a> <a id="12239" href="/20.07/Confluence/#12216" class="Bound">M</a> <a id="12241" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="12243" href="/20.07/Confluence/#12218" class="Bound">M′</a>
|
||
<a id="12253" class="Symbol">→</a> <a id="12255" href="/20.07/Confluence/#7524" class="Function">par-subst</a> <a id="12265" class="Symbol">(</a><a id="12266" href="/20.07/Untyped/#7375" class="Function">subst-zero</a> <a id="12277" href="/20.07/Confluence/#12216" class="Bound">M</a><a id="12278" class="Symbol">)</a> <a id="12280" class="Symbol">(</a><a id="12281" href="/20.07/Untyped/#7375" class="Function">subst-zero</a> <a id="12292" href="/20.07/Confluence/#12218" class="Bound">M′</a><a id="12294" class="Symbol">)</a>
|
||
<a id="12296" href="/20.07/Confluence/#12191" class="Function">par-subst-zero</a> <a id="12311" class="Symbol">{</a><a id="12312" href="/20.07/Confluence/#12312" class="Bound">M</a><a id="12313" class="Symbol">}</a> <a id="12315" class="Symbol">{</a><a id="12316" href="/20.07/Confluence/#12316" class="Bound">M′</a><a id="12318" class="Symbol">}</a> <a id="12320" href="/20.07/Confluence/#12320" class="Bound">p</a> <a id="12322" class="Symbol">{</a><a id="12323" href="/20.07/Confluence/#12323" class="Bound">A</a><a id="12324" class="Symbol">}</a> <a id="12326" class="Symbol">{</a><a id="12327" href="/20.07/Untyped/#3557" class="InductiveConstructor">Z</a><a id="12328" class="Symbol">}</a> <a id="12330" class="Symbol">=</a> <a id="12332" href="/20.07/Confluence/#12320" class="Bound">p</a>
|
||
<a id="12334" href="/20.07/Confluence/#12191" class="Function">par-subst-zero</a> <a id="12349" class="Symbol">{</a><a id="12350" href="/20.07/Confluence/#12350" class="Bound">M</a><a id="12351" class="Symbol">}</a> <a id="12353" class="Symbol">{</a><a id="12354" href="/20.07/Confluence/#12354" class="Bound">M′</a><a id="12356" class="Symbol">}</a> <a id="12358" href="/20.07/Confluence/#12358" class="Bound">p</a> <a id="12360" class="Symbol">{</a><a id="12361" href="/20.07/Confluence/#12361" class="Bound">A</a><a id="12362" class="Symbol">}</a> <a id="12364" class="Symbol">{</a><a id="12365" href="/20.07/Untyped/#3602" class="InductiveConstructor Operator">S</a> <a id="12367" href="/20.07/Confluence/#12367" class="Bound">x</a><a id="12368" class="Symbol">}</a> <a id="12370" class="Symbol">=</a> <a id="12372" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a>
|
||
</pre>
|
||
<p>We conclude this section with the desired corollary, that substitution
|
||
respects parallel reduction.</p>
|
||
|
||
<pre class="Agda"><a id="sub-par"></a><a id="12487" href="/20.07/Confluence/#12487" class="Function">sub-par</a> <a id="12495" class="Symbol">:</a> <a id="12497" class="Symbol">∀{</a><a id="12499" href="/20.07/Confluence/#12499" class="Bound">Γ</a> <a id="12501" href="/20.07/Confluence/#12501" class="Bound">A</a> <a id="12503" href="/20.07/Confluence/#12503" class="Bound">B</a><a id="12504" class="Symbol">}</a> <a id="12506" class="Symbol">{</a><a id="12507" href="/20.07/Confluence/#12507" class="Bound">N</a> <a id="12509" href="/20.07/Confluence/#12509" class="Bound">N′</a> <a id="12512" class="Symbol">:</a> <a id="12514" href="/20.07/Confluence/#12499" class="Bound">Γ</a> <a id="12516" href="/20.07/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="12518" href="/20.07/Confluence/#12501" class="Bound">A</a> <a id="12520" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="12522" href="/20.07/Confluence/#12503" class="Bound">B</a><a id="12523" class="Symbol">}</a> <a id="12525" class="Symbol">{</a><a id="12526" href="/20.07/Confluence/#12526" class="Bound">M</a> <a id="12528" href="/20.07/Confluence/#12528" class="Bound">M′</a> <a id="12531" class="Symbol">:</a> <a id="12533" href="/20.07/Confluence/#12499" class="Bound">Γ</a> <a id="12535" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="12537" href="/20.07/Confluence/#12501" class="Bound">A</a><a id="12538" class="Symbol">}</a>
|
||
<a id="12542" class="Symbol">→</a> <a id="12544" href="/20.07/Confluence/#12507" class="Bound">N</a> <a id="12546" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="12548" href="/20.07/Confluence/#12509" class="Bound">N′</a>
|
||
<a id="12553" class="Symbol">→</a> <a id="12555" href="/20.07/Confluence/#12526" class="Bound">M</a> <a id="12557" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="12559" href="/20.07/Confluence/#12528" class="Bound">M′</a>
|
||
<a id="12566" class="Comment">--------------------------</a>
|
||
<a id="12595" class="Symbol">→</a> <a id="12597" href="/20.07/Confluence/#12507" class="Bound">N</a> <a id="12599" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="12601" href="/20.07/Confluence/#12526" class="Bound">M</a> <a id="12603" href="/20.07/Untyped/#7491" class="Function Operator">]</a> <a id="12605" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="12607" href="/20.07/Confluence/#12509" class="Bound">N′</a> <a id="12610" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="12612" href="/20.07/Confluence/#12528" class="Bound">M′</a> <a id="12615" href="/20.07/Untyped/#7491" class="Function Operator">]</a>
|
||
<a id="12617" href="/20.07/Confluence/#12487" class="Function">sub-par</a> <a id="12625" href="/20.07/Confluence/#12625" class="Bound">pn</a> <a id="12628" href="/20.07/Confluence/#12628" class="Bound">pm</a> <a id="12631" class="Symbol">=</a> <a id="12633" href="/20.07/Confluence/#10264" class="Function">subst-par</a> <a id="12643" class="Symbol">(</a><a id="12644" href="/20.07/Confluence/#12191" class="Function">par-subst-zero</a> <a id="12659" href="/20.07/Confluence/#12628" class="Bound">pm</a><a id="12661" class="Symbol">)</a> <a id="12663" href="/20.07/Confluence/#12625" class="Bound">pn</a>
|
||
</pre>
|
||
|
||
<h2 id="parallel-reduction-satisfies-the-diamond-property">Parallel reduction satisfies the diamond property</h2>
|
||
|
||
<p>The heart of the confluence proof is made of stone, or rather, of
|
||
diamond! We show that parallel reduction satisfies the diamond
|
||
property: that if <code class="language-plaintext highlighter-rouge">M ⇛ N</code> and <code class="language-plaintext highlighter-rouge">M ⇛ N′</code>, then <code class="language-plaintext highlighter-rouge">N ⇛ L</code> and <code class="language-plaintext highlighter-rouge">N′ ⇛ L</code> for
|
||
some <code class="language-plaintext highlighter-rouge">L</code>. The proof is relatively easy; it is parallel reduction’s
|
||
<em>raison d’etre</em>.</p>
|
||
|
||
<pre class="Agda"><a id="par-diamond"></a><a id="13016" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13028" class="Symbol">:</a> <a id="13030" class="Symbol">∀{</a><a id="13032" href="/20.07/Confluence/#13032" class="Bound">Γ</a> <a id="13034" href="/20.07/Confluence/#13034" class="Bound">A</a><a id="13035" class="Symbol">}</a> <a id="13037" class="Symbol">{</a><a id="13038" href="/20.07/Confluence/#13038" class="Bound">M</a> <a id="13040" href="/20.07/Confluence/#13040" class="Bound">N</a> <a id="13042" href="/20.07/Confluence/#13042" class="Bound">N′</a> <a id="13045" class="Symbol">:</a> <a id="13047" href="/20.07/Confluence/#13032" class="Bound">Γ</a> <a id="13049" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="13051" href="/20.07/Confluence/#13034" class="Bound">A</a><a id="13052" class="Symbol">}</a>
|
||
<a id="13056" class="Symbol">→</a> <a id="13058" href="/20.07/Confluence/#13038" class="Bound">M</a> <a id="13060" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="13062" href="/20.07/Confluence/#13040" class="Bound">N</a>
|
||
<a id="13066" class="Symbol">→</a> <a id="13068" href="/20.07/Confluence/#13038" class="Bound">M</a> <a id="13070" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="13072" href="/20.07/Confluence/#13042" class="Bound">N′</a>
|
||
<a id="13079" class="Comment">---------------------------------</a>
|
||
<a id="13115" class="Symbol">→</a> <a id="13117" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="13120" href="/20.07/Confluence/#13120" class="Bound">L</a> <a id="13122" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="13124" href="/20.07/Confluence/#13032" class="Bound">Γ</a> <a id="13126" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="13128" href="/20.07/Confluence/#13034" class="Bound">A</a> <a id="13130" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="13132" class="Symbol">(</a><a id="13133" href="/20.07/Confluence/#13040" class="Bound">N</a> <a id="13135" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="13137" href="/20.07/Confluence/#13120" class="Bound">L</a><a id="13138" class="Symbol">)</a> <a id="13140" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="13142" class="Symbol">(</a><a id="13143" href="/20.07/Confluence/#13042" class="Bound">N′</a> <a id="13146" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="13148" href="/20.07/Confluence/#13120" class="Bound">L</a><a id="13149" class="Symbol">)</a>
|
||
<a id="13151" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13163" class="Symbol">(</a><a id="13164" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a><a id="13168" class="Symbol">{</a><a id="13169" class="Argument">x</a> <a id="13171" class="Symbol">=</a> <a id="13173" href="/20.07/Confluence/#13173" class="Bound">x</a><a id="13174" class="Symbol">})</a> <a id="13177" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a> <a id="13182" class="Symbol">=</a> <a id="13184" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13186" href="/20.07/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="13188" href="/20.07/Confluence/#13173" class="Bound">x</a> <a id="13190" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13192" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13194" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a> <a id="13199" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13201" href="/20.07/Confluence/#2703" class="InductiveConstructor">pvar</a> <a id="13206" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13208" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="13210" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13222" class="Symbol">(</a><a id="13223" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="13228" href="/20.07/Confluence/#13228" class="Bound">p1</a><a id="13230" class="Symbol">)</a> <a id="13232" class="Symbol">(</a><a id="13233" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="13238" href="/20.07/Confluence/#13238" class="Bound">p2</a><a id="13240" class="Symbol">)</a>
|
||
<a id="13246" class="Keyword">with</a> <a id="13251" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13263" href="/20.07/Confluence/#13228" class="Bound">p1</a> <a id="13266" href="/20.07/Confluence/#13238" class="Bound">p2</a>
|
||
<a id="13269" class="Symbol">...</a> <a id="13273" class="Symbol">|</a> <a id="13275" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13277" href="/20.07/Confluence/#13277" class="Bound">L′</a> <a id="13280" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13282" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13284" href="/20.07/Confluence/#13284" class="Bound">p3</a> <a id="13287" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13289" href="/20.07/Confluence/#13289" class="Bound">p4</a> <a id="13292" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13294" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13296" class="Symbol">=</a>
|
||
<a id="13304" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13306" href="/20.07/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="13308" href="/20.07/Confluence/#13277" class="Bound">L′</a> <a id="13311" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13313" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13315" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="13320" href="/20.07/Confluence/#13284" class="Bound">p3</a> <a id="13323" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13325" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="13330" href="/20.07/Confluence/#13289" class="Bound">p4</a> <a id="13333" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13335" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="13337" href="/20.07/Confluence/#13016" class="Function">par-diamond</a><a id="13348" class="Symbol">{</a><a id="13349" href="/20.07/Confluence/#13349" class="Bound">Γ</a><a id="13350" class="Symbol">}{</a><a id="13352" href="/20.07/Confluence/#13352" class="Bound">A</a><a id="13353" class="Symbol">}{</a><a id="13355" href="/20.07/Confluence/#13355" class="Bound">L</a> <a id="13357" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="13359" href="/20.07/Confluence/#13359" class="Bound">M</a><a id="13360" class="Symbol">}{</a><a id="13362" href="/20.07/Confluence/#13362" class="Bound">N</a><a id="13363" class="Symbol">}{</a><a id="13365" href="/20.07/Confluence/#13365" class="Bound">N′</a><a id="13367" class="Symbol">}</a> <a id="13369" class="Symbol">(</a><a id="13370" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a><a id="13374" class="Symbol">{</a><a id="13375" href="/20.07/Confluence/#13349" class="Bound">Γ</a><a id="13376" class="Symbol">}{</a><a id="13378" href="/20.07/Confluence/#13355" class="Bound">L</a><a id="13379" class="Symbol">}{</a><a id="13381" href="/20.07/Confluence/#13381" class="Bound">L₁</a><a id="13383" class="Symbol">}{</a><a id="13385" href="/20.07/Confluence/#13359" class="Bound">M</a><a id="13386" class="Symbol">}{</a><a id="13388" href="/20.07/Confluence/#13388" class="Bound">M₁</a><a id="13390" class="Symbol">}</a> <a id="13392" href="/20.07/Confluence/#13392" class="Bound">p1</a> <a id="13395" href="/20.07/Confluence/#13395" class="Bound">p3</a><a id="13397" class="Symbol">)</a>
|
||
<a id="13431" class="Symbol">(</a><a id="13432" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a><a id="13436" class="Symbol">{</a><a id="13437" href="/20.07/Confluence/#13349" class="Bound">Γ</a><a id="13438" class="Symbol">}{</a><a id="13440" href="/20.07/Confluence/#13355" class="Bound">L</a><a id="13441" class="Symbol">}{</a><a id="13443" href="/20.07/Confluence/#13443" class="Bound">L₂</a><a id="13445" class="Symbol">}{</a><a id="13447" href="/20.07/Confluence/#13359" class="Bound">M</a><a id="13448" class="Symbol">}{</a><a id="13450" href="/20.07/Confluence/#13450" class="Bound">M₂</a><a id="13452" class="Symbol">}</a> <a id="13454" href="/20.07/Confluence/#13454" class="Bound">p2</a> <a id="13457" href="/20.07/Confluence/#13457" class="Bound">p4</a><a id="13459" class="Symbol">)</a>
|
||
<a id="13465" class="Keyword">with</a> <a id="13470" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13482" href="/20.07/Confluence/#13392" class="Bound">p1</a> <a id="13485" href="/20.07/Confluence/#13454" class="Bound">p2</a>
|
||
<a id="13488" class="Symbol">...</a> <a id="13492" class="Symbol">|</a> <a id="13494" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13496" href="/20.07/Confluence/#13496" class="Bound">L₃</a> <a id="13499" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13501" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13503" href="/20.07/Confluence/#13503" class="Bound">p5</a> <a id="13506" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13508" href="/20.07/Confluence/#13508" class="Bound">p6</a> <a id="13511" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13513" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="13521" class="Keyword">with</a> <a id="13526" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13538" class="Bound">p3</a> <a id="13541" class="Bound">p4</a>
|
||
<a id="13544" class="Symbol">...</a> <a id="13550" class="Symbol">|</a> <a id="13552" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13554" href="/20.07/Confluence/#13554" class="Bound">M₃</a> <a id="13557" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13559" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13561" href="/20.07/Confluence/#13561" class="Bound">p7</a> <a id="13564" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13566" href="/20.07/Confluence/#13566" class="Bound">p8</a> <a id="13569" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13571" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13573" class="Symbol">=</a>
|
||
<a id="13583" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13585" class="Symbol">(</a><a id="13586" class="Bound">L₃</a> <a id="13589" href="/20.07/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="13591" href="/20.07/Confluence/#13554" class="Bound">M₃</a><a id="13593" class="Symbol">)</a> <a id="13595" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13597" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13599" class="Symbol">(</a><a id="13600" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="13605" class="Bound">p5</a> <a id="13608" href="/20.07/Confluence/#13561" class="Bound">p7</a><a id="13610" class="Symbol">)</a> <a id="13612" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13614" class="Symbol">(</a><a id="13615" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="13620" class="Bound">p6</a> <a id="13623" href="/20.07/Confluence/#13566" class="Bound">p8</a><a id="13625" class="Symbol">)</a> <a id="13627" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13629" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="13631" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13643" class="Symbol">(</a><a id="13644" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="13649" class="Symbol">(</a><a id="13650" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="13655" href="/20.07/Confluence/#13655" class="Bound">p1</a><a id="13657" class="Symbol">)</a> <a id="13659" href="/20.07/Confluence/#13659" class="Bound">p3</a><a id="13661" class="Symbol">)</a> <a id="13663" class="Symbol">(</a><a id="13664" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="13670" href="/20.07/Confluence/#13670" class="Bound">p2</a> <a id="13673" href="/20.07/Confluence/#13673" class="Bound">p4</a><a id="13675" class="Symbol">)</a>
|
||
<a id="13681" class="Keyword">with</a> <a id="13686" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13698" href="/20.07/Confluence/#13655" class="Bound">p1</a> <a id="13701" href="/20.07/Confluence/#13670" class="Bound">p2</a>
|
||
<a id="13704" class="Symbol">...</a> <a id="13708" class="Symbol">|</a> <a id="13710" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13712" href="/20.07/Confluence/#13712" class="Bound">N₃</a> <a id="13715" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13717" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13719" href="/20.07/Confluence/#13719" class="Bound">p5</a> <a id="13722" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13724" href="/20.07/Confluence/#13724" class="Bound">p6</a> <a id="13727" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13729" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="13737" class="Keyword">with</a> <a id="13742" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13754" class="Bound">p3</a> <a id="13757" class="Bound">p4</a>
|
||
<a id="13760" class="Symbol">...</a> <a id="13766" class="Symbol">|</a> <a id="13768" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13770" href="/20.07/Confluence/#13770" class="Bound">M₃</a> <a id="13773" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13775" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13777" href="/20.07/Confluence/#13777" class="Bound">p7</a> <a id="13780" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13782" href="/20.07/Confluence/#13782" class="Bound">p8</a> <a id="13785" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13787" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13789" class="Symbol">=</a>
|
||
<a id="13799" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13801" class="Bound">N₃</a> <a id="13804" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="13806" href="/20.07/Confluence/#13770" class="Bound">M₃</a> <a id="13809" href="/20.07/Untyped/#7491" class="Function Operator">]</a> <a id="13811" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13813" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13815" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="13821" class="Bound">p5</a> <a id="13824" href="/20.07/Confluence/#13777" class="Bound">p7</a> <a id="13827" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13829" href="/20.07/Confluence/#12487" class="Function">sub-par</a> <a id="13837" class="Bound">p6</a> <a id="13840" href="/20.07/Confluence/#13782" class="Bound">p8</a> <a id="13843" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13845" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="13847" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13859" class="Symbol">(</a><a id="13860" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="13866" href="/20.07/Confluence/#13866" class="Bound">p1</a> <a id="13869" href="/20.07/Confluence/#13869" class="Bound">p3</a><a id="13871" class="Symbol">)</a> <a id="13873" class="Symbol">(</a><a id="13874" href="/20.07/Confluence/#2847" class="InductiveConstructor">papp</a> <a id="13879" class="Symbol">(</a><a id="13880" href="/20.07/Confluence/#2767" class="InductiveConstructor">pabs</a> <a id="13885" href="/20.07/Confluence/#13885" class="Bound">p2</a><a id="13887" class="Symbol">)</a> <a id="13889" href="/20.07/Confluence/#13889" class="Bound">p4</a><a id="13891" class="Symbol">)</a>
|
||
<a id="13897" class="Keyword">with</a> <a id="13902" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13914" href="/20.07/Confluence/#13866" class="Bound">p1</a> <a id="13917" href="/20.07/Confluence/#13885" class="Bound">p2</a>
|
||
<a id="13920" class="Symbol">...</a> <a id="13924" class="Symbol">|</a> <a id="13926" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13928" href="/20.07/Confluence/#13928" class="Bound">N₃</a> <a id="13931" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13933" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13935" href="/20.07/Confluence/#13935" class="Bound">p5</a> <a id="13938" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13940" href="/20.07/Confluence/#13940" class="Bound">p6</a> <a id="13943" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13945" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="13953" class="Keyword">with</a> <a id="13958" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="13970" class="Bound">p3</a> <a id="13973" class="Bound">p4</a>
|
||
<a id="13976" class="Symbol">...</a> <a id="13982" class="Symbol">|</a> <a id="13984" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13986" href="/20.07/Confluence/#13986" class="Bound">M₃</a> <a id="13989" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13991" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13993" href="/20.07/Confluence/#13993" class="Bound">p7</a> <a id="13996" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13998" href="/20.07/Confluence/#13998" class="Bound">p8</a> <a id="14001" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14003" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14005" class="Symbol">=</a>
|
||
<a id="14015" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14017" class="Symbol">(</a><a id="14018" class="Bound">N₃</a> <a id="14021" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="14023" href="/20.07/Confluence/#13986" class="Bound">M₃</a> <a id="14026" href="/20.07/Untyped/#7491" class="Function Operator">]</a><a id="14027" class="Symbol">)</a> <a id="14029" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14031" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14033" href="/20.07/Confluence/#12487" class="Function">sub-par</a> <a id="14041" class="Bound">p5</a> <a id="14045" href="/20.07/Confluence/#13993" class="Bound">p7</a> <a id="14048" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14050" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="14056" class="Bound">p6</a> <a id="14059" href="/20.07/Confluence/#13998" class="Bound">p8</a> <a id="14062" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14064" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="14066" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="14078" class="Symbol">{</a><a id="14079" href="/20.07/Confluence/#14079" class="Bound">Γ</a><a id="14080" class="Symbol">}{</a><a id="14082" href="/20.07/Confluence/#14082" class="Bound">A</a><a id="14083" class="Symbol">}</a> <a id="14085" class="Symbol">(</a><a id="14086" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="14092" href="/20.07/Confluence/#14092" class="Bound">p1</a> <a id="14095" href="/20.07/Confluence/#14095" class="Bound">p3</a><a id="14097" class="Symbol">)</a> <a id="14099" class="Symbol">(</a><a id="14100" href="/20.07/Confluence/#2953" class="InductiveConstructor">pbeta</a> <a id="14106" href="/20.07/Confluence/#14106" class="Bound">p2</a> <a id="14109" href="/20.07/Confluence/#14109" class="Bound">p4</a><a id="14111" class="Symbol">)</a>
|
||
<a id="14117" class="Keyword">with</a> <a id="14122" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="14134" href="/20.07/Confluence/#14092" class="Bound">p1</a> <a id="14137" href="/20.07/Confluence/#14106" class="Bound">p2</a>
|
||
<a id="14140" class="Symbol">...</a> <a id="14144" class="Symbol">|</a> <a id="14146" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14148" href="/20.07/Confluence/#14148" class="Bound">N₃</a> <a id="14151" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14153" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14155" href="/20.07/Confluence/#14155" class="Bound">p5</a> <a id="14158" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14160" href="/20.07/Confluence/#14160" class="Bound">p6</a> <a id="14163" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14165" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="14173" class="Keyword">with</a> <a id="14178" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="14190" class="Bound">p3</a> <a id="14193" class="Bound">p4</a>
|
||
<a id="14196" class="Symbol">...</a> <a id="14202" class="Symbol">|</a> <a id="14204" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14206" href="/20.07/Confluence/#14206" class="Bound">M₃</a> <a id="14209" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14211" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14213" href="/20.07/Confluence/#14213" class="Bound">p7</a> <a id="14216" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14218" href="/20.07/Confluence/#14218" class="Bound">p8</a> <a id="14221" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14223" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14225" class="Symbol">=</a>
|
||
<a id="14235" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14237" class="Bound">N₃</a> <a id="14240" href="/20.07/Untyped/#7491" class="Function Operator">[</a> <a id="14242" href="/20.07/Confluence/#14206" class="Bound">M₃</a> <a id="14245" href="/20.07/Untyped/#7491" class="Function Operator">]</a> <a id="14247" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14249" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14251" href="/20.07/Confluence/#12487" class="Function">sub-par</a> <a id="14259" class="Bound">p5</a> <a id="14262" href="/20.07/Confluence/#14213" class="Bound">p7</a> <a id="14265" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14267" href="/20.07/Confluence/#12487" class="Function">sub-par</a> <a id="14275" class="Bound">p6</a> <a id="14278" href="/20.07/Confluence/#14218" class="Bound">p8</a> <a id="14281" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14283" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
<p>The proof is by induction on both premises.</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">x ⇛ x</code> and <code class="language-plaintext highlighter-rouge">x ⇛ x</code>.
|
||
We choose <code class="language-plaintext highlighter-rouge">L = x</code> and immediately have <code class="language-plaintext highlighter-rouge">x ⇛ x</code> and <code class="language-plaintext highlighter-rouge">x ⇛ x</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose <code class="language-plaintext highlighter-rouge">ƛ N ⇛ ƛ N₁</code> and <code class="language-plaintext highlighter-rouge">ƛ N ⇛ ƛ N₂</code>.
|
||
By the induction hypothesis, there exists <code class="language-plaintext highlighter-rouge">L′</code> such that
|
||
<code class="language-plaintext highlighter-rouge">N₁ ⇛ L′</code> and <code class="language-plaintext highlighter-rouge">N₂ ⇛ L′</code>. We choose <code class="language-plaintext highlighter-rouge">L = ƛ L′</code> and
|
||
by <code class="language-plaintext highlighter-rouge">pabs</code> conclude that <code class="language-plaintext highlighter-rouge">ƛ N₁ ⇛ ƛ L′</code> and `ƛ N₂ ⇛ ƛ L′.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose that <code class="language-plaintext highlighter-rouge">L · M ⇛ L₁ · M₁</code> and <code class="language-plaintext highlighter-rouge">L · M ⇛ L₂ · M₂</code>.
|
||
By the induction hypothesis we have
|
||
<code class="language-plaintext highlighter-rouge">L₁ ⇛ L₃</code> and <code class="language-plaintext highlighter-rouge">L₂ ⇛ L₃</code> for some <code class="language-plaintext highlighter-rouge">L₃</code>.
|
||
Likewise, we have
|
||
<code class="language-plaintext highlighter-rouge">M₁ ⇛ M₃</code> and <code class="language-plaintext highlighter-rouge">M₂ ⇛ M₃</code> for some <code class="language-plaintext highlighter-rouge">M₃</code>.
|
||
We choose <code class="language-plaintext highlighter-rouge">L = L₃ · M₃</code> and conclude with two uses of <code class="language-plaintext highlighter-rouge">papp</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose that <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ (ƛ N₁) · M₁</code> and <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ N₂ [ M₂ ]</code>
|
||
By the induction hypothesis we have
|
||
<code class="language-plaintext highlighter-rouge">N₁ ⇛ N₃</code> and <code class="language-plaintext highlighter-rouge">N₂ ⇛ N₃</code> for some <code class="language-plaintext highlighter-rouge">N₃</code>.
|
||
Likewise, we have
|
||
<code class="language-plaintext highlighter-rouge">M₁ ⇛ M₃</code> and <code class="language-plaintext highlighter-rouge">M₂ ⇛ M₃</code> for some <code class="language-plaintext highlighter-rouge">M₃</code>.
|
||
We choose <code class="language-plaintext highlighter-rouge">L = N₃ [ M₃ ]</code>.
|
||
We have <code class="language-plaintext highlighter-rouge">(ƛ N₁) · M₁ ⇛ N₃ [ M₃ ]</code> by rule <code class="language-plaintext highlighter-rouge">pbeta</code>
|
||
and conclude that <code class="language-plaintext highlighter-rouge">N₂ [ M₂ ] ⇛ N₃ [ M₃ ]</code> because
|
||
substitution respects parallel reduction.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose that <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ N₁ [ M₁ ]</code> and <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ (ƛ N₂) · M₂</code>.
|
||
The proof of this case is the mirror image of the last one.</p>
|
||
</li>
|
||
<li>
|
||
<p>Suppose that <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ N₁ [ M₁ ]</code> and <code class="language-plaintext highlighter-rouge">(ƛ N) · M ⇛ N₂ [ M₂ ]</code>.
|
||
By the induction hypothesis we have
|
||
<code class="language-plaintext highlighter-rouge">N₁ ⇛ N₃</code> and <code class="language-plaintext highlighter-rouge">N₂ ⇛ N₃</code> for some <code class="language-plaintext highlighter-rouge">N₃</code>.
|
||
Likewise, we have
|
||
<code class="language-plaintext highlighter-rouge">M₁ ⇛ M₃</code> and <code class="language-plaintext highlighter-rouge">M₂ ⇛ M₃</code> for some <code class="language-plaintext highlighter-rouge">M₃</code>.
|
||
We choose <code class="language-plaintext highlighter-rouge">L = N₃ [ M₃ ]</code>.
|
||
We have both <code class="language-plaintext highlighter-rouge">(ƛ N₁) · M₁ ⇛ N₃ [ M₃ ]</code>
|
||
and <code class="language-plaintext highlighter-rouge">(ƛ N₂) · M₂ ⇛ N₃ [ M₃ ]</code>
|
||
by rule <code class="language-plaintext highlighter-rouge">pbeta</code></p>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="exercise-practice">Exercise (practice)</h4>
|
||
|
||
<p>Draw pictures that represent the proofs of each of the six cases in
|
||
the above proof of <code class="language-plaintext highlighter-rouge">par-diamond</code>. The pictures should consist of nodes
|
||
and directed edges, where each node is labeled with a term and each
|
||
edge represents parallel reduction.</p>
|
||
|
||
<h2 id="proof-of-confluence-for-parallel-reduction">Proof of confluence for parallel reduction</h2>
|
||
|
||
<p>As promised at the beginning, the proof that parallel reduction is
|
||
confluent is easy now that we know it satisfies the diamond property.
|
||
We just need to prove the strip lemma, which states that
|
||
if <code class="language-plaintext highlighter-rouge">M ⇛ N</code> and <code class="language-plaintext highlighter-rouge">M ⇛* N′</code>, then
|
||
<code class="language-plaintext highlighter-rouge">N ⇛* L</code> and <code class="language-plaintext highlighter-rouge">N′ ⇛ L</code> for some <code class="language-plaintext highlighter-rouge">L</code>.
|
||
The following diagram illustrates the strip lemma</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> M
|
||
/ \
|
||
1 *
|
||
/ \
|
||
N N′
|
||
\ /
|
||
* 1
|
||
\ /
|
||
L
|
||
</code></pre></div></div>
|
||
|
||
<p>where downward lines are instances of <code class="language-plaintext highlighter-rouge">⇛</code> or <code class="language-plaintext highlighter-rouge">⇛*</code>, depending on how
|
||
they are marked.</p>
|
||
|
||
<p>The proof of the strip lemma is a straightforward induction on <code class="language-plaintext highlighter-rouge">M ⇛* N′</code>,
|
||
using the diamond property in the induction step.</p>
|
||
|
||
<pre class="Agda"><a id="strip"></a><a id="16703" href="/20.07/Confluence/#16703" class="Function">strip</a> <a id="16709" class="Symbol">:</a> <a id="16711" class="Symbol">∀{</a><a id="16713" href="/20.07/Confluence/#16713" class="Bound">Γ</a> <a id="16715" href="/20.07/Confluence/#16715" class="Bound">A</a><a id="16716" class="Symbol">}</a> <a id="16718" class="Symbol">{</a><a id="16719" href="/20.07/Confluence/#16719" class="Bound">M</a> <a id="16721" href="/20.07/Confluence/#16721" class="Bound">N</a> <a id="16723" href="/20.07/Confluence/#16723" class="Bound">N′</a> <a id="16726" class="Symbol">:</a> <a id="16728" href="/20.07/Confluence/#16713" class="Bound">Γ</a> <a id="16730" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="16732" href="/20.07/Confluence/#16715" class="Bound">A</a><a id="16733" class="Symbol">}</a>
|
||
<a id="16737" class="Symbol">→</a> <a id="16739" href="/20.07/Confluence/#16719" class="Bound">M</a> <a id="16741" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="16743" href="/20.07/Confluence/#16721" class="Bound">N</a>
|
||
<a id="16747" class="Symbol">→</a> <a id="16749" href="/20.07/Confluence/#16719" class="Bound">M</a> <a id="16751" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="16754" href="/20.07/Confluence/#16723" class="Bound">N′</a>
|
||
<a id="16761" class="Comment">------------------------------------</a>
|
||
<a id="16800" class="Symbol">→</a> <a id="16802" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="16805" href="/20.07/Confluence/#16805" class="Bound">L</a> <a id="16807" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="16809" href="/20.07/Confluence/#16713" class="Bound">Γ</a> <a id="16811" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="16813" href="/20.07/Confluence/#16715" class="Bound">A</a> <a id="16815" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="16817" class="Symbol">(</a><a id="16818" href="/20.07/Confluence/#16721" class="Bound">N</a> <a id="16820" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="16823" href="/20.07/Confluence/#16805" class="Bound">L</a><a id="16824" class="Symbol">)</a> <a id="16827" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="16830" class="Symbol">(</a><a id="16831" href="/20.07/Confluence/#16723" class="Bound">N′</a> <a id="16834" href="/20.07/Confluence/#2654" class="Datatype Operator">⇛</a> <a id="16836" href="/20.07/Confluence/#16805" class="Bound">L</a><a id="16837" class="Symbol">)</a>
|
||
<a id="16839" href="/20.07/Confluence/#16703" class="Function">strip</a><a id="16844" class="Symbol">{</a><a id="16845" href="/20.07/Confluence/#16845" class="Bound">Γ</a><a id="16846" class="Symbol">}{</a><a id="16848" href="/20.07/Confluence/#16848" class="Bound">A</a><a id="16849" class="Symbol">}{</a><a id="16851" href="/20.07/Confluence/#16851" class="Bound">M</a><a id="16852" class="Symbol">}{</a><a id="16854" href="/20.07/Confluence/#16854" class="Bound">N</a><a id="16855" class="Symbol">}{</a><a id="16857" href="/20.07/Confluence/#16857" class="Bound">N′</a><a id="16859" class="Symbol">}</a> <a id="16861" href="/20.07/Confluence/#16861" class="Bound">mn</a> <a id="16864" class="Symbol">(</a><a id="16865" href="/20.07/Confluence/#16851" class="Bound">M</a> <a id="16867" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">∎</a><a id="16868" class="Symbol">)</a> <a id="16870" class="Symbol">=</a> <a id="16872" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16874" href="/20.07/Confluence/#16854" class="Bound">N</a> <a id="16876" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16878" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16880" href="/20.07/Confluence/#16854" class="Bound">N</a> <a id="16882" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">∎</a> <a id="16884" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16886" href="/20.07/Confluence/#16861" class="Bound">mn</a> <a id="16889" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16891" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="16893" href="/20.07/Confluence/#16703" class="Function">strip</a><a id="16898" class="Symbol">{</a><a id="16899" href="/20.07/Confluence/#16899" class="Bound">Γ</a><a id="16900" class="Symbol">}{</a><a id="16902" href="/20.07/Confluence/#16902" class="Bound">A</a><a id="16903" class="Symbol">}{</a><a id="16905" href="/20.07/Confluence/#16905" class="Bound">M</a><a id="16906" class="Symbol">}{</a><a id="16908" href="/20.07/Confluence/#16908" class="Bound">N</a><a id="16909" class="Symbol">}{</a><a id="16911" href="/20.07/Confluence/#16911" class="Bound">N′</a><a id="16913" class="Symbol">}</a> <a id="16915" href="/20.07/Confluence/#16915" class="Bound">mn</a> <a id="16918" class="Symbol">(</a><a id="16919" href="/20.07/Confluence/#16905" class="Bound">M</a> <a id="16921" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⇛⟨</a> <a id="16924" href="/20.07/Confluence/#16924" class="Bound">mm'</a> <a id="16928" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⟩</a> <a id="16930" href="/20.07/Confluence/#16930" class="Bound">m'n'</a><a id="16934" class="Symbol">)</a>
|
||
<a id="16940" class="Keyword">with</a> <a id="16945" href="/20.07/Confluence/#13016" class="Function">par-diamond</a> <a id="16957" href="/20.07/Confluence/#16915" class="Bound">mn</a> <a id="16960" href="/20.07/Confluence/#16924" class="Bound">mm'</a>
|
||
<a id="16964" class="Symbol">...</a> <a id="16968" class="Symbol">|</a> <a id="16970" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16972" href="/20.07/Confluence/#16972" class="Bound">L</a> <a id="16974" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16976" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16978" href="/20.07/Confluence/#16978" class="Bound">nl</a> <a id="16981" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16983" href="/20.07/Confluence/#16983" class="Bound">m'l</a> <a id="16987" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16989" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="16997" class="Keyword">with</a> <a id="17002" href="/20.07/Confluence/#16703" class="Function">strip</a> <a id="17008" href="/20.07/Confluence/#16983" class="Bound">m'l</a> <a id="17012" class="Bound">m'n'</a>
|
||
<a id="17017" class="Symbol">...</a> <a id="17023" class="Symbol">|</a> <a id="17025" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17027" href="/20.07/Confluence/#17027" class="Bound">L′</a> <a id="17030" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17032" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17034" href="/20.07/Confluence/#17034" class="Bound">ll'</a> <a id="17038" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17040" href="/20.07/Confluence/#17040" class="Bound">n'l'</a> <a id="17045" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17047" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17049" class="Symbol">=</a>
|
||
<a id="17059" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17061" href="/20.07/Confluence/#17027" class="Bound">L′</a> <a id="17064" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17066" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17068" class="Symbol">(</a><a id="17069" class="Bound">N</a> <a id="17071" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⇛⟨</a> <a id="17074" class="Bound">nl</a> <a id="17077" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⟩</a> <a id="17079" href="/20.07/Confluence/#17034" class="Bound">ll'</a><a id="17082" class="Symbol">)</a> <a id="17084" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17086" href="/20.07/Confluence/#17040" class="Bound">n'l'</a> <a id="17091" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17093" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
<p>The proof of confluence for parallel reduction is now proved by
|
||
induction on the sequence <code class="language-plaintext highlighter-rouge">M ⇛* N</code>, using the above lemma in the
|
||
induction step.</p>
|
||
|
||
<pre class="Agda"><a id="par-confluence"></a><a id="17250" href="/20.07/Confluence/#17250" class="Function">par-confluence</a> <a id="17265" class="Symbol">:</a> <a id="17267" class="Symbol">∀{</a><a id="17269" href="/20.07/Confluence/#17269" class="Bound">Γ</a> <a id="17271" href="/20.07/Confluence/#17271" class="Bound">A</a><a id="17272" class="Symbol">}</a> <a id="17274" class="Symbol">{</a><a id="17275" href="/20.07/Confluence/#17275" class="Bound">L</a> <a id="17277" href="/20.07/Confluence/#17277" class="Bound">M₁</a> <a id="17280" href="/20.07/Confluence/#17280" class="Bound">M₂</a> <a id="17283" class="Symbol">:</a> <a id="17285" href="/20.07/Confluence/#17269" class="Bound">Γ</a> <a id="17287" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="17289" href="/20.07/Confluence/#17271" class="Bound">A</a><a id="17290" class="Symbol">}</a>
|
||
<a id="17294" class="Symbol">→</a> <a id="17296" href="/20.07/Confluence/#17275" class="Bound">L</a> <a id="17298" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="17301" href="/20.07/Confluence/#17277" class="Bound">M₁</a>
|
||
<a id="17306" class="Symbol">→</a> <a id="17308" href="/20.07/Confluence/#17275" class="Bound">L</a> <a id="17310" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="17313" href="/20.07/Confluence/#17280" class="Bound">M₂</a>
|
||
<a id="17320" class="Comment">------------------------------------</a>
|
||
<a id="17359" class="Symbol">→</a> <a id="17361" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="17364" href="/20.07/Confluence/#17364" class="Bound">N</a> <a id="17366" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="17368" href="/20.07/Confluence/#17269" class="Bound">Γ</a> <a id="17370" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="17372" href="/20.07/Confluence/#17271" class="Bound">A</a> <a id="17374" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="17376" class="Symbol">(</a><a id="17377" href="/20.07/Confluence/#17277" class="Bound">M₁</a> <a id="17380" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="17383" href="/20.07/Confluence/#17364" class="Bound">N</a><a id="17384" class="Symbol">)</a> <a id="17386" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="17388" class="Symbol">(</a><a id="17389" href="/20.07/Confluence/#17280" class="Bound">M₂</a> <a id="17392" href="/20.07/Confluence/#3757" class="Datatype Operator">⇛*</a> <a id="17395" href="/20.07/Confluence/#17364" class="Bound">N</a><a id="17396" class="Symbol">)</a>
|
||
<a id="17398" href="/20.07/Confluence/#17250" class="Function">par-confluence</a> <a id="17413" class="Symbol">{</a><a id="17414" href="/20.07/Confluence/#17414" class="Bound">Γ</a><a id="17415" class="Symbol">}{</a><a id="17417" href="/20.07/Confluence/#17417" class="Bound">A</a><a id="17418" class="Symbol">}{</a><a id="17420" href="/20.07/Confluence/#17420" class="Bound">L</a><a id="17421" class="Symbol">}{</a><a id="17423" class="DottedPattern Symbol">.</a><a id="17424" href="/20.07/Confluence/#17420" class="DottedPattern Bound">L</a><a id="17425" class="Symbol">}{</a><a id="17427" href="/20.07/Confluence/#17427" class="Bound">N</a><a id="17428" class="Symbol">}</a> <a id="17430" class="Symbol">(</a><a id="17431" href="/20.07/Confluence/#17420" class="Bound">L</a> <a id="17433" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">∎</a><a id="17434" class="Symbol">)</a> <a id="17436" href="/20.07/Confluence/#17436" class="Bound">L⇛*N</a> <a id="17441" class="Symbol">=</a> <a id="17443" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17445" href="/20.07/Confluence/#17427" class="Bound">N</a> <a id="17447" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17449" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17451" href="/20.07/Confluence/#17436" class="Bound">L⇛*N</a> <a id="17456" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17458" href="/20.07/Confluence/#17427" class="Bound">N</a> <a id="17460" href="/20.07/Confluence/#3807" class="InductiveConstructor Operator">∎</a> <a id="17462" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17464" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="17466" href="/20.07/Confluence/#17250" class="Function">par-confluence</a> <a id="17481" class="Symbol">{</a><a id="17482" href="/20.07/Confluence/#17482" class="Bound">Γ</a><a id="17483" class="Symbol">}{</a><a id="17485" href="/20.07/Confluence/#17485" class="Bound">A</a><a id="17486" class="Symbol">}{</a><a id="17488" href="/20.07/Confluence/#17488" class="Bound">L</a><a id="17489" class="Symbol">}{</a><a id="17491" href="/20.07/Confluence/#17491" class="Bound">M₁′</a><a id="17494" class="Symbol">}{</a><a id="17496" href="/20.07/Confluence/#17496" class="Bound">M₂</a><a id="17498" class="Symbol">}</a> <a id="17500" class="Symbol">(</a><a id="17501" href="/20.07/Confluence/#17488" class="Bound">L</a> <a id="17503" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⇛⟨</a> <a id="17506" href="/20.07/Confluence/#17506" class="Bound">L⇛M₁</a> <a id="17511" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⟩</a> <a id="17513" href="/20.07/Confluence/#17513" class="Bound">M₁⇛*M₁′</a><a id="17520" class="Symbol">)</a> <a id="17522" href="/20.07/Confluence/#17522" class="Bound">L⇛*M₂</a>
|
||
<a id="17532" class="Keyword">with</a> <a id="17537" href="/20.07/Confluence/#16703" class="Function">strip</a> <a id="17543" href="/20.07/Confluence/#17506" class="Bound">L⇛M₁</a> <a id="17548" href="/20.07/Confluence/#17522" class="Bound">L⇛*M₂</a>
|
||
<a id="17554" class="Symbol">...</a> <a id="17558" class="Symbol">|</a> <a id="17560" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17562" href="/20.07/Confluence/#17562" class="Bound">N</a> <a id="17564" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17566" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17568" href="/20.07/Confluence/#17568" class="Bound">M₁⇛*N</a> <a id="17574" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17576" href="/20.07/Confluence/#17576" class="Bound">M₂⇛N</a> <a id="17581" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17583" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
<a id="17591" class="Keyword">with</a> <a id="17596" href="/20.07/Confluence/#17250" class="Function">par-confluence</a> <a id="17611" class="Bound">M₁⇛*M₁′</a> <a id="17619" href="/20.07/Confluence/#17568" class="Bound">M₁⇛*N</a>
|
||
<a id="17625" class="Symbol">...</a> <a id="17631" class="Symbol">|</a> <a id="17633" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17635" href="/20.07/Confluence/#17635" class="Bound">N′</a> <a id="17638" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17640" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17642" href="/20.07/Confluence/#17642" class="Bound">M₁′⇛*N′</a> <a id="17650" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17652" href="/20.07/Confluence/#17652" class="Bound">N⇛*N′</a> <a id="17658" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17660" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17662" class="Symbol">=</a>
|
||
<a id="17672" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17674" href="/20.07/Confluence/#17635" class="Bound">N′</a> <a id="17677" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17679" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17681" href="/20.07/Confluence/#17642" class="Bound">M₁′⇛*N′</a> <a id="17689" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17691" class="Symbol">(</a><a id="17692" class="Bound">M₂</a> <a id="17695" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⇛⟨</a> <a id="17698" class="Bound">M₂⇛N</a> <a id="17703" href="/20.07/Confluence/#3863" class="InductiveConstructor Operator">⟩</a> <a id="17705" href="/20.07/Confluence/#17652" class="Bound">N⇛*N′</a><a id="17710" class="Symbol">)</a> <a id="17712" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17714" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
<p>The step case may be illustrated as follows:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> L
|
||
/ \
|
||
1 *
|
||
/ \
|
||
M₁ (a) M₂
|
||
/ \ /
|
||
* * 1
|
||
/ \ /
|
||
M₁′(b) N
|
||
\ /
|
||
* *
|
||
\ /
|
||
N′
|
||
</code></pre></div></div>
|
||
|
||
<p>where downward lines are instances of <code class="language-plaintext highlighter-rouge">⇛</code> or <code class="language-plaintext highlighter-rouge">⇛*</code>, depending on how
|
||
they are marked. Here <code class="language-plaintext highlighter-rouge">(a)</code> holds by <code class="language-plaintext highlighter-rouge">strip</code> and <code class="language-plaintext highlighter-rouge">(b)</code> holds by
|
||
induction.</p>
|
||
|
||
<h2 id="proof-of-confluence-for-reduction">Proof of confluence for reduction</h2>
|
||
|
||
<p>Confluence of reduction is a corollary of confluence for parallel
|
||
reduction. From
|
||
<code class="language-plaintext highlighter-rouge">L —↠ M₁</code> and <code class="language-plaintext highlighter-rouge">L —↠ M₂</code> we have
|
||
<code class="language-plaintext highlighter-rouge">L ⇛* M₁</code> and <code class="language-plaintext highlighter-rouge">L ⇛* M₂</code> by <code class="language-plaintext highlighter-rouge">betas-pars</code>.
|
||
Then by confluence we obtain some <code class="language-plaintext highlighter-rouge">L</code> such that
|
||
<code class="language-plaintext highlighter-rouge">M₁ ⇛* N</code> and <code class="language-plaintext highlighter-rouge">M₂ ⇛* N</code>, from which we conclude that
|
||
<code class="language-plaintext highlighter-rouge">M₁ —↠ N</code> and <code class="language-plaintext highlighter-rouge">M₂ —↠ N</code> by <code class="language-plaintext highlighter-rouge">pars-betas</code>.</p>
|
||
|
||
<pre class="Agda"><a id="confluence"></a><a id="18443" href="/20.07/Confluence/#18443" class="Function">confluence</a> <a id="18454" class="Symbol">:</a> <a id="18456" class="Symbol">∀{</a><a id="18458" href="/20.07/Confluence/#18458" class="Bound">Γ</a> <a id="18460" href="/20.07/Confluence/#18460" class="Bound">A</a><a id="18461" class="Symbol">}</a> <a id="18463" class="Symbol">{</a><a id="18464" href="/20.07/Confluence/#18464" class="Bound">L</a> <a id="18466" href="/20.07/Confluence/#18466" class="Bound">M₁</a> <a id="18469" href="/20.07/Confluence/#18469" class="Bound">M₂</a> <a id="18472" class="Symbol">:</a> <a id="18474" href="/20.07/Confluence/#18458" class="Bound">Γ</a> <a id="18476" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="18478" href="/20.07/Confluence/#18460" class="Bound">A</a><a id="18479" class="Symbol">}</a>
|
||
<a id="18483" class="Symbol">→</a> <a id="18485" href="/20.07/Confluence/#18464" class="Bound">L</a> <a id="18487" href="/20.07/Untyped/#11068" class="Datatype Operator">—↠</a> <a id="18490" href="/20.07/Confluence/#18466" class="Bound">M₁</a>
|
||
<a id="18495" class="Symbol">→</a> <a id="18497" href="/20.07/Confluence/#18464" class="Bound">L</a> <a id="18499" href="/20.07/Untyped/#11068" class="Datatype Operator">—↠</a> <a id="18502" href="/20.07/Confluence/#18469" class="Bound">M₂</a>
|
||
<a id="18509" class="Comment">-----------------------------------</a>
|
||
<a id="18547" class="Symbol">→</a> <a id="18549" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="18552" href="/20.07/Confluence/#18552" class="Bound">N</a> <a id="18554" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="18556" href="/20.07/Confluence/#18458" class="Bound">Γ</a> <a id="18558" href="/20.07/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="18560" href="/20.07/Confluence/#18460" class="Bound">A</a> <a id="18562" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="18564" class="Symbol">(</a><a id="18565" href="/20.07/Confluence/#18466" class="Bound">M₁</a> <a id="18568" href="/20.07/Untyped/#11068" class="Datatype Operator">—↠</a> <a id="18571" href="/20.07/Confluence/#18552" class="Bound">N</a><a id="18572" class="Symbol">)</a> <a id="18574" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="18576" class="Symbol">(</a><a id="18577" href="/20.07/Confluence/#18469" class="Bound">M₂</a> <a id="18580" href="/20.07/Untyped/#11068" class="Datatype Operator">—↠</a> <a id="18583" href="/20.07/Confluence/#18552" class="Bound">N</a><a id="18584" class="Symbol">)</a>
|
||
<a id="18586" href="/20.07/Confluence/#18443" class="Function">confluence</a> <a id="18597" href="/20.07/Confluence/#18597" class="Bound">L↠M₁</a> <a id="18602" href="/20.07/Confluence/#18602" class="Bound">L↠M₂</a>
|
||
<a id="18611" class="Keyword">with</a> <a id="18616" href="/20.07/Confluence/#17250" class="Function">par-confluence</a> <a id="18631" class="Symbol">(</a><a id="18632" href="/20.07/Confluence/#4959" class="Function">betas-pars</a> <a id="18643" href="/20.07/Confluence/#18597" class="Bound">L↠M₁</a><a id="18647" class="Symbol">)</a> <a id="18649" class="Symbol">(</a><a id="18650" href="/20.07/Confluence/#4959" class="Function">betas-pars</a> <a id="18661" href="/20.07/Confluence/#18602" class="Bound">L↠M₂</a><a id="18665" class="Symbol">)</a>
|
||
<a id="18667" class="Symbol">...</a> <a id="18671" class="Symbol">|</a> <a id="18673" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18675" href="/20.07/Confluence/#18675" class="Bound">N</a> <a id="18677" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18679" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18681" href="/20.07/Confluence/#18681" class="Bound">M₁⇛N</a> <a id="18686" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18688" href="/20.07/Confluence/#18688" class="Bound">M₂⇛N</a> <a id="18693" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18695" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18697" class="Symbol">=</a>
|
||
<a id="18705" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18707" href="/20.07/Confluence/#18675" class="Bound">N</a> <a id="18709" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18711" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18713" href="/20.07/Confluence/#6858" class="Function">pars-betas</a> <a id="18724" href="/20.07/Confluence/#18681" class="Bound">M₁⇛N</a> <a id="18729" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18731" href="/20.07/Confluence/#6858" class="Function">pars-betas</a> <a id="18742" href="/20.07/Confluence/#18688" class="Bound">M₂⇛N</a> <a id="18747" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18749" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
|
||
</pre>
|
||
|
||
<h2 id="notes">Notes</h2>
|
||
|
||
<p>Broadly speaking, this proof of confluence, based on parallel
|
||
reduction, is due to W. Tait and P. Martin-Lof (see Barendredgt 1984,
|
||
Section 3.2). Details of the mechanization come from several sources.
|
||
The <code class="language-plaintext highlighter-rouge">subst-par</code> lemma is the “strong substitutivity” lemma of Shafer,
|
||
Tebbi, and Smolka (ITP 2015). The proofs of <code class="language-plaintext highlighter-rouge">par-diamond</code>, <code class="language-plaintext highlighter-rouge">strip</code>,
|
||
and <code class="language-plaintext highlighter-rouge">par-confluence</code> are based on Pfenning’s 1992 technical report
|
||
about the Church-Rosser theorem. In addition, we consulted Nipkow and
|
||
Berghofer’s mechanization in Isabelle, which is based on an earlier
|
||
article by Nipkow (JAR 1996). We opted not to use the “complete
|
||
developments” approach of Takahashi (1995) because we felt that the
|
||
proof was simple enough based solely on parallel reduction. There are
|
||
many more mechanizations of the Church-Rosser theorem that we have not
|
||
yet had the time to read, including Shankar’s (J. ACM 1988) and
|
||
Homeier’s (TPHOLs 2001).</p>
|
||
|
||
<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+3015 RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)
|
||
</code></pre></div></div>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Untyped/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part2/Confluence.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/BigStep/">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>
|