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

822 lines
175 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

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

<!DOCTYPE html>
<html lang="en"><head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>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/19.08/Confluence/" />
<meta property="og:url" content="https://plfa.github.io/19.08/Confluence/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/19.08/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="/19.08/assets/main.css"></head>
<body><header class="site-header" role="banner">
<div class="wrapper">
<a class="site-title" href="/19.08/">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="/19.08/">The Book</a>
<a class="page-link" href="/19.08/Announcements/">Announcements</a>
<a class="page-link" href="/19.08/GettingStarted/">Getting Started</a>
<a class="page-link" href="/19.08/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="/19.08/Untyped/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part2/Confluence.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/BigStep/">Next</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="166" class="Keyword">module</a> <a id="173" href="/19.08/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="/19.08/Substitution/" class="Module">plfa.part2.Substitution</a> <a id="2296" class="Keyword">using</a> <a id="2302" class="Symbol">(</a><a id="2303" href="plfa.part2.Substitution.html#2192" class="Function">Rename</a><a id="2309" class="Symbol">;</a> <a id="2311" href="plfa.part2.Substitution.html#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="/19.08/Untyped/" class="Module">plfa.part2.Untyped</a>
<a id="2351" class="Keyword">using</a> <a id="2357" class="Symbol">(</a><a id="2358" href="/19.08/Untyped/#10147" class="Datatype Operator">_—→_</a><a id="2362" class="Symbol">;</a> <a id="2364" href="plfa.part2.Untyped.html#10377" class="InductiveConstructor">β</a><a id="2365" class="Symbol">;</a> <a id="2367" href="plfa.part2.Untyped.html#10197" class="InductiveConstructor">ξ₁</a><a id="2369" class="Symbol">;</a> <a id="2371" href="plfa.part2.Untyped.html#10287" class="InductiveConstructor">ξ₂</a><a id="2373" class="Symbol">;</a> <a id="2375" href="plfa.part2.Untyped.html#10485" class="InductiveConstructor">ζ</a><a id="2376" class="Symbol">;</a> <a id="2378" href="plfa.part2.Untyped.html#11267" class="Datatype Operator">_—↠_</a><a id="2382" class="Symbol">;</a> <a id="2384" href="plfa.part2.Untyped.html#11373" class="InductiveConstructor Operator">_—→⟨_⟩_</a><a id="2391" class="Symbol">;</a> <a id="2393" href="plfa.part2.Untyped.html#11317" class="InductiveConstructor Operator">_∎</a><a id="2395" class="Symbol">;</a>
<a id="2399" href="/19.08/Untyped/#23800" class="Function">abs-cong</a><a id="2407" class="Symbol">;</a> <a id="2409" href="plfa.part2.Untyped.html#22803" class="Function">appL-cong</a><a id="2418" class="Symbol">;</a> <a id="2420" href="plfa.part2.Untyped.html#23572" class="Function">appR-cong</a><a id="2429" class="Symbol">;</a> <a id="2431" href="plfa.part2.Untyped.html#21619" class="Function">—↠-trans</a><a id="2439" class="Symbol">;</a>
<a id="2443" href="/19.08/Untyped/#4294" class="Datatype Operator">_⊢_</a><a id="2446" class="Symbol">;</a> <a id="2448" href="plfa.part2.Untyped.html#3521" class="Datatype Operator">_∋_</a><a id="2451" class="Symbol">;</a> <a id="2453" href="plfa.part2.Untyped.html#4330" class="InductiveConstructor Operator">`_</a><a id="2455" class="Symbol">;</a> <a id="2457" href="plfa.part2.Untyped.html#5111" class="Function Operator">#_</a><a id="2459" class="Symbol">;</a> <a id="2461" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">_,_</a><a id="2464" class="Symbol">;</a> <a id="2466" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="2467" class="Symbol">;</a> <a id="2469" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ_</a><a id="2471" class="Symbol">;</a> <a id="2473" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">_·_</a><a id="2476" class="Symbol">;</a> <a id="2478" href="plfa.part2.Untyped.html#7491" class="Function Operator">_[_]</a><a id="2482" class="Symbol">;</a>
<a id="2486" href="/19.08/Untyped/#6235" class="Function">rename</a><a id="2492" class="Symbol">;</a> <a id="2494" href="plfa.part2.Untyped.html#5925" class="Function">ext</a><a id="2497" class="Symbol">;</a> <a id="2499" href="plfa.part2.Untyped.html#6671" class="Function">exts</a><a id="2503" class="Symbol">;</a> <a id="2505" href="plfa.part2.Untyped.html#3557" class="InductiveConstructor">Z</a><a id="2506" class="Symbol">;</a> <a id="2508" href="plfa.part2.Untyped.html#3602" class="InductiveConstructor Operator">S_</a><a id="2510" class="Symbol">;</a> <a id="2512" href="plfa.part2.Untyped.html#6963" class="Function">subst</a><a id="2517" class="Symbol">;</a> <a id="2519" href="plfa.part2.Untyped.html#7375" class="Function">subst-zero</a><a id="2529" 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="2619" class="Keyword">infix</a> <a id="2625" class="Number">2</a> <a id="2627" href="/19.08/Confluence/#2637" class="Datatype Operator">_⇛_</a>
<a id="2632" class="Keyword">data</a> <a id="_⇛_"></a><a id="2637" href="/19.08/Confluence/#2637" class="Datatype Operator">_⇛_</a> <a id="2641" class="Symbol">:</a> <a id="2643" class="Symbol">∀</a> <a id="2645" class="Symbol">{</a><a id="2646" href="plfa.part2.Confluence.html#2646" class="Bound">Γ</a> <a id="2648" href="plfa.part2.Confluence.html#2648" class="Bound">A</a><a id="2649" class="Symbol">}</a> <a id="2651" class="Symbol">→</a> <a id="2653" class="Symbol">(</a><a id="2654" href="plfa.part2.Confluence.html#2646" class="Bound">Γ</a> <a id="2656" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2658" href="plfa.part2.Confluence.html#2648" class="Bound">A</a><a id="2659" class="Symbol">)</a> <a id="2661" class="Symbol">→</a> <a id="2663" class="Symbol">(</a><a id="2664" href="plfa.part2.Confluence.html#2646" class="Bound">Γ</a> <a id="2666" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="2668" href="plfa.part2.Confluence.html#2648" class="Bound">A</a><a id="2669" class="Symbol">)</a> <a id="2671" class="Symbol">→</a> <a id="2673" class="PrimitiveType">Set</a> <a id="2677" class="Keyword">where</a>
<a id="_⇛_.pvar"></a><a id="2686" href="/19.08/Confluence/#2686" class="InductiveConstructor">pvar</a> <a id="2691" class="Symbol">:</a> <a id="2693" class="Symbol">∀{</a><a id="2695" href="plfa.part2.Confluence.html#2695" class="Bound">Γ</a> <a id="2697" href="plfa.part2.Confluence.html#2697" class="Bound">A</a><a id="2698" class="Symbol">}{</a><a id="2700" href="plfa.part2.Confluence.html#2700" class="Bound">x</a> <a id="2702" class="Symbol">:</a> <a id="2704" href="plfa.part2.Confluence.html#2695" class="Bound">Γ</a> <a id="2706" href="/19.08/Untyped/#3521" class="Datatype Operator">∋</a> <a id="2708" href="plfa.part2.Confluence.html#2697" class="Bound">A</a><a id="2709" class="Symbol">}</a>
<a id="2717" class="Comment">---------</a>
<a id="2731" class="Symbol">→</a> <a id="2733" class="Symbol">(</a><a id="2734" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="2736" href="/19.08/Confluence/#2700" class="Bound">x</a><a id="2737" class="Symbol">)</a> <a id="2739" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="2741" class="Symbol">(</a><a id="2742" href="plfa.part2.Untyped.html#4330" class="InductiveConstructor Operator">`</a> <a id="2744" href="plfa.part2.Confluence.html#2700" class="Bound">x</a><a id="2745" class="Symbol">)</a>
<a id="_⇛_.pabs"></a><a id="2750" href="/19.08/Confluence/#2750" class="InductiveConstructor">pabs</a> <a id="2755" class="Symbol">:</a> <a id="2757" class="Symbol">∀{</a><a id="2759" href="plfa.part2.Confluence.html#2759" class="Bound">Γ</a><a id="2760" class="Symbol">}{</a><a id="2762" href="plfa.part2.Confluence.html#2762" class="Bound">N</a> <a id="2764" href="plfa.part2.Confluence.html#2764" class="Bound">N′</a> <a id="2767" class="Symbol">:</a> <a id="2769" href="plfa.part2.Confluence.html#2759" class="Bound">Γ</a> <a id="2771" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="2773" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="2775" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="2777" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="2778" class="Symbol">}</a>
<a id="2784" class="Symbol">→</a> <a id="2786" href="/19.08/Confluence/#2762" class="Bound">N</a> <a id="2788" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="2790" href="plfa.part2.Confluence.html#2764" class="Bound">N′</a>
<a id="2799" class="Comment">----------</a>
<a id="2814" class="Symbol">→</a> <a id="2816" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="2818" href="/19.08/Confluence/#2762" class="Bound">N</a> <a id="2820" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="2822" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="2824" href="plfa.part2.Confluence.html#2764" class="Bound">N′</a>
<a id="_⇛_.papp"></a><a id="2830" href="/19.08/Confluence/#2830" class="InductiveConstructor">papp</a> <a id="2835" class="Symbol">:</a> <a id="2837" class="Symbol">∀{</a><a id="2839" href="plfa.part2.Confluence.html#2839" class="Bound">Γ</a><a id="2840" class="Symbol">}{</a><a id="2842" href="plfa.part2.Confluence.html#2842" class="Bound">L</a> <a id="2844" href="plfa.part2.Confluence.html#2844" class="Bound">L′</a> <a id="2847" href="plfa.part2.Confluence.html#2847" class="Bound">M</a> <a id="2849" href="plfa.part2.Confluence.html#2849" class="Bound">M′</a> <a id="2852" class="Symbol">:</a> <a id="2854" href="plfa.part2.Confluence.html#2839" class="Bound">Γ</a> <a id="2856" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="2858" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="2859" class="Symbol">}</a>
<a id="2865" class="Symbol">→</a> <a id="2867" href="/19.08/Confluence/#2842" class="Bound">L</a> <a id="2869" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="2871" href="plfa.part2.Confluence.html#2844" class="Bound">L′</a>
<a id="2878" class="Symbol">→</a> <a id="2880" href="/19.08/Confluence/#2847" class="Bound">M</a> <a id="2882" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="2884" href="plfa.part2.Confluence.html#2849" class="Bound">M′</a>
<a id="2893" class="Comment">-----------------</a>
<a id="2915" class="Symbol">→</a> <a id="2917" href="/19.08/Confluence/#2842" class="Bound">L</a> <a id="2919" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="2921" href="plfa.part2.Confluence.html#2847" class="Bound">M</a> <a id="2923" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="2925" href="plfa.part2.Confluence.html#2844" class="Bound">L′</a> <a id="2928" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="2930" href="plfa.part2.Confluence.html#2849" class="Bound">M′</a>
<a id="_⇛_.pbeta"></a><a id="2936" href="/19.08/Confluence/#2936" class="InductiveConstructor">pbeta</a> <a id="2942" class="Symbol">:</a> <a id="2944" class="Symbol">∀{</a><a id="2946" href="plfa.part2.Confluence.html#2946" class="Bound">Γ</a><a id="2947" class="Symbol">}{</a><a id="2949" href="plfa.part2.Confluence.html#2949" class="Bound">N</a> <a id="2951" href="plfa.part2.Confluence.html#2951" class="Bound">N′</a> <a id="2955" class="Symbol">:</a> <a id="2957" href="plfa.part2.Confluence.html#2946" class="Bound">Γ</a> <a id="2959" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="2961" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="2963" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="2965" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="2966" class="Symbol">}{</a><a id="2968" href="plfa.part2.Confluence.html#2968" class="Bound">M</a> <a id="2970" href="plfa.part2.Confluence.html#2970" class="Bound">M′</a> <a id="2973" class="Symbol">:</a> <a id="2975" href="plfa.part2.Confluence.html#2946" class="Bound">Γ</a> <a id="2977" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="2979" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="2980" class="Symbol">}</a>
<a id="2986" class="Symbol">→</a> <a id="2988" href="/19.08/Confluence/#2949" class="Bound">N</a> <a id="2990" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="2992" href="plfa.part2.Confluence.html#2951" class="Bound">N′</a>
<a id="2999" class="Symbol">→</a> <a id="3001" href="/19.08/Confluence/#2968" class="Bound">M</a> <a id="3003" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="3005" href="plfa.part2.Confluence.html#2970" class="Bound">M′</a>
<a id="3014" class="Comment">-----------------------</a>
<a id="3042" class="Symbol">→</a> <a id="3044" class="Symbol">(</a><a id="3045" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="3047" href="/19.08/Confluence/#2949" class="Bound">N</a><a id="3048" class="Symbol">)</a> <a id="3050" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="3052" href="plfa.part2.Confluence.html#2968" class="Bound">M</a> <a id="3055" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="3058" href="plfa.part2.Confluence.html#2951" class="Bound">N′</a> <a id="3061" href="plfa.part2.Untyped.html#7491" class="Function Operator">[</a> <a id="3063" href="plfa.part2.Confluence.html#2970" class="Bound">M′</a> <a id="3066" href="plfa.part2.Untyped.html#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="3469" href="/19.08/Confluence/#3469" class="Function">par-refl</a> <a id="3478" class="Symbol">:</a> <a id="3480" class="Symbol">∀{</a><a id="3482" href="plfa.part2.Confluence.html#3482" class="Bound">Γ</a> <a id="3484" href="plfa.part2.Confluence.html#3484" class="Bound">A</a><a id="3485" class="Symbol">}{</a><a id="3487" href="plfa.part2.Confluence.html#3487" class="Bound">M</a> <a id="3489" class="Symbol">:</a> <a id="3491" href="plfa.part2.Confluence.html#3482" class="Bound">Γ</a> <a id="3493" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3495" href="plfa.part2.Confluence.html#3484" class="Bound">A</a><a id="3496" class="Symbol">}</a> <a id="3498" class="Symbol">→</a> <a id="3500" href="plfa.part2.Confluence.html#3487" class="Bound">M</a> <a id="3502" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="3504" href="plfa.part2.Confluence.html#3487" class="Bound">M</a>
<a id="3506" href="/19.08/Confluence/#3469" class="Function">par-refl</a> <a id="3515" class="Symbol">{</a><a id="3516" href="plfa.part2.Confluence.html#3516" class="Bound">Γ</a><a id="3517" class="Symbol">}</a> <a id="3519" class="Symbol">{</a><a id="3520" href="plfa.part2.Confluence.html#3520" class="Bound">A</a><a id="3521" class="Symbol">}</a> <a id="3523" class="Symbol">{</a><a id="3524" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="3526" href="plfa.part2.Confluence.html#3526" class="Bound">x</a><a id="3527" class="Symbol">}</a> <a id="3529" class="Symbol">=</a> <a id="3531" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a>
<a id="3536" href="/19.08/Confluence/#3469" class="Function">par-refl</a> <a id="3545" class="Symbol">{</a><a id="3546" href="plfa.part2.Confluence.html#3546" class="Bound">Γ</a><a id="3547" class="Symbol">}</a> <a id="3549" class="Symbol">{</a><a id="3550" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="3551" class="Symbol">}</a> <a id="3553" class="Symbol">{</a><a id="3554" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="3556" href="plfa.part2.Confluence.html#3556" class="Bound">N</a><a id="3557" class="Symbol">}</a> <a id="3559" class="Symbol">=</a> <a id="3561" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="3566" href="plfa.part2.Confluence.html#3469" class="Function">par-refl</a>
<a id="3575" href="/19.08/Confluence/#3469" class="Function">par-refl</a> <a id="3584" class="Symbol">{</a><a id="3585" href="plfa.part2.Confluence.html#3585" class="Bound">Γ</a><a id="3586" class="Symbol">}</a> <a id="3588" class="Symbol">{</a><a id="3589" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="3590" class="Symbol">}</a> <a id="3592" class="Symbol">{</a><a id="3593" href="plfa.part2.Confluence.html#3593" class="Bound">L</a> <a id="3595" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="3597" href="plfa.part2.Confluence.html#3597" class="Bound">M</a><a id="3598" class="Symbol">}</a> <a id="3600" class="Symbol">=</a> <a id="3602" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="3607" href="plfa.part2.Confluence.html#3469" class="Function">par-refl</a> <a id="3616" href="plfa.part2.Confluence.html#3469" class="Function">par-refl</a>
</pre>
<p>We define the sequences of parallel reduction as follows.</p>
<pre class="Agda"><a id="3692" class="Keyword">infix</a> <a id="3699" class="Number">2</a> <a id="3701" href="/19.08/Confluence/#3740" class="Datatype Operator">_⇛*_</a>
<a id="3706" class="Keyword">infixr</a> <a id="3713" class="Number">2</a> <a id="3715" href="/19.08/Confluence/#3846" class="InductiveConstructor Operator">_⇛⟨_⟩_</a>
<a id="3722" class="Keyword">infix</a> <a id="3729" class="Number">3</a> <a id="3731" href="/19.08/Confluence/#3790" class="InductiveConstructor Operator">_∎</a>
<a id="3735" class="Keyword">data</a> <a id="_⇛*_"></a><a id="3740" href="/19.08/Confluence/#3740" class="Datatype Operator">_⇛*_</a> <a id="3745" class="Symbol">:</a> <a id="3747" class="Symbol">∀</a> <a id="3749" class="Symbol">{</a><a id="3750" href="plfa.part2.Confluence.html#3750" class="Bound">Γ</a> <a id="3752" href="plfa.part2.Confluence.html#3752" class="Bound">A</a><a id="3753" class="Symbol">}</a> <a id="3755" class="Symbol">→</a> <a id="3757" class="Symbol">(</a><a id="3758" href="plfa.part2.Confluence.html#3750" class="Bound">Γ</a> <a id="3760" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3762" href="plfa.part2.Confluence.html#3752" class="Bound">A</a><a id="3763" class="Symbol">)</a> <a id="3765" class="Symbol">→</a> <a id="3767" class="Symbol">(</a><a id="3768" href="plfa.part2.Confluence.html#3750" class="Bound">Γ</a> <a id="3770" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="3772" href="plfa.part2.Confluence.html#3752" class="Bound">A</a><a id="3773" class="Symbol">)</a> <a id="3775" class="Symbol">→</a> <a id="3777" class="PrimitiveType">Set</a> <a id="3781" class="Keyword">where</a>
<a id="_⇛*_._∎"></a><a id="3790" href="/19.08/Confluence/#3790" class="InductiveConstructor Operator">_∎</a> <a id="3793" class="Symbol">:</a> <a id="3795" class="Symbol">∀</a> <a id="3797" class="Symbol">{</a><a id="3798" href="plfa.part2.Confluence.html#3798" class="Bound">Γ</a> <a id="3800" href="plfa.part2.Confluence.html#3800" class="Bound">A</a><a id="3801" class="Symbol">}</a> <a id="3803" class="Symbol">(</a><a id="3804" href="plfa.part2.Confluence.html#3804" class="Bound">M</a> <a id="3806" class="Symbol">:</a> <a id="3808" href="plfa.part2.Confluence.html#3798" class="Bound">Γ</a> <a id="3810" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3812" href="plfa.part2.Confluence.html#3800" class="Bound">A</a><a id="3813" class="Symbol">)</a>
<a id="3821" class="Comment">--------</a>
<a id="3834" class="Symbol">→</a> <a id="3836" href="/19.08/Confluence/#3804" class="Bound">M</a> <a id="3838" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="3841" href="plfa.part2.Confluence.html#3804" class="Bound">M</a>
<a id="_⇛*_._⇛⟨_⟩_"></a><a id="3846" href="/19.08/Confluence/#3846" class="InductiveConstructor Operator">_⇛⟨_⟩_</a> <a id="3853" class="Symbol">:</a> <a id="3855" class="Symbol">∀</a> <a id="3857" class="Symbol">{</a><a id="3858" href="plfa.part2.Confluence.html#3858" class="Bound">Γ</a> <a id="3860" href="plfa.part2.Confluence.html#3860" class="Bound">A</a><a id="3861" class="Symbol">}</a> <a id="3863" class="Symbol">(</a><a id="3864" href="plfa.part2.Confluence.html#3864" class="Bound">L</a> <a id="3866" class="Symbol">:</a> <a id="3868" href="plfa.part2.Confluence.html#3858" class="Bound">Γ</a> <a id="3870" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="3872" href="plfa.part2.Confluence.html#3860" class="Bound">A</a><a id="3873" class="Symbol">)</a> <a id="3875" class="Symbol">{</a><a id="3876" href="plfa.part2.Confluence.html#3876" class="Bound">M</a> <a id="3878" href="plfa.part2.Confluence.html#3878" class="Bound">N</a> <a id="3880" class="Symbol">:</a> <a id="3882" href="plfa.part2.Confluence.html#3858" class="Bound">Γ</a> <a id="3884" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="3886" href="plfa.part2.Confluence.html#3860" class="Bound">A</a><a id="3887" class="Symbol">}</a>
<a id="3893" class="Symbol">→</a> <a id="3895" href="/19.08/Confluence/#3864" class="Bound">L</a> <a id="3897" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="3899" href="plfa.part2.Confluence.html#3876" class="Bound">M</a>
<a id="3905" class="Symbol">→</a> <a id="3907" href="/19.08/Confluence/#3876" class="Bound">M</a> <a id="3909" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="3912" href="plfa.part2.Confluence.html#3878" class="Bound">N</a>
<a id="3920" class="Comment">---------</a>
<a id="3934" class="Symbol">→</a> <a id="3936" href="/19.08/Confluence/#3864" class="Bound">L</a> <a id="3938" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="3941" href="plfa.part2.Confluence.html#3878" 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="4143" 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="4457" href="/19.08/Confluence/#4457" class="Function">beta-par</a> <a id="4466" class="Symbol">:</a> <a id="4468" class="Symbol">∀{</a><a id="4470" href="plfa.part2.Confluence.html#4470" class="Bound">Γ</a> <a id="4472" href="plfa.part2.Confluence.html#4472" class="Bound">A</a><a id="4473" class="Symbol">}{</a><a id="4475" href="plfa.part2.Confluence.html#4475" class="Bound">M</a> <a id="4477" href="plfa.part2.Confluence.html#4477" class="Bound">N</a> <a id="4479" class="Symbol">:</a> <a id="4481" href="plfa.part2.Confluence.html#4470" class="Bound">Γ</a> <a id="4483" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="4485" href="plfa.part2.Confluence.html#4472" class="Bound">A</a><a id="4486" class="Symbol">}</a>
<a id="4490" class="Symbol">→</a> <a id="4492" href="/19.08/Confluence/#4475" class="Bound">M</a> <a id="4494" href="/19.08/Untyped/#10147" class="Datatype Operator">—→</a> <a id="4497" href="plfa.part2.Confluence.html#4477" class="Bound">N</a>
<a id="4503" class="Comment">------</a>
<a id="4512" class="Symbol">→</a> <a id="4514" href="/19.08/Confluence/#4475" class="Bound">M</a> <a id="4516" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="4518" href="plfa.part2.Confluence.html#4477" class="Bound">N</a>
<a id="4520" href="/19.08/Confluence/#4457" class="Function">beta-par</a> <a id="4529" class="Symbol">{</a><a id="4530" href="plfa.part2.Confluence.html#4530" class="Bound">Γ</a><a id="4531" class="Symbol">}</a> <a id="4533" class="Symbol">{</a><a id="4534" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="4535" class="Symbol">}</a> <a id="4537" class="Symbol">{</a><a id="4538" href="plfa.part2.Confluence.html#4538" class="Bound">L</a> <a id="4540" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="4542" href="plfa.part2.Confluence.html#4542" class="Bound">M</a><a id="4543" class="Symbol">}</a> <a id="4545" class="Symbol">(</a><a id="4546" href="plfa.part2.Untyped.html#10197" class="InductiveConstructor">ξ₁</a> <a id="4549" href="plfa.part2.Confluence.html#4549" class="Bound">r</a><a id="4550" class="Symbol">)</a> <a id="4552" class="Symbol">=</a> <a id="4554" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="4559" class="Symbol">(</a><a id="4560" href="plfa.part2.Confluence.html#4457" class="Function">beta-par</a> <a id="4569" class="Symbol">{</a><a id="4570" class="Argument">M</a> <a id="4572" class="Symbol">=</a> <a id="4574" href="plfa.part2.Confluence.html#4538" class="Bound">L</a><a id="4575" class="Symbol">}</a> <a id="4577" href="plfa.part2.Confluence.html#4549" class="Bound">r</a><a id="4578" class="Symbol">)</a> <a id="4580" href="plfa.part2.Confluence.html#3469" class="Function">par-refl</a>
<a id="4589" href="/19.08/Confluence/#4457" class="Function">beta-par</a> <a id="4598" class="Symbol">{</a><a id="4599" href="plfa.part2.Confluence.html#4599" class="Bound">Γ</a><a id="4600" class="Symbol">}</a> <a id="4602" class="Symbol">{</a><a id="4603" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="4604" class="Symbol">}</a> <a id="4606" class="Symbol">{</a><a id="4607" href="plfa.part2.Confluence.html#4607" class="Bound">L</a> <a id="4609" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="4611" href="plfa.part2.Confluence.html#4611" class="Bound">M</a><a id="4612" class="Symbol">}</a> <a id="4614" class="Symbol">(</a><a id="4615" href="plfa.part2.Untyped.html#10287" class="InductiveConstructor">ξ₂</a> <a id="4618" href="plfa.part2.Confluence.html#4618" class="Bound">r</a><a id="4619" class="Symbol">)</a> <a id="4621" class="Symbol">=</a> <a id="4623" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="4628" href="plfa.part2.Confluence.html#3469" class="Function">par-refl</a> <a id="4637" class="Symbol">(</a><a id="4638" href="plfa.part2.Confluence.html#4457" class="Function">beta-par</a> <a id="4647" class="Symbol">{</a><a id="4648" class="Argument">M</a> <a id="4650" class="Symbol">=</a> <a id="4652" href="plfa.part2.Confluence.html#4611" class="Bound">M</a><a id="4653" class="Symbol">}</a> <a id="4655" href="plfa.part2.Confluence.html#4618" class="Bound">r</a><a id="4656" class="Symbol">)</a>
<a id="4658" href="/19.08/Confluence/#4457" class="Function">beta-par</a> <a id="4667" class="Symbol">{</a><a id="4668" href="plfa.part2.Confluence.html#4668" class="Bound">Γ</a><a id="4669" class="Symbol">}</a> <a id="4671" class="Symbol">{</a><a id="4672" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="4673" class="Symbol">}</a> <a id="4675" class="Symbol">{(</a><a id="4677" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="4679" href="plfa.part2.Confluence.html#4679" class="Bound">N</a><a id="4680" class="Symbol">)</a> <a id="4682" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="4684" href="plfa.part2.Confluence.html#4684" class="Bound">M</a><a id="4685" class="Symbol">}</a> <a id="4687" href="plfa.part2.Untyped.html#10377" class="InductiveConstructor">β</a> <a id="4689" class="Symbol">=</a> <a id="4691" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a> <a id="4697" href="plfa.part2.Confluence.html#3469" class="Function">par-refl</a> <a id="4706" href="plfa.part2.Confluence.html#3469" class="Function">par-refl</a>
<a id="4715" href="/19.08/Confluence/#4457" class="Function">beta-par</a> <a id="4724" class="Symbol">{</a><a id="4725" href="plfa.part2.Confluence.html#4725" class="Bound">Γ</a><a id="4726" class="Symbol">}</a> <a id="4728" class="Symbol">{</a><a id="4729" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="4730" class="Symbol">}</a> <a id="4732" class="Symbol">{</a><a id="4733" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="4735" href="plfa.part2.Confluence.html#4735" class="Bound">N</a><a id="4736" class="Symbol">}</a> <a id="4738" class="Symbol">(</a><a id="4739" href="plfa.part2.Untyped.html#10485" class="InductiveConstructor">ζ</a> <a id="4741" href="plfa.part2.Confluence.html#4741" class="Bound">r</a><a id="4742" class="Symbol">)</a> <a id="4744" class="Symbol">=</a> <a id="4746" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="4751" class="Symbol">(</a><a id="4752" href="plfa.part2.Confluence.html#4457" class="Function">beta-par</a> <a id="4761" href="plfa.part2.Confluence.html#4741" class="Bound">r</a><a id="4762" 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="4942" href="/19.08/Confluence/#4942" class="Function">betas-pars</a> <a id="4953" class="Symbol">:</a> <a id="4955" class="Symbol">∀{</a><a id="4957" href="plfa.part2.Confluence.html#4957" class="Bound">Γ</a> <a id="4959" href="plfa.part2.Confluence.html#4959" class="Bound">A</a><a id="4960" class="Symbol">}</a> <a id="4962" class="Symbol">{</a><a id="4963" href="plfa.part2.Confluence.html#4963" class="Bound">M</a> <a id="4965" href="plfa.part2.Confluence.html#4965" class="Bound">N</a> <a id="4967" class="Symbol">:</a> <a id="4969" href="plfa.part2.Confluence.html#4957" class="Bound">Γ</a> <a id="4971" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="4973" href="plfa.part2.Confluence.html#4959" class="Bound">A</a><a id="4974" class="Symbol">}</a>
<a id="4978" class="Symbol">→</a> <a id="4980" href="/19.08/Confluence/#4963" class="Bound">M</a> <a id="4982" href="/19.08/Untyped/#11267" class="Datatype Operator">—↠</a> <a id="4985" href="plfa.part2.Confluence.html#4965" class="Bound">N</a>
<a id="4991" class="Comment">------</a>
<a id="5000" class="Symbol">→</a> <a id="5002" href="/19.08/Confluence/#4963" class="Bound">M</a> <a id="5004" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="5007" href="plfa.part2.Confluence.html#4965" class="Bound">N</a>
<a id="5009" href="/19.08/Confluence/#4942" class="Function">betas-pars</a> <a id="5020" class="Symbol">{</a><a id="5021" href="plfa.part2.Confluence.html#5021" class="Bound">Γ</a><a id="5022" class="Symbol">}</a> <a id="5024" class="Symbol">{</a><a id="5025" href="plfa.part2.Confluence.html#5025" class="Bound">A</a><a id="5026" class="Symbol">}</a> <a id="5028" class="Symbol">{</a><a id="5029" href="plfa.part2.Confluence.html#5029" class="Bound">M₁</a><a id="5031" class="Symbol">}</a> <a id="5033" class="Symbol">{</a><a id="5034" class="DottedPattern Symbol">.</a><a id="5035" href="plfa.part2.Confluence.html#5029" class="DottedPattern Bound">M₁</a><a id="5037" class="Symbol">}</a> <a id="5039" class="Symbol">(</a><a id="5040" href="plfa.part2.Confluence.html#5029" class="Bound">M₁</a> <a id="5043" href="/19.08/Untyped/#11317" class="InductiveConstructor Operator">∎</a><a id="5044" class="Symbol">)</a> <a id="5046" class="Symbol">=</a> <a id="5048" href="plfa.part2.Confluence.html#5029" class="Bound">M₁</a> <a id="5051" href="plfa.part2.Confluence.html#3790" class="InductiveConstructor Operator">∎</a>
<a id="5053" href="/19.08/Confluence/#4942" class="Function">betas-pars</a> <a id="5064" class="Symbol">{</a><a id="5065" href="plfa.part2.Confluence.html#5065" class="Bound">Γ</a><a id="5066" class="Symbol">}</a> <a id="5068" class="Symbol">{</a><a id="5069" href="plfa.part2.Confluence.html#5069" class="Bound">A</a><a id="5070" class="Symbol">}</a> <a id="5072" class="Symbol">{</a><a id="5073" class="DottedPattern Symbol">.</a><a id="5074" href="plfa.part2.Confluence.html#5082" class="DottedPattern Bound">L</a><a id="5075" class="Symbol">}</a> <a id="5077" class="Symbol">{</a><a id="5078" href="plfa.part2.Confluence.html#5078" class="Bound">N</a><a id="5079" class="Symbol">}</a> <a id="5081" class="Symbol">(</a><a id="5082" href="plfa.part2.Confluence.html#5082" class="Bound">L</a> <a id="5084" href="/19.08/Untyped/#11373" class="InductiveConstructor Operator">—→⟨</a> <a id="5088" href="plfa.part2.Confluence.html#5088" class="Bound">b</a> <a id="5090" href="plfa.part2.Untyped.html#11373" class="InductiveConstructor Operator">⟩</a> <a id="5092" href="plfa.part2.Confluence.html#5092" class="Bound">bs</a><a id="5094" class="Symbol">)</a> <a id="5096" class="Symbol">=</a>
<a id="5101" href="/19.08/Confluence/#5082" class="Bound">L</a> <a id="5103" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⇛⟨</a> <a id="5106" href="plfa.part2.Confluence.html#4457" class="Function">beta-par</a> <a id="5115" href="plfa.part2.Confluence.html#5088" class="Bound">b</a> <a id="5117" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⟩</a> <a id="5119" href="plfa.part2.Confluence.html#4942" class="Function">betas-pars</a> <a id="5130" href="plfa.part2.Confluence.html#5092" 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="5411" href="/19.08/Confluence/#5411" class="Function">par-betas</a> <a id="5421" class="Symbol">:</a> <a id="5423" class="Symbol">∀{</a><a id="5425" href="plfa.part2.Confluence.html#5425" class="Bound">Γ</a> <a id="5427" href="plfa.part2.Confluence.html#5427" class="Bound">A</a><a id="5428" class="Symbol">}{</a><a id="5430" href="plfa.part2.Confluence.html#5430" class="Bound">M</a> <a id="5432" href="plfa.part2.Confluence.html#5432" class="Bound">N</a> <a id="5434" class="Symbol">:</a> <a id="5436" href="plfa.part2.Confluence.html#5425" class="Bound">Γ</a> <a id="5438" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="5440" href="plfa.part2.Confluence.html#5427" class="Bound">A</a><a id="5441" class="Symbol">}</a>
<a id="5445" class="Symbol">→</a> <a id="5447" href="/19.08/Confluence/#5430" class="Bound">M</a> <a id="5449" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="5451" href="plfa.part2.Confluence.html#5432" class="Bound">N</a>
<a id="5457" class="Comment">------</a>
<a id="5466" class="Symbol">→</a> <a id="5468" href="/19.08/Confluence/#5430" class="Bound">M</a> <a id="5470" href="/19.08/Untyped/#11267" class="Datatype Operator">—↠</a> <a id="5473" href="plfa.part2.Confluence.html#5432" class="Bound">N</a>
<a id="5475" href="/19.08/Confluence/#5411" class="Function">par-betas</a> <a id="5485" class="Symbol">{</a><a id="5486" href="plfa.part2.Confluence.html#5486" class="Bound">Γ</a><a id="5487" class="Symbol">}</a> <a id="5489" class="Symbol">{</a><a id="5490" href="plfa.part2.Confluence.html#5490" class="Bound">A</a><a id="5491" class="Symbol">}</a> <a id="5493" class="Symbol">{</a><a id="5494" class="DottedPattern Symbol">.(</a><a id="5496" href="/19.08/Untyped/#4330" class="DottedPattern InductiveConstructor Operator">`</a> <a id="5498" class="DottedPattern Symbol">_)</a><a id="5500" class="Symbol">}</a> <a id="5502" class="Symbol">(</a><a id="5503" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a><a id="5507" class="Symbol">{</a><a id="5508" class="Argument">x</a> <a id="5510" class="Symbol">=</a> <a id="5512" href="plfa.part2.Confluence.html#5512" class="Bound">x</a><a id="5513" class="Symbol">})</a> <a id="5516" class="Symbol">=</a> <a id="5518" class="Symbol">(</a><a id="5519" href="plfa.part2.Untyped.html#4330" class="InductiveConstructor Operator">`</a> <a id="5521" href="plfa.part2.Confluence.html#5512" class="Bound">x</a><a id="5522" class="Symbol">)</a> <a id="5524" href="plfa.part2.Untyped.html#11317" class="InductiveConstructor Operator">∎</a>
<a id="5526" href="/19.08/Confluence/#5411" class="Function">par-betas</a> <a id="5536" class="Symbol">{</a><a id="5537" href="plfa.part2.Confluence.html#5537" class="Bound">Γ</a><a id="5538" class="Symbol">}</a> <a id="5540" class="Symbol">{</a><a id="5541" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="5542" class="Symbol">}</a> <a id="5544" class="Symbol">{</a><a id="5545" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5547" href="plfa.part2.Confluence.html#5547" class="Bound">N</a><a id="5548" class="Symbol">}</a> <a id="5550" class="Symbol">(</a><a id="5551" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="5556" href="plfa.part2.Confluence.html#5556" class="Bound">p</a><a id="5557" class="Symbol">)</a> <a id="5559" class="Symbol">=</a> <a id="5561" href="plfa.part2.Untyped.html#23800" class="Function">abs-cong</a> <a id="5570" class="Symbol">(</a><a id="5571" href="plfa.part2.Confluence.html#5411" class="Function">par-betas</a> <a id="5581" href="plfa.part2.Confluence.html#5556" class="Bound">p</a><a id="5582" class="Symbol">)</a>
<a id="5584" href="/19.08/Confluence/#5411" class="Function">par-betas</a> <a id="5594" class="Symbol">{</a><a id="5595" href="plfa.part2.Confluence.html#5595" class="Bound">Γ</a><a id="5596" class="Symbol">}</a> <a id="5598" class="Symbol">{</a><a id="5599" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="5600" class="Symbol">}</a> <a id="5602" class="Symbol">{</a><a id="5603" href="plfa.part2.Confluence.html#5603" class="Bound">L</a> <a id="5605" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="5607" href="plfa.part2.Confluence.html#5607" class="Bound">M</a><a id="5608" class="Symbol">}</a> <a id="5610" class="Symbol">(</a><a id="5611" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="5616" href="plfa.part2.Confluence.html#5616" class="Bound">p₁</a> <a id="5619" href="plfa.part2.Confluence.html#5619" class="Bound">p₂</a><a id="5621" class="Symbol">)</a> <a id="5623" class="Symbol">=</a>
<a id="5628" href="/19.08/Untyped/#21619" class="Function">—↠-trans</a> <a id="5637" class="Symbol">(</a><a id="5638" href="plfa.part2.Untyped.html#22803" class="Function">appL-cong</a><a id="5647" class="Symbol">{</a><a id="5648" class="Argument">M</a> <a id="5650" class="Symbol">=</a> <a id="5652" href="/19.08/Confluence/#5607" class="Bound">M</a><a id="5653" class="Symbol">}</a> <a id="5655" class="Symbol">(</a><a id="5656" href="plfa.part2.Confluence.html#5411" class="Function">par-betas</a> <a id="5666" href="plfa.part2.Confluence.html#5616" class="Bound">p₁</a><a id="5668" class="Symbol">))</a> <a id="5671" class="Symbol">(</a><a id="5672" href="plfa.part2.Untyped.html#23572" class="Function">appR-cong</a> <a id="5682" class="Symbol">(</a><a id="5683" href="plfa.part2.Confluence.html#5411" class="Function">par-betas</a> <a id="5693" href="plfa.part2.Confluence.html#5619" class="Bound">p₂</a><a id="5695" class="Symbol">))</a>
<a id="5698" href="/19.08/Confluence/#5411" class="Function">par-betas</a> <a id="5708" class="Symbol">{</a><a id="5709" href="plfa.part2.Confluence.html#5709" class="Bound">Γ</a><a id="5710" class="Symbol">}</a> <a id="5712" class="Symbol">{</a><a id="5713" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="5714" class="Symbol">}</a> <a id="5716" class="Symbol">{(</a><a id="5718" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5720" href="plfa.part2.Confluence.html#5720" class="Bound">N</a><a id="5721" class="Symbol">)</a> <a id="5723" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="5725" href="plfa.part2.Confluence.html#5725" class="Bound">M</a><a id="5726" class="Symbol">}</a> <a id="5728" class="Symbol">(</a><a id="5729" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a><a id="5734" class="Symbol">{</a><a id="5735" class="Argument">N′</a> <a id="5738" class="Symbol">=</a> <a id="5740" href="plfa.part2.Confluence.html#5740" class="Bound">N′</a><a id="5742" class="Symbol">}{</a><a id="5744" class="Argument">M′</a> <a id="5747" class="Symbol">=</a> <a id="5749" href="plfa.part2.Confluence.html#5749" class="Bound">M′</a><a id="5751" class="Symbol">}</a> <a id="5753" href="plfa.part2.Confluence.html#5753" class="Bound">p₁</a> <a id="5756" href="plfa.part2.Confluence.html#5756" class="Bound">p₂</a><a id="5758" class="Symbol">)</a> <a id="5760" class="Symbol">=</a>
<a id="5764" class="Keyword">let</a> <a id="5768" href="/19.08/Confluence/#5768" class="Bound">ih₁</a> <a id="5772" class="Symbol">=</a> <a id="5774" href="plfa.part2.Confluence.html#5411" class="Function">par-betas</a> <a id="5784" href="plfa.part2.Confluence.html#5753" class="Bound">p₁</a> <a id="5787" class="Keyword">in</a>
<a id="5792" class="Keyword">let</a> <a id="5796" href="/19.08/Confluence/#5796" class="Bound">ih₂</a> <a id="5800" class="Symbol">=</a> <a id="5802" href="plfa.part2.Confluence.html#5411" class="Function">par-betas</a> <a id="5812" href="plfa.part2.Confluence.html#5756" class="Bound">p₂</a> <a id="5815" class="Keyword">in</a>
<a id="5820" class="Keyword">let</a> <a id="5824" href="/19.08/Confluence/#5824" class="Bound">a</a> <a id="5826" class="Symbol">:</a> <a id="5828" class="Symbol">(</a><a id="5829" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5831" href="plfa.part2.Confluence.html#5720" class="Bound">N</a><a id="5832" class="Symbol">)</a> <a id="5834" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="5836" href="plfa.part2.Confluence.html#5725" class="Bound">M</a> <a id="5838" href="plfa.part2.Untyped.html#11267" class="Datatype Operator">—↠</a> <a id="5841" class="Symbol">(</a><a id="5842" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5844" href="plfa.part2.Confluence.html#5740" class="Bound">N′</a><a id="5846" class="Symbol">)</a> <a id="5848" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="5850" href="plfa.part2.Confluence.html#5725" class="Bound">M</a>
<a id="5858" href="/19.08/Confluence/#5824" class="Bound">a</a> <a id="5860" class="Symbol">=</a> <a id="5862" href="/19.08/Untyped/#22803" class="Function">appL-cong</a><a id="5871" class="Symbol">{</a><a id="5872" class="Argument">M</a> <a id="5874" class="Symbol">=</a> <a id="5876" href="plfa.part2.Confluence.html#5725" class="Bound">M</a><a id="5877" class="Symbol">}</a> <a id="5879" class="Symbol">(</a><a id="5880" href="plfa.part2.Untyped.html#23800" class="Function">abs-cong</a> <a id="5889" href="plfa.part2.Confluence.html#5768" class="Bound">ih₁</a><a id="5892" class="Symbol">)</a> <a id="5894" class="Keyword">in</a>
<a id="5899" class="Keyword">let</a> <a id="5903" href="/19.08/Confluence/#5903" class="Bound">b</a> <a id="5905" class="Symbol">:</a> <a id="5907" class="Symbol">(</a><a id="5908" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5910" href="plfa.part2.Confluence.html#5740" class="Bound">N′</a><a id="5912" class="Symbol">)</a> <a id="5914" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="5916" href="plfa.part2.Confluence.html#5725" class="Bound">M</a> <a id="5918" href="plfa.part2.Untyped.html#11267" class="Datatype Operator">—↠</a> <a id="5921" class="Symbol">(</a><a id="5922" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5924" href="plfa.part2.Confluence.html#5740" class="Bound">N′</a><a id="5926" class="Symbol">)</a> <a id="5928" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="5930" href="plfa.part2.Confluence.html#5749" class="Bound">M′</a>
<a id="5939" href="/19.08/Confluence/#5903" class="Bound">b</a> <a id="5941" class="Symbol">=</a> <a id="5943" href="/19.08/Untyped/#23572" class="Function">appR-cong</a><a id="5952" class="Symbol">{</a><a id="5953" class="Argument">L</a> <a id="5955" class="Symbol">=</a> <a id="5957" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5959" href="plfa.part2.Confluence.html#5740" class="Bound">N′</a><a id="5961" class="Symbol">}</a> <a id="5963" href="plfa.part2.Confluence.html#5796" class="Bound">ih₂</a> <a id="5967" class="Keyword">in</a>
<a id="5972" class="Keyword">let</a> <a id="5976" href="/19.08/Confluence/#5976" class="Bound">c</a> <a id="5978" class="Symbol">=</a> <a id="5980" class="Symbol">(</a><a id="5981" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="5983" href="plfa.part2.Confluence.html#5740" class="Bound">N′</a><a id="5985" class="Symbol">)</a> <a id="5987" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="5989" href="plfa.part2.Confluence.html#5749" class="Bound">M′</a> <a id="5992" href="plfa.part2.Untyped.html#11373" class="InductiveConstructor Operator">—→⟨</a> <a id="5996" href="plfa.part2.Untyped.html#10377" class="InductiveConstructor">β</a> <a id="5998" href="plfa.part2.Untyped.html#11373" class="InductiveConstructor Operator">⟩</a> <a id="6000" href="plfa.part2.Confluence.html#5740" class="Bound">N′</a> <a id="6003" href="plfa.part2.Untyped.html#7491" class="Function Operator">[</a> <a id="6005" href="plfa.part2.Confluence.html#5749" class="Bound">M′</a> <a id="6008" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a> <a id="6010" href="plfa.part2.Untyped.html#11317" class="InductiveConstructor Operator">∎</a> <a id="6012" class="Keyword">in</a>
<a id="6017" href="/19.08/Untyped/#21619" class="Function">—↠-trans</a> <a id="6026" class="Symbol">(</a><a id="6027" href="plfa.part2.Untyped.html#21619" class="Function">—↠-trans</a> <a id="6036" href="/19.08/Confluence/#5824" class="Bound">a</a> <a id="6038" href="plfa.part2.Confluence.html#5903" class="Bound">b</a><a id="6039" class="Symbol">)</a> <a id="6041" href="plfa.part2.Confluence.html#5976" class="Bound">c</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. We conclude using the transitity
of <code class="language-plaintext highlighter-rouge">—↠</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>.
By similar reasoning, we have
<code class="language-plaintext highlighter-rouge">(ƛ N) · M —↠ (ƛ N′) · M′</code>.
Of course, <code class="language-plaintext highlighter-rouge">(ƛ N′) · M′ —→ N′ [ M′ ]</code>, so we can conclude
using the transitivity of <code class="language-plaintext highlighter-rouge">—↠</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="6888" href="/19.08/Confluence/#6888" class="Function">pars-betas</a> <a id="6899" class="Symbol">:</a> <a id="6901" class="Symbol">∀{</a><a id="6903" href="plfa.part2.Confluence.html#6903" class="Bound">Γ</a> <a id="6905" href="plfa.part2.Confluence.html#6905" class="Bound">A</a><a id="6906" class="Symbol">}</a> <a id="6908" class="Symbol">{</a><a id="6909" href="plfa.part2.Confluence.html#6909" class="Bound">M</a> <a id="6911" href="plfa.part2.Confluence.html#6911" class="Bound">N</a> <a id="6913" class="Symbol">:</a> <a id="6915" href="plfa.part2.Confluence.html#6903" class="Bound">Γ</a> <a id="6917" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="6919" href="plfa.part2.Confluence.html#6905" class="Bound">A</a><a id="6920" class="Symbol">}</a>
<a id="6924" class="Symbol">→</a> <a id="6926" href="/19.08/Confluence/#6909" class="Bound">M</a> <a id="6928" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="6931" href="plfa.part2.Confluence.html#6911" class="Bound">N</a>
<a id="6937" class="Comment">------</a>
<a id="6946" class="Symbol">→</a> <a id="6948" href="/19.08/Confluence/#6909" class="Bound">M</a> <a id="6950" href="/19.08/Untyped/#11267" class="Datatype Operator">—↠</a> <a id="6953" href="plfa.part2.Confluence.html#6911" class="Bound">N</a>
<a id="6955" href="/19.08/Confluence/#6888" class="Function">pars-betas</a> <a id="6966" class="Symbol">(</a><a id="6967" href="plfa.part2.Confluence.html#6967" class="Bound">M₁</a> <a id="6970" href="plfa.part2.Confluence.html#3790" class="InductiveConstructor Operator">∎</a><a id="6971" class="Symbol">)</a> <a id="6973" class="Symbol">=</a> <a id="6975" href="plfa.part2.Confluence.html#6967" class="Bound">M₁</a> <a id="6978" href="/19.08/Untyped/#11317" class="InductiveConstructor Operator">∎</a>
<a id="6980" href="/19.08/Confluence/#6888" class="Function">pars-betas</a> <a id="6991" class="Symbol">(</a><a id="6992" href="plfa.part2.Confluence.html#6992" class="Bound">L</a> <a id="6994" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⇛⟨</a> <a id="6997" href="plfa.part2.Confluence.html#6997" class="Bound">p</a> <a id="6999" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⟩</a> <a id="7001" href="plfa.part2.Confluence.html#7001" class="Bound">ps</a><a id="7003" class="Symbol">)</a> <a id="7005" class="Symbol">=</a> <a id="7007" href="/19.08/Untyped/#21619" class="Function">—↠-trans</a> <a id="7016" class="Symbol">(</a><a id="7017" href="plfa.part2.Confluence.html#5411" class="Function">par-betas</a> <a id="7027" href="plfa.part2.Confluence.html#6997" class="Bound">p</a><a id="7028" class="Symbol">)</a> <a id="7030" class="Symbol">(</a><a id="7031" href="plfa.part2.Confluence.html#6888" class="Function">pars-betas</a> <a id="7042" href="plfa.part2.Confluence.html#7001" class="Bound">ps</a><a id="7044" 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="7554" href="/19.08/Confluence/#7554" class="Function">par-subst</a> <a id="7564" class="Symbol">:</a> <a id="7566" class="Symbol">∀{</a><a id="7568" href="plfa.part2.Confluence.html#7568" class="Bound">Γ</a> <a id="7570" href="plfa.part2.Confluence.html#7570" class="Bound">Δ</a><a id="7571" class="Symbol">}</a> <a id="7573" class="Symbol">→</a> <a id="7575" href="/19.08/Substitution/#2405" class="Function">Subst</a> <a id="7581" href="plfa.part2.Confluence.html#7568" class="Bound">Γ</a> <a id="7583" href="plfa.part2.Confluence.html#7570" class="Bound">Δ</a> <a id="7585" class="Symbol">→</a> <a id="7587" href="plfa.part2.Substitution.html#2405" class="Function">Subst</a> <a id="7593" href="plfa.part2.Confluence.html#7568" class="Bound">Γ</a> <a id="7595" href="plfa.part2.Confluence.html#7570" class="Bound">Δ</a> <a id="7597" class="Symbol">→</a> <a id="7599" class="PrimitiveType">Set</a>
<a id="7603" href="/19.08/Confluence/#7554" class="Function">par-subst</a> <a id="7613" class="Symbol">{</a><a id="7614" href="plfa.part2.Confluence.html#7614" class="Bound">Γ</a><a id="7615" class="Symbol">}{</a><a id="7617" href="plfa.part2.Confluence.html#7617" class="Bound">Δ</a><a id="7618" class="Symbol">}</a> <a id="7620" href="plfa.part2.Confluence.html#7620" class="Bound">σ</a> <a id="7622" href="plfa.part2.Confluence.html#7622" class="Bound">σ′</a> <a id="7625" class="Symbol">=</a> <a id="7627" class="Symbol">∀{</a><a id="7629" href="plfa.part2.Confluence.html#7629" class="Bound">A</a><a id="7630" class="Symbol">}{</a><a id="7632" href="plfa.part2.Confluence.html#7632" class="Bound">x</a> <a id="7634" class="Symbol">:</a> <a id="7636" href="plfa.part2.Confluence.html#7614" class="Bound">Γ</a> <a id="7638" href="/19.08/Untyped/#3521" class="Datatype Operator">∋</a> <a id="7640" href="plfa.part2.Confluence.html#7629" class="Bound">A</a><a id="7641" class="Symbol">}</a> <a id="7643" class="Symbol">→</a> <a id="7645" href="plfa.part2.Confluence.html#7620" class="Bound">σ</a> <a id="7647" href="plfa.part2.Confluence.html#7632" class="Bound">x</a> <a id="7649" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="7651" href="plfa.part2.Confluence.html#7622" class="Bound">σ′</a> <a id="7654" href="plfa.part2.Confluence.html#7632" 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="/19.08/Substitution/">Substitution</a>
and restate here.</p>
<pre class="Agda"><a id="rename-subst-commute"></a><a id="8084" href="/19.08/Confluence/#8084" class="Function">rename-subst-commute</a> <a id="8105" class="Symbol">:</a> <a id="8107" class="Symbol">∀{</a><a id="8109" href="plfa.part2.Confluence.html#8109" class="Bound">Γ</a> <a id="8111" href="plfa.part2.Confluence.html#8111" class="Bound">Δ</a><a id="8112" class="Symbol">}{</a><a id="8114" href="plfa.part2.Confluence.html#8114" class="Bound">N</a> <a id="8116" class="Symbol">:</a> <a id="8118" href="plfa.part2.Confluence.html#8109" class="Bound">Γ</a> <a id="8120" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="8122" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="8124" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="8126" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="8127" class="Symbol">}{</a><a id="8129" href="plfa.part2.Confluence.html#8129" class="Bound">M</a> <a id="8131" class="Symbol">:</a> <a id="8133" href="plfa.part2.Confluence.html#8109" class="Bound">Γ</a> <a id="8135" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="8137" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="8138" class="Symbol">}{</a><a id="8140" href="plfa.part2.Confluence.html#8140" class="Bound">ρ</a> <a id="8142" class="Symbol">:</a> <a id="8144" href="/19.08/Substitution/#2192" class="Function">Rename</a> <a id="8151" href="plfa.part2.Confluence.html#8109" class="Bound">Γ</a> <a id="8153" href="plfa.part2.Confluence.html#8111" class="Bound">Δ</a> <a id="8155" class="Symbol">}</a>
<a id="8161" class="Symbol">→</a> <a id="8163" class="Symbol">(</a><a id="8164" href="/19.08/Untyped/#6235" class="Function">rename</a> <a id="8171" class="Symbol">(</a><a id="8172" href="plfa.part2.Untyped.html#5925" class="Function">ext</a> <a id="8176" href="/19.08/Confluence/#8140" class="Bound">ρ</a><a id="8177" class="Symbol">)</a> <a id="8179" href="plfa.part2.Confluence.html#8114" class="Bound">N</a><a id="8180" class="Symbol">)</a> <a id="8182" href="plfa.part2.Untyped.html#7491" class="Function Operator">[</a> <a id="8184" href="plfa.part2.Untyped.html#6235" class="Function">rename</a> <a id="8191" href="plfa.part2.Confluence.html#8140" class="Bound">ρ</a> <a id="8193" href="plfa.part2.Confluence.html#8129" class="Bound">M</a> <a id="8195" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a> <a id="8197" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="8199" href="plfa.part2.Untyped.html#6235" class="Function">rename</a> <a id="8206" href="plfa.part2.Confluence.html#8140" class="Bound">ρ</a> <a id="8208" class="Symbol">(</a><a id="8209" href="plfa.part2.Confluence.html#8114" class="Bound">N</a> <a id="8211" href="plfa.part2.Untyped.html#7491" class="Function Operator">[</a> <a id="8213" href="plfa.part2.Confluence.html#8129" class="Bound">M</a> <a id="8215" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a><a id="8216" class="Symbol">)</a>
<a id="8218" href="/19.08/Confluence/#8084" class="Function">rename-subst-commute</a> <a id="8239" class="Symbol">{</a><a id="8240" class="Argument">N</a> <a id="8242" class="Symbol">=</a> <a id="8244" href="plfa.part2.Confluence.html#8244" class="Bound">N</a><a id="8245" class="Symbol">}</a> <a id="8247" class="Symbol">=</a> <a id="8249" href="/19.08/Substitution/#27953" class="Function">plfa.part2.Substitution.rename-subst-commute</a> <a id="8294" class="Symbol">{</a><a id="8295" class="Argument">N</a> <a id="8297" class="Symbol">=</a> <a id="8299" href="plfa.part2.Confluence.html#8244" class="Bound">N</a><a id="8300" 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="8344" href="/19.08/Confluence/#8344" class="Function">par-rename</a> <a id="8355" class="Symbol">:</a> <a id="8357" class="Symbol">∀{</a><a id="8359" href="plfa.part2.Confluence.html#8359" class="Bound">Γ</a> <a id="8361" href="plfa.part2.Confluence.html#8361" class="Bound">Δ</a> <a id="8363" href="plfa.part2.Confluence.html#8363" class="Bound">A</a><a id="8364" class="Symbol">}</a> <a id="8366" class="Symbol">{</a><a id="8367" href="plfa.part2.Confluence.html#8367" class="Bound">ρ</a> <a id="8369" class="Symbol">:</a> <a id="8371" href="/19.08/Substitution/#2192" class="Function">Rename</a> <a id="8378" href="plfa.part2.Confluence.html#8359" class="Bound">Γ</a> <a id="8380" href="plfa.part2.Confluence.html#8361" class="Bound">Δ</a><a id="8381" class="Symbol">}</a> <a id="8383" class="Symbol">{</a><a id="8384" href="plfa.part2.Confluence.html#8384" class="Bound">M</a> <a id="8386" href="plfa.part2.Confluence.html#8386" class="Bound">M′</a> <a id="8389" class="Symbol">:</a> <a id="8391" href="plfa.part2.Confluence.html#8359" class="Bound">Γ</a> <a id="8393" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="8395" href="plfa.part2.Confluence.html#8363" class="Bound">A</a><a id="8396" class="Symbol">}</a>
<a id="8400" class="Symbol">→</a> <a id="8402" href="/19.08/Confluence/#8384" class="Bound">M</a> <a id="8404" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="8406" href="plfa.part2.Confluence.html#8386" class="Bound">M′</a>
<a id="8413" class="Comment">------------------------</a>
<a id="8440" class="Symbol">→</a> <a id="8442" href="/19.08/Untyped/#6235" class="Function">rename</a> <a id="8449" href="/19.08/Confluence/#8367" class="Bound">ρ</a> <a id="8451" href="plfa.part2.Confluence.html#8384" class="Bound">M</a> <a id="8453" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="8455" href="plfa.part2.Untyped.html#6235" class="Function">rename</a> <a id="8462" href="plfa.part2.Confluence.html#8367" class="Bound">ρ</a> <a id="8464" href="plfa.part2.Confluence.html#8386" class="Bound">M′</a>
<a id="8467" href="/19.08/Confluence/#8344" class="Function">par-rename</a> <a id="8478" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a> <a id="8483" class="Symbol">=</a> <a id="8485" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a>
<a id="8490" href="/19.08/Confluence/#8344" class="Function">par-rename</a> <a id="8501" class="Symbol">(</a><a id="8502" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="8507" href="plfa.part2.Confluence.html#8507" class="Bound">p</a><a id="8508" class="Symbol">)</a> <a id="8510" class="Symbol">=</a> <a id="8512" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="8517" class="Symbol">(</a><a id="8518" href="plfa.part2.Confluence.html#8344" class="Function">par-rename</a> <a id="8529" href="plfa.part2.Confluence.html#8507" class="Bound">p</a><a id="8530" class="Symbol">)</a>
<a id="8532" href="/19.08/Confluence/#8344" class="Function">par-rename</a> <a id="8543" class="Symbol">(</a><a id="8544" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="8549" href="plfa.part2.Confluence.html#8549" class="Bound">p₁</a> <a id="8552" href="plfa.part2.Confluence.html#8552" class="Bound">p₂</a><a id="8554" class="Symbol">)</a> <a id="8556" class="Symbol">=</a> <a id="8558" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="8563" class="Symbol">(</a><a id="8564" href="plfa.part2.Confluence.html#8344" class="Function">par-rename</a> <a id="8575" href="plfa.part2.Confluence.html#8549" class="Bound">p₁</a><a id="8577" class="Symbol">)</a> <a id="8579" class="Symbol">(</a><a id="8580" href="plfa.part2.Confluence.html#8344" class="Function">par-rename</a> <a id="8591" href="plfa.part2.Confluence.html#8552" class="Bound">p₂</a><a id="8593" class="Symbol">)</a>
<a id="8595" href="/19.08/Confluence/#8344" class="Function">par-rename</a> <a id="8606" class="Symbol">{</a><a id="8607" href="plfa.part2.Confluence.html#8607" class="Bound">Γ</a><a id="8608" class="Symbol">}{</a><a id="8610" href="plfa.part2.Confluence.html#8610" class="Bound">Δ</a><a id="8611" class="Symbol">}{</a><a id="8613" href="plfa.part2.Confluence.html#8613" class="Bound">A</a><a id="8614" class="Symbol">}{</a><a id="8616" href="plfa.part2.Confluence.html#8616" class="Bound">ρ</a><a id="8617" class="Symbol">}</a> <a id="8619" class="Symbol">(</a><a id="8620" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a><a id="8625" class="Symbol">{</a><a id="8626" href="plfa.part2.Confluence.html#8607" class="Bound">Γ</a><a id="8627" class="Symbol">}{</a><a id="8629" href="plfa.part2.Confluence.html#8629" class="Bound">N</a><a id="8630" class="Symbol">}{</a><a id="8632" href="plfa.part2.Confluence.html#8632" class="Bound">N′</a><a id="8634" class="Symbol">}{</a><a id="8636" href="plfa.part2.Confluence.html#8636" class="Bound">M</a><a id="8637" class="Symbol">}{</a><a id="8639" href="plfa.part2.Confluence.html#8639" class="Bound">M′</a><a id="8641" class="Symbol">}</a> <a id="8643" href="plfa.part2.Confluence.html#8643" class="Bound">p₁</a> <a id="8646" href="plfa.part2.Confluence.html#8646" class="Bound">p₂</a><a id="8648" class="Symbol">)</a>
<a id="8654" class="Keyword">with</a> <a id="8659" href="/19.08/Confluence/#2936" class="InductiveConstructor">pbeta</a> <a id="8665" class="Symbol">(</a><a id="8666" href="plfa.part2.Confluence.html#8344" class="Function">par-rename</a><a id="8676" class="Symbol">{</a><a id="8677" class="Argument">ρ</a> <a id="8679" class="Symbol">=</a> <a id="8681" href="/19.08/Untyped/#5925" class="Function">ext</a> <a id="8685" href="plfa.part2.Confluence.html#8616" class="Bound">ρ</a><a id="8686" class="Symbol">}</a> <a id="8688" href="plfa.part2.Confluence.html#8643" class="Bound">p₁</a><a id="8690" class="Symbol">)</a> <a id="8692" class="Symbol">(</a><a id="8693" href="plfa.part2.Confluence.html#8344" class="Function">par-rename</a><a id="8703" class="Symbol">{</a><a id="8704" class="Argument">ρ</a> <a id="8706" class="Symbol">=</a> <a id="8708" href="plfa.part2.Confluence.html#8616" class="Bound">ρ</a><a id="8709" class="Symbol">}</a> <a id="8711" href="plfa.part2.Confluence.html#8646" class="Bound">p₂</a><a id="8713" class="Symbol">)</a>
<a id="8715" class="Symbol">...</a> <a id="8719" class="Symbol">|</a> <a id="8721" href="/19.08/Confluence/#8721" class="Bound">G</a> <a id="8723" class="Keyword">rewrite</a> <a id="8731" href="plfa.part2.Confluence.html#8084" class="Function">rename-subst-commute</a><a id="8751" class="Symbol">{</a><a id="8752" class="Bound">Γ</a><a id="8753" class="Symbol">}{</a><a id="8755" class="Bound">Δ</a><a id="8756" class="Symbol">}{</a><a id="8758" class="Bound">N′</a><a id="8760" class="Symbol">}{</a><a id="8762" class="Bound">M′</a><a id="8764" class="Symbol">}{</a><a id="8766" class="Bound">ρ</a><a id="8767" class="Symbol">}</a> <a id="8769" class="Symbol">=</a> <a id="8771" href="plfa.part2.Confluence.html#8721" 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="9499" href="/19.08/Confluence/#9499" class="Function">par-subst-exts</a> <a id="9514" class="Symbol">:</a> <a id="9516" class="Symbol">∀{</a><a id="9518" href="plfa.part2.Confluence.html#9518" class="Bound">Γ</a> <a id="9520" href="plfa.part2.Confluence.html#9520" class="Bound">Δ</a><a id="9521" class="Symbol">}</a> <a id="9523" class="Symbol">{</a><a id="9524" href="plfa.part2.Confluence.html#9524" class="Bound">σ</a> <a id="9526" href="plfa.part2.Confluence.html#9526" class="Bound">τ</a> <a id="9528" class="Symbol">:</a> <a id="9530" href="/19.08/Substitution/#2405" class="Function">Subst</a> <a id="9536" href="plfa.part2.Confluence.html#9518" class="Bound">Γ</a> <a id="9538" href="plfa.part2.Confluence.html#9520" class="Bound">Δ</a><a id="9539" class="Symbol">}</a>
<a id="9543" class="Symbol">→</a> <a id="9545" href="/19.08/Confluence/#7554" class="Function">par-subst</a> <a id="9555" href="plfa.part2.Confluence.html#9524" class="Bound">σ</a> <a id="9557" href="plfa.part2.Confluence.html#9526" class="Bound">τ</a>
<a id="9563" class="Comment">------------------------------------------</a>
<a id="9608" class="Symbol">→</a> <a id="9610" class="Symbol">∀{</a><a id="9612" href="/19.08/Confluence/#9612" class="Bound">B</a><a id="9613" class="Symbol">}</a> <a id="9615" class="Symbol">→</a> <a id="9617" href="plfa.part2.Confluence.html#7554" class="Function">par-subst</a> <a id="9627" class="Symbol">(</a><a id="9628" href="/19.08/Untyped/#6671" class="Function">exts</a> <a id="9633" href="plfa.part2.Confluence.html#9524" class="Bound">σ</a> <a id="9635" class="Symbol">{</a><a id="9636" class="Argument">B</a> <a id="9638" class="Symbol">=</a> <a id="9640" href="plfa.part2.Confluence.html#9612" class="Bound">B</a><a id="9641" class="Symbol">})</a> <a id="9644" class="Symbol">(</a><a id="9645" href="plfa.part2.Untyped.html#6671" class="Function">exts</a> <a id="9650" href="plfa.part2.Confluence.html#9526" class="Bound">τ</a><a id="9651" class="Symbol">)</a>
<a id="9653" href="/19.08/Confluence/#9499" class="Function">par-subst-exts</a> <a id="9668" href="plfa.part2.Confluence.html#9668" class="Bound">s</a> <a id="9670" class="Symbol">{</a><a id="9671" class="Argument">x</a> <a id="9673" class="Symbol">=</a> <a id="9675" href="/19.08/Untyped/#3557" class="InductiveConstructor">Z</a><a id="9676" class="Symbol">}</a> <a id="9678" class="Symbol">=</a> <a id="9680" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a>
<a id="9685" href="/19.08/Confluence/#9499" class="Function">par-subst-exts</a> <a id="9700" href="plfa.part2.Confluence.html#9700" class="Bound">s</a> <a id="9702" class="Symbol">{</a><a id="9703" class="Argument">x</a> <a id="9705" class="Symbol">=</a> <a id="9707" href="/19.08/Untyped/#3602" class="InductiveConstructor Operator">S</a> <a id="9709" href="plfa.part2.Confluence.html#9709" class="Bound">x</a><a id="9710" class="Symbol">}</a> <a id="9712" class="Symbol">=</a> <a id="9714" href="plfa.part2.Confluence.html#8344" class="Function">par-rename</a> <a id="9725" href="plfa.part2.Confluence.html#9700" 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="/19.08/Substitution/">Substitution</a>
and restate it below.</p>
<pre class="Agda"><a id="subst-commute"></a><a id="10025" href="/19.08/Confluence/#10025" class="Function">subst-commute</a> <a id="10039" class="Symbol">:</a> <a id="10041" class="Symbol">∀{</a><a id="10043" href="plfa.part2.Confluence.html#10043" class="Bound">Γ</a> <a id="10045" href="plfa.part2.Confluence.html#10045" class="Bound">Δ</a><a id="10046" class="Symbol">}{</a><a id="10048" href="plfa.part2.Confluence.html#10048" class="Bound">N</a> <a id="10050" class="Symbol">:</a> <a id="10052" href="plfa.part2.Confluence.html#10043" class="Bound">Γ</a> <a id="10054" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="10056" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="10058" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="10060" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="10061" class="Symbol">}{</a><a id="10063" href="plfa.part2.Confluence.html#10063" class="Bound">M</a> <a id="10065" class="Symbol">:</a> <a id="10067" href="plfa.part2.Confluence.html#10043" class="Bound">Γ</a> <a id="10069" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="10071" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="10072" class="Symbol">}{</a><a id="10074" href="plfa.part2.Confluence.html#10074" class="Bound">σ</a> <a id="10076" class="Symbol">:</a> <a id="10078" href="/19.08/Substitution/#2405" class="Function">Subst</a> <a id="10084" href="plfa.part2.Confluence.html#10043" class="Bound">Γ</a> <a id="10086" href="plfa.part2.Confluence.html#10045" class="Bound">Δ</a> <a id="10088" class="Symbol">}</a>
<a id="10092" class="Symbol">→</a> <a id="10094" href="/19.08/Untyped/#6963" class="Function">subst</a> <a id="10100" class="Symbol">(</a><a id="10101" href="plfa.part2.Untyped.html#6671" class="Function">exts</a> <a id="10106" href="/19.08/Confluence/#10074" class="Bound">σ</a><a id="10107" class="Symbol">)</a> <a id="10109" href="plfa.part2.Confluence.html#10048" class="Bound">N</a> <a id="10111" href="plfa.part2.Untyped.html#7491" class="Function Operator">[</a> <a id="10113" href="plfa.part2.Untyped.html#6963" class="Function">subst</a> <a id="10119" href="plfa.part2.Confluence.html#10074" class="Bound">σ</a> <a id="10121" href="plfa.part2.Confluence.html#10063" class="Bound">M</a> <a id="10123" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a> <a id="10125" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="10127" href="plfa.part2.Untyped.html#6963" class="Function">subst</a> <a id="10133" href="plfa.part2.Confluence.html#10074" class="Bound">σ</a> <a id="10135" class="Symbol">(</a><a id="10136" href="plfa.part2.Confluence.html#10048" class="Bound">N</a> <a id="10138" href="plfa.part2.Untyped.html#7491" class="Function Operator">[</a> <a id="10140" href="plfa.part2.Confluence.html#10063" class="Bound">M</a> <a id="10142" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a><a id="10143" class="Symbol">)</a>
<a id="10145" href="/19.08/Confluence/#10025" class="Function">subst-commute</a> <a id="10159" class="Symbol">{</a><a id="10160" class="Argument">N</a> <a id="10162" class="Symbol">=</a> <a id="10164" href="plfa.part2.Confluence.html#10164" class="Bound">N</a><a id="10165" class="Symbol">}</a> <a id="10167" class="Symbol">=</a> <a id="10169" href="/19.08/Substitution/#26412" class="Function">plfa.part2.Substitution.subst-commute</a> <a id="10207" class="Symbol">{</a><a id="10208" class="Argument">N</a> <a id="10210" class="Symbol">=</a> <a id="10212" href="plfa.part2.Confluence.html#10164" class="Bound">N</a><a id="10213" 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="10294" href="/19.08/Confluence/#10294" class="Function">subst-par</a> <a id="10304" class="Symbol">:</a> <a id="10306" class="Symbol">∀{</a><a id="10308" href="plfa.part2.Confluence.html#10308" class="Bound">Γ</a> <a id="10310" href="plfa.part2.Confluence.html#10310" class="Bound">Δ</a> <a id="10312" href="plfa.part2.Confluence.html#10312" class="Bound">A</a><a id="10313" class="Symbol">}</a> <a id="10315" class="Symbol">{</a><a id="10316" href="plfa.part2.Confluence.html#10316" class="Bound">σ</a> <a id="10318" href="plfa.part2.Confluence.html#10318" class="Bound">τ</a> <a id="10320" class="Symbol">:</a> <a id="10322" href="/19.08/Substitution/#2405" class="Function">Subst</a> <a id="10328" href="plfa.part2.Confluence.html#10308" class="Bound">Γ</a> <a id="10330" href="plfa.part2.Confluence.html#10310" class="Bound">Δ</a><a id="10331" class="Symbol">}</a> <a id="10333" class="Symbol">{</a><a id="10334" href="plfa.part2.Confluence.html#10334" class="Bound">M</a> <a id="10336" href="plfa.part2.Confluence.html#10336" class="Bound">M′</a> <a id="10339" class="Symbol">:</a> <a id="10341" href="plfa.part2.Confluence.html#10308" class="Bound">Γ</a> <a id="10343" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="10345" href="plfa.part2.Confluence.html#10312" class="Bound">A</a><a id="10346" class="Symbol">}</a>
<a id="10350" class="Symbol">→</a> <a id="10352" href="/19.08/Confluence/#7554" class="Function">par-subst</a> <a id="10362" href="plfa.part2.Confluence.html#10316" class="Bound">σ</a> <a id="10364" href="plfa.part2.Confluence.html#10318" class="Bound">τ</a> <a id="10367" class="Symbol">→</a> <a id="10370" href="plfa.part2.Confluence.html#10334" class="Bound">M</a> <a id="10372" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="10374" href="plfa.part2.Confluence.html#10336" class="Bound">M′</a>
<a id="10381" class="Comment">--------------------------</a>
<a id="10410" class="Symbol">→</a> <a id="10412" href="/19.08/Untyped/#6963" class="Function">subst</a> <a id="10418" href="/19.08/Confluence/#10316" class="Bound">σ</a> <a id="10420" href="plfa.part2.Confluence.html#10334" class="Bound">M</a> <a id="10422" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="10424" href="plfa.part2.Untyped.html#6963" class="Function">subst</a> <a id="10430" href="plfa.part2.Confluence.html#10318" class="Bound">τ</a> <a id="10432" href="plfa.part2.Confluence.html#10336" class="Bound">M′</a>
<a id="10435" href="/19.08/Confluence/#10294" class="Function">subst-par</a> <a id="10445" class="Symbol">{</a><a id="10446" href="plfa.part2.Confluence.html#10446" class="Bound">Γ</a><a id="10447" class="Symbol">}</a> <a id="10449" class="Symbol">{</a><a id="10450" href="plfa.part2.Confluence.html#10450" class="Bound">Δ</a><a id="10451" class="Symbol">}</a> <a id="10453" class="Symbol">{</a><a id="10454" href="plfa.part2.Confluence.html#10454" class="Bound">A</a><a id="10455" class="Symbol">}</a> <a id="10457" class="Symbol">{</a><a id="10458" href="plfa.part2.Confluence.html#10458" class="Bound">σ</a><a id="10459" class="Symbol">}</a> <a id="10461" class="Symbol">{</a><a id="10462" href="plfa.part2.Confluence.html#10462" class="Bound">τ</a><a id="10463" class="Symbol">}</a> <a id="10465" class="Symbol">{</a><a id="10466" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="10468" href="plfa.part2.Confluence.html#10468" class="Bound">x</a><a id="10469" class="Symbol">}</a> <a id="10471" href="plfa.part2.Confluence.html#10471" class="Bound">s</a> <a id="10473" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a> <a id="10478" class="Symbol">=</a> <a id="10480" href="plfa.part2.Confluence.html#10471" class="Bound">s</a>
<a id="10482" href="/19.08/Confluence/#10294" class="Function">subst-par</a> <a id="10492" class="Symbol">{</a><a id="10493" href="plfa.part2.Confluence.html#10493" class="Bound">Γ</a><a id="10494" class="Symbol">}</a> <a id="10496" class="Symbol">{</a><a id="10497" href="plfa.part2.Confluence.html#10497" class="Bound">Δ</a><a id="10498" class="Symbol">}</a> <a id="10500" class="Symbol">{</a><a id="10501" href="plfa.part2.Confluence.html#10501" class="Bound">A</a><a id="10502" class="Symbol">}</a> <a id="10504" class="Symbol">{</a><a id="10505" href="plfa.part2.Confluence.html#10505" class="Bound">σ</a><a id="10506" class="Symbol">}</a> <a id="10508" class="Symbol">{</a><a id="10509" href="plfa.part2.Confluence.html#10509" class="Bound">τ</a><a id="10510" class="Symbol">}</a> <a id="10512" class="Symbol">{</a><a id="10513" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="10515" href="plfa.part2.Confluence.html#10515" class="Bound">N</a><a id="10516" class="Symbol">}</a> <a id="10518" href="plfa.part2.Confluence.html#10518" class="Bound">s</a> <a id="10520" class="Symbol">(</a><a id="10521" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="10526" href="plfa.part2.Confluence.html#10526" class="Bound">p</a><a id="10527" class="Symbol">)</a> <a id="10529" class="Symbol">=</a>
<a id="10533" href="/19.08/Confluence/#2750" class="InductiveConstructor">pabs</a> <a id="10538" class="Symbol">(</a><a id="10539" href="plfa.part2.Confluence.html#10294" class="Function">subst-par</a> <a id="10549" class="Symbol">{</a><a id="10550" class="Argument">σ</a> <a id="10552" class="Symbol">=</a> <a id="10554" href="/19.08/Untyped/#6671" class="Function">exts</a> <a id="10559" href="plfa.part2.Confluence.html#10505" class="Bound">σ</a><a id="10560" class="Symbol">}</a> <a id="10562" class="Symbol">{</a><a id="10563" class="Argument">τ</a> <a id="10565" class="Symbol">=</a> <a id="10567" href="plfa.part2.Untyped.html#6671" class="Function">exts</a> <a id="10572" href="plfa.part2.Confluence.html#10509" class="Bound">τ</a><a id="10573" class="Symbol">}</a>
<a id="10583" class="Symbol">(λ</a> <a id="10586" class="Symbol">{</a><a id="10587" href="/19.08/Confluence/#10587" class="Bound">A</a><a id="10588" class="Symbol">}{</a><a id="10590" href="plfa.part2.Confluence.html#10590" class="Bound">x</a><a id="10591" class="Symbol">}</a> <a id="10593" class="Symbol">→</a> <a id="10595" href="plfa.part2.Confluence.html#9499" class="Function">par-subst-exts</a> <a id="10610" href="plfa.part2.Confluence.html#10518" class="Bound">s</a> <a id="10612" class="Symbol">{</a><a id="10613" class="Argument">x</a> <a id="10615" class="Symbol">=</a> <a id="10617" href="plfa.part2.Confluence.html#10590" class="Bound">x</a><a id="10618" class="Symbol">})</a> <a id="10621" href="plfa.part2.Confluence.html#10526" class="Bound">p</a><a id="10622" class="Symbol">)</a>
<a id="10624" href="/19.08/Confluence/#10294" class="Function">subst-par</a> <a id="10634" class="Symbol">{</a><a id="10635" href="plfa.part2.Confluence.html#10635" class="Bound">Γ</a><a id="10636" class="Symbol">}</a> <a id="10638" class="Symbol">{</a><a id="10639" href="plfa.part2.Confluence.html#10639" class="Bound">Δ</a><a id="10640" class="Symbol">}</a> <a id="10642" class="Symbol">{</a><a id="10643" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="10644" class="Symbol">}</a> <a id="10646" class="Symbol">{</a><a id="10647" href="plfa.part2.Confluence.html#10647" class="Bound">σ</a><a id="10648" class="Symbol">}</a> <a id="10650" class="Symbol">{</a><a id="10651" href="plfa.part2.Confluence.html#10651" class="Bound">τ</a><a id="10652" class="Symbol">}</a> <a id="10654" class="Symbol">{</a><a id="10655" href="plfa.part2.Confluence.html#10655" class="Bound">L</a> <a id="10657" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="10659" href="plfa.part2.Confluence.html#10659" class="Bound">M</a><a id="10660" class="Symbol">}</a> <a id="10662" href="plfa.part2.Confluence.html#10662" class="Bound">s</a> <a id="10664" class="Symbol">(</a><a id="10665" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="10670" href="plfa.part2.Confluence.html#10670" class="Bound">p₁</a> <a id="10673" href="plfa.part2.Confluence.html#10673" class="Bound">p₂</a><a id="10675" class="Symbol">)</a> <a id="10677" class="Symbol">=</a>
<a id="10681" href="/19.08/Confluence/#2830" class="InductiveConstructor">papp</a> <a id="10686" class="Symbol">(</a><a id="10687" href="plfa.part2.Confluence.html#10294" class="Function">subst-par</a> <a id="10697" href="plfa.part2.Confluence.html#10662" class="Bound">s</a> <a id="10699" href="plfa.part2.Confluence.html#10670" class="Bound">p₁</a><a id="10701" class="Symbol">)</a> <a id="10703" class="Symbol">(</a><a id="10704" href="plfa.part2.Confluence.html#10294" class="Function">subst-par</a> <a id="10714" href="plfa.part2.Confluence.html#10662" class="Bound">s</a> <a id="10716" href="plfa.part2.Confluence.html#10673" class="Bound">p₂</a><a id="10718" class="Symbol">)</a>
<a id="10720" href="/19.08/Confluence/#10294" class="Function">subst-par</a> <a id="10730" class="Symbol">{</a><a id="10731" href="plfa.part2.Confluence.html#10731" class="Bound">Γ</a><a id="10732" class="Symbol">}</a> <a id="10734" class="Symbol">{</a><a id="10735" href="plfa.part2.Confluence.html#10735" class="Bound">Δ</a><a id="10736" class="Symbol">}</a> <a id="10738" class="Symbol">{</a><a id="10739" href="/19.08/Untyped/#2888" class="InductiveConstructor">★</a><a id="10740" class="Symbol">}</a> <a id="10742" class="Symbol">{</a><a id="10743" href="plfa.part2.Confluence.html#10743" class="Bound">σ</a><a id="10744" class="Symbol">}</a> <a id="10746" class="Symbol">{</a><a id="10747" href="plfa.part2.Confluence.html#10747" class="Bound">τ</a><a id="10748" class="Symbol">}</a> <a id="10750" class="Symbol">{(</a><a id="10752" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="10754" href="plfa.part2.Confluence.html#10754" class="Bound">N</a><a id="10755" class="Symbol">)</a> <a id="10757" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">·</a> <a id="10759" href="plfa.part2.Confluence.html#10759" class="Bound">M</a><a id="10760" class="Symbol">}</a> <a id="10762" href="plfa.part2.Confluence.html#10762" class="Bound">s</a> <a id="10764" class="Symbol">(</a><a id="10765" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a><a id="10770" class="Symbol">{</a><a id="10771" class="Argument">N′</a> <a id="10774" class="Symbol">=</a> <a id="10776" href="plfa.part2.Confluence.html#10776" class="Bound">N′</a><a id="10778" class="Symbol">}{</a><a id="10780" class="Argument">M′</a> <a id="10783" class="Symbol">=</a> <a id="10785" href="plfa.part2.Confluence.html#10785" class="Bound">M′</a><a id="10787" class="Symbol">}</a> <a id="10789" href="plfa.part2.Confluence.html#10789" class="Bound">p₁</a> <a id="10792" href="plfa.part2.Confluence.html#10792" class="Bound">p₂</a><a id="10794" class="Symbol">)</a>
<a id="10800" class="Keyword">with</a> <a id="10805" href="/19.08/Confluence/#2936" class="InductiveConstructor">pbeta</a> <a id="10811" class="Symbol">(</a><a id="10812" href="plfa.part2.Confluence.html#10294" class="Function">subst-par</a><a id="10821" class="Symbol">{</a><a id="10822" class="Argument">σ</a> <a id="10824" class="Symbol">=</a> <a id="10826" href="/19.08/Untyped/#6671" class="Function">exts</a> <a id="10831" href="plfa.part2.Confluence.html#10743" class="Bound">σ</a><a id="10832" class="Symbol">}{</a><a id="10834" class="Argument">τ</a> <a id="10836" class="Symbol">=</a> <a id="10838" href="plfa.part2.Untyped.html#6671" class="Function">exts</a> <a id="10843" href="plfa.part2.Confluence.html#10747" class="Bound">τ</a><a id="10844" class="Symbol">}{</a><a id="10846" class="Argument">M</a> <a id="10848" class="Symbol">=</a> <a id="10850" href="plfa.part2.Confluence.html#10754" class="Bound">N</a><a id="10851" class="Symbol">}</a>
<a id="10877" class="Symbol">(λ{</a><a id="10880" href="/19.08/Confluence/#10880" class="Bound">A</a><a id="10881" class="Symbol">}{</a><a id="10883" href="plfa.part2.Confluence.html#10883" class="Bound">x</a><a id="10884" class="Symbol">}</a> <a id="10886" class="Symbol">→</a> <a id="10888" href="plfa.part2.Confluence.html#9499" class="Function">par-subst-exts</a> <a id="10903" href="plfa.part2.Confluence.html#10762" class="Bound">s</a> <a id="10905" class="Symbol">{</a><a id="10906" class="Argument">x</a> <a id="10908" class="Symbol">=</a> <a id="10910" href="plfa.part2.Confluence.html#10883" class="Bound">x</a><a id="10911" class="Symbol">})</a> <a id="10914" href="plfa.part2.Confluence.html#10789" class="Bound">p₁</a><a id="10916" class="Symbol">)</a>
<a id="10933" class="Symbol">(</a><a id="10934" href="/19.08/Confluence/#10294" class="Function">subst-par</a> <a id="10944" class="Symbol">{</a><a id="10945" class="Argument">σ</a> <a id="10947" class="Symbol">=</a> <a id="10949" href="plfa.part2.Confluence.html#10743" class="Bound">σ</a><a id="10950" class="Symbol">}</a> <a id="10952" href="plfa.part2.Confluence.html#10762" class="Bound">s</a> <a id="10954" href="plfa.part2.Confluence.html#10792" class="Bound">p₂</a><a id="10956" class="Symbol">)</a>
<a id="10958" class="Symbol">...</a> <a id="10962" class="Symbol">|</a> <a id="10964" href="/19.08/Confluence/#10964" class="Bound">G</a> <a id="10966" class="Keyword">rewrite</a> <a id="10974" href="plfa.part2.Confluence.html#10025" class="Function">subst-commute</a><a id="10987" class="Symbol">{</a><a id="10988" class="Argument">N</a> <a id="10990" class="Symbol">=</a> <a id="10992" class="Bound">N′</a><a id="10994" class="Symbol">}{</a><a id="10996" class="Argument">M</a> <a id="10998" class="Symbol">=</a> <a id="11000" class="Bound">M′</a><a id="11002" class="Symbol">}{</a><a id="11004" class="Argument">σ</a> <a id="11006" class="Symbol">=</a> <a id="11008" class="Bound">τ</a><a id="11009" class="Symbol">}</a> <a id="11011" class="Symbol">=</a> <a id="11013" href="plfa.part2.Confluence.html#10964" 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="12221" href="/19.08/Confluence/#12221" class="Function">par-subst-zero</a> <a id="12236" class="Symbol">:</a> <a id="12238" class="Symbol">∀{</a><a id="12240" href="plfa.part2.Confluence.html#12240" class="Bound">Γ</a><a id="12241" class="Symbol">}{</a><a id="12243" href="plfa.part2.Confluence.html#12243" class="Bound">A</a><a id="12244" class="Symbol">}{</a><a id="12246" href="plfa.part2.Confluence.html#12246" class="Bound">M</a> <a id="12248" href="plfa.part2.Confluence.html#12248" class="Bound">M′</a> <a id="12251" class="Symbol">:</a> <a id="12253" href="plfa.part2.Confluence.html#12240" class="Bound">Γ</a> <a id="12255" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="12257" href="plfa.part2.Confluence.html#12243" class="Bound">A</a><a id="12258" class="Symbol">}</a>
<a id="12267" class="Symbol">→</a> <a id="12269" href="/19.08/Confluence/#12246" class="Bound">M</a> <a id="12271" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="12273" href="plfa.part2.Confluence.html#12248" class="Bound">M′</a>
<a id="12283" class="Symbol">→</a> <a id="12285" href="/19.08/Confluence/#7554" class="Function">par-subst</a> <a id="12295" class="Symbol">(</a><a id="12296" href="/19.08/Untyped/#7375" class="Function">subst-zero</a> <a id="12307" href="plfa.part2.Confluence.html#12246" class="Bound">M</a><a id="12308" class="Symbol">)</a> <a id="12310" class="Symbol">(</a><a id="12311" href="plfa.part2.Untyped.html#7375" class="Function">subst-zero</a> <a id="12322" href="plfa.part2.Confluence.html#12248" class="Bound">M′</a><a id="12324" class="Symbol">)</a>
<a id="12326" href="/19.08/Confluence/#12221" class="Function">par-subst-zero</a> <a id="12341" class="Symbol">{</a><a id="12342" href="plfa.part2.Confluence.html#12342" class="Bound">M</a><a id="12343" class="Symbol">}</a> <a id="12345" class="Symbol">{</a><a id="12346" href="plfa.part2.Confluence.html#12346" class="Bound">M′</a><a id="12348" class="Symbol">}</a> <a id="12350" href="plfa.part2.Confluence.html#12350" class="Bound">p</a> <a id="12352" class="Symbol">{</a><a id="12353" href="plfa.part2.Confluence.html#12353" class="Bound">A</a><a id="12354" class="Symbol">}</a> <a id="12356" class="Symbol">{</a><a id="12357" href="/19.08/Untyped/#3557" class="InductiveConstructor">Z</a><a id="12358" class="Symbol">}</a> <a id="12360" class="Symbol">=</a> <a id="12362" href="plfa.part2.Confluence.html#12350" class="Bound">p</a>
<a id="12364" href="/19.08/Confluence/#12221" class="Function">par-subst-zero</a> <a id="12379" class="Symbol">{</a><a id="12380" href="plfa.part2.Confluence.html#12380" class="Bound">M</a><a id="12381" class="Symbol">}</a> <a id="12383" class="Symbol">{</a><a id="12384" href="plfa.part2.Confluence.html#12384" class="Bound">M′</a><a id="12386" class="Symbol">}</a> <a id="12388" href="plfa.part2.Confluence.html#12388" class="Bound">p</a> <a id="12390" class="Symbol">{</a><a id="12391" href="plfa.part2.Confluence.html#12391" class="Bound">A</a><a id="12392" class="Symbol">}</a> <a id="12394" class="Symbol">{</a><a id="12395" href="/19.08/Untyped/#3602" class="InductiveConstructor Operator">S</a> <a id="12397" href="plfa.part2.Confluence.html#12397" class="Bound">x</a><a id="12398" class="Symbol">}</a> <a id="12400" class="Symbol">=</a> <a id="12402" href="plfa.part2.Confluence.html#2686" 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="12517" href="/19.08/Confluence/#12517" class="Function">sub-par</a> <a id="12525" class="Symbol">:</a> <a id="12527" class="Symbol">∀{</a><a id="12529" href="plfa.part2.Confluence.html#12529" class="Bound">Γ</a> <a id="12531" href="plfa.part2.Confluence.html#12531" class="Bound">A</a> <a id="12533" href="plfa.part2.Confluence.html#12533" class="Bound">B</a><a id="12534" class="Symbol">}</a> <a id="12536" class="Symbol">{</a><a id="12537" href="plfa.part2.Confluence.html#12537" class="Bound">N</a> <a id="12539" href="plfa.part2.Confluence.html#12539" class="Bound">N′</a> <a id="12542" class="Symbol">:</a> <a id="12544" href="plfa.part2.Confluence.html#12529" class="Bound">Γ</a> <a id="12546" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="12548" href="plfa.part2.Confluence.html#12531" class="Bound">A</a> <a id="12550" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="12552" href="plfa.part2.Confluence.html#12533" class="Bound">B</a><a id="12553" class="Symbol">}</a> <a id="12555" class="Symbol">{</a><a id="12556" href="plfa.part2.Confluence.html#12556" class="Bound">M</a> <a id="12558" href="plfa.part2.Confluence.html#12558" class="Bound">M′</a> <a id="12561" class="Symbol">:</a> <a id="12563" href="plfa.part2.Confluence.html#12529" class="Bound">Γ</a> <a id="12565" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="12567" href="plfa.part2.Confluence.html#12531" class="Bound">A</a><a id="12568" class="Symbol">}</a>
<a id="12572" class="Symbol">→</a> <a id="12574" href="/19.08/Confluence/#12537" class="Bound">N</a> <a id="12576" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="12578" href="plfa.part2.Confluence.html#12539" class="Bound">N′</a>
<a id="12583" class="Symbol">→</a> <a id="12585" href="/19.08/Confluence/#12556" class="Bound">M</a> <a id="12587" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="12589" href="plfa.part2.Confluence.html#12558" class="Bound">M′</a>
<a id="12596" class="Comment">--------------------------</a>
<a id="12625" class="Symbol">→</a> <a id="12627" href="/19.08/Confluence/#12537" class="Bound">N</a> <a id="12629" href="/19.08/Untyped/#7491" class="Function Operator">[</a> <a id="12631" href="plfa.part2.Confluence.html#12556" class="Bound">M</a> <a id="12633" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a> <a id="12635" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="12637" href="plfa.part2.Confluence.html#12539" class="Bound">N′</a> <a id="12640" href="plfa.part2.Untyped.html#7491" class="Function Operator">[</a> <a id="12642" href="plfa.part2.Confluence.html#12558" class="Bound">M′</a> <a id="12645" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a>
<a id="12647" href="/19.08/Confluence/#12517" class="Function">sub-par</a> <a id="12655" href="plfa.part2.Confluence.html#12655" class="Bound">pn</a> <a id="12658" href="plfa.part2.Confluence.html#12658" class="Bound">pm</a> <a id="12661" class="Symbol">=</a> <a id="12663" href="plfa.part2.Confluence.html#10294" class="Function">subst-par</a> <a id="12673" class="Symbol">(</a><a id="12674" href="plfa.part2.Confluence.html#12221" class="Function">par-subst-zero</a> <a id="12689" href="plfa.part2.Confluence.html#12658" class="Bound">pm</a><a id="12691" class="Symbol">)</a> <a id="12693" href="plfa.part2.Confluence.html#12655" 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="13046" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13058" class="Symbol">:</a> <a id="13060" class="Symbol">∀{</a><a id="13062" href="plfa.part2.Confluence.html#13062" class="Bound">Γ</a> <a id="13064" href="plfa.part2.Confluence.html#13064" class="Bound">A</a><a id="13065" class="Symbol">}</a> <a id="13067" class="Symbol">{</a><a id="13068" href="plfa.part2.Confluence.html#13068" class="Bound">M</a> <a id="13070" href="plfa.part2.Confluence.html#13070" class="Bound">N</a> <a id="13072" href="plfa.part2.Confluence.html#13072" class="Bound">N′</a> <a id="13075" class="Symbol">:</a> <a id="13077" href="plfa.part2.Confluence.html#13062" class="Bound">Γ</a> <a id="13079" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="13081" href="plfa.part2.Confluence.html#13064" class="Bound">A</a><a id="13082" class="Symbol">}</a>
<a id="13086" class="Symbol">→</a> <a id="13088" href="/19.08/Confluence/#13068" class="Bound">M</a> <a id="13090" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="13092" href="plfa.part2.Confluence.html#13070" class="Bound">N</a>
<a id="13096" class="Symbol">→</a> <a id="13098" href="/19.08/Confluence/#13068" class="Bound">M</a> <a id="13100" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="13102" href="plfa.part2.Confluence.html#13072" class="Bound">N′</a>
<a id="13109" class="Comment">---------------------------------</a>
<a id="13145" class="Symbol">→</a> <a id="13147" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="13150" href="/19.08/Confluence/#13150" class="Bound">L</a> <a id="13152" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="13154" href="plfa.part2.Confluence.html#13062" class="Bound">Γ</a> <a id="13156" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="13158" href="plfa.part2.Confluence.html#13064" class="Bound">A</a> <a id="13160" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="13162" class="Symbol">(</a><a id="13163" href="plfa.part2.Confluence.html#13070" class="Bound">N</a> <a id="13165" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="13167" href="plfa.part2.Confluence.html#13150" class="Bound">L</a><a id="13168" class="Symbol">)</a> <a id="13170" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="13172" class="Symbol">(</a><a id="13173" href="plfa.part2.Confluence.html#13072" class="Bound">N′</a> <a id="13176" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="13178" href="plfa.part2.Confluence.html#13150" class="Bound">L</a><a id="13179" class="Symbol">)</a>
<a id="13181" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13193" class="Symbol">(</a><a id="13194" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a><a id="13198" class="Symbol">{</a><a id="13199" class="Argument">x</a> <a id="13201" class="Symbol">=</a> <a id="13203" href="plfa.part2.Confluence.html#13203" class="Bound">x</a><a id="13204" class="Symbol">})</a> <a id="13207" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a> <a id="13212" class="Symbol">=</a> <a id="13214" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13216" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="13218" href="plfa.part2.Confluence.html#13203" class="Bound">x</a> <a id="13220" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13222" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13224" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a> <a id="13229" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13231" href="plfa.part2.Confluence.html#2686" class="InductiveConstructor">pvar</a> <a id="13236" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13238" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="13240" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13252" class="Symbol">(</a><a id="13253" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="13258" href="plfa.part2.Confluence.html#13258" class="Bound">p1</a><a id="13260" class="Symbol">)</a> <a id="13262" class="Symbol">(</a><a id="13263" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="13268" href="plfa.part2.Confluence.html#13268" class="Bound">p2</a><a id="13270" class="Symbol">)</a>
<a id="13276" class="Keyword">with</a> <a id="13281" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13293" href="plfa.part2.Confluence.html#13258" class="Bound">p1</a> <a id="13296" href="plfa.part2.Confluence.html#13268" class="Bound">p2</a>
<a id="13299" class="Symbol">...</a> <a id="13303" class="Symbol">|</a> <a id="13305" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13307" href="/19.08/Confluence/#13307" class="Bound">L′</a> <a id="13310" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13312" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13314" href="plfa.part2.Confluence.html#13314" class="Bound">p3</a> <a id="13317" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13319" href="plfa.part2.Confluence.html#13319" class="Bound">p4</a> <a id="13322" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13324" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13326" class="Symbol">=</a>
<a id="13334" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13336" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="13338" href="/19.08/Confluence/#13307" class="Bound">L′</a> <a id="13341" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13343" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13345" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="13350" href="plfa.part2.Confluence.html#13314" class="Bound">p3</a> <a id="13353" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13355" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="13360" href="plfa.part2.Confluence.html#13319" class="Bound">p4</a> <a id="13363" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13365" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="13367" href="/19.08/Confluence/#13046" class="Function">par-diamond</a><a id="13378" class="Symbol">{</a><a id="13379" href="plfa.part2.Confluence.html#13379" class="Bound">Γ</a><a id="13380" class="Symbol">}{</a><a id="13382" href="plfa.part2.Confluence.html#13382" class="Bound">A</a><a id="13383" class="Symbol">}{</a><a id="13385" href="plfa.part2.Confluence.html#13385" class="Bound">L</a> <a id="13387" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="13389" href="plfa.part2.Confluence.html#13389" class="Bound">M</a><a id="13390" class="Symbol">}{</a><a id="13392" href="plfa.part2.Confluence.html#13392" class="Bound">N</a><a id="13393" class="Symbol">}{</a><a id="13395" href="plfa.part2.Confluence.html#13395" class="Bound">N′</a><a id="13397" class="Symbol">}</a> <a id="13399" class="Symbol">(</a><a id="13400" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a><a id="13404" class="Symbol">{</a><a id="13405" href="plfa.part2.Confluence.html#13379" class="Bound">Γ</a><a id="13406" class="Symbol">}{</a><a id="13408" href="plfa.part2.Confluence.html#13385" class="Bound">L</a><a id="13409" class="Symbol">}{</a><a id="13411" href="plfa.part2.Confluence.html#13411" class="Bound">L₁</a><a id="13413" class="Symbol">}{</a><a id="13415" href="plfa.part2.Confluence.html#13389" class="Bound">M</a><a id="13416" class="Symbol">}{</a><a id="13418" href="plfa.part2.Confluence.html#13418" class="Bound">M₁</a><a id="13420" class="Symbol">}</a> <a id="13422" href="plfa.part2.Confluence.html#13422" class="Bound">p1</a> <a id="13425" href="plfa.part2.Confluence.html#13425" class="Bound">p3</a><a id="13427" class="Symbol">)</a>
<a id="13461" class="Symbol">(</a><a id="13462" href="/19.08/Confluence/#2830" class="InductiveConstructor">papp</a><a id="13466" class="Symbol">{</a><a id="13467" href="plfa.part2.Confluence.html#13379" class="Bound">Γ</a><a id="13468" class="Symbol">}{</a><a id="13470" href="plfa.part2.Confluence.html#13385" class="Bound">L</a><a id="13471" class="Symbol">}{</a><a id="13473" href="plfa.part2.Confluence.html#13473" class="Bound">L₂</a><a id="13475" class="Symbol">}{</a><a id="13477" href="plfa.part2.Confluence.html#13389" class="Bound">M</a><a id="13478" class="Symbol">}{</a><a id="13480" href="plfa.part2.Confluence.html#13480" class="Bound">M₂</a><a id="13482" class="Symbol">}</a> <a id="13484" href="plfa.part2.Confluence.html#13484" class="Bound">p2</a> <a id="13487" href="plfa.part2.Confluence.html#13487" class="Bound">p4</a><a id="13489" class="Symbol">)</a>
<a id="13495" class="Keyword">with</a> <a id="13500" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13512" href="plfa.part2.Confluence.html#13422" class="Bound">p1</a> <a id="13515" href="plfa.part2.Confluence.html#13484" class="Bound">p2</a>
<a id="13518" class="Symbol">...</a> <a id="13522" class="Symbol">|</a> <a id="13524" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13526" href="/19.08/Confluence/#13526" class="Bound">L₃</a> <a id="13529" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13531" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13533" href="plfa.part2.Confluence.html#13533" class="Bound">p5</a> <a id="13536" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13538" href="plfa.part2.Confluence.html#13538" class="Bound">p6</a> <a id="13541" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13543" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="13551" class="Keyword">with</a> <a id="13556" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13568" class="Bound">p3</a> <a id="13571" class="Bound">p4</a>
<a id="13574" class="Symbol">...</a> <a id="13580" class="Symbol">|</a> <a id="13582" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13584" href="/19.08/Confluence/#13584" class="Bound">M₃</a> <a id="13587" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13589" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13591" href="plfa.part2.Confluence.html#13591" class="Bound">p7</a> <a id="13594" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13596" href="plfa.part2.Confluence.html#13596" class="Bound">p8</a> <a id="13599" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13601" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13603" class="Symbol">=</a>
<a id="13613" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13615" class="Symbol">(</a><a id="13616" class="Bound">L₃</a> <a id="13619" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="13621" href="/19.08/Confluence/#13584" class="Bound">M₃</a><a id="13623" class="Symbol">)</a> <a id="13625" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13627" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13629" class="Symbol">(</a><a id="13630" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="13635" class="Bound">p5</a> <a id="13638" href="plfa.part2.Confluence.html#13591" class="Bound">p7</a><a id="13640" class="Symbol">)</a> <a id="13642" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13644" class="Symbol">(</a><a id="13645" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="13650" class="Bound">p6</a> <a id="13653" href="plfa.part2.Confluence.html#13596" class="Bound">p8</a><a id="13655" class="Symbol">)</a> <a id="13657" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13659" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="13661" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13673" class="Symbol">(</a><a id="13674" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="13679" class="Symbol">(</a><a id="13680" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="13685" href="plfa.part2.Confluence.html#13685" class="Bound">p1</a><a id="13687" class="Symbol">)</a> <a id="13689" href="plfa.part2.Confluence.html#13689" class="Bound">p3</a><a id="13691" class="Symbol">)</a> <a id="13693" class="Symbol">(</a><a id="13694" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a> <a id="13700" href="plfa.part2.Confluence.html#13700" class="Bound">p2</a> <a id="13703" href="plfa.part2.Confluence.html#13703" class="Bound">p4</a><a id="13705" class="Symbol">)</a>
<a id="13711" class="Keyword">with</a> <a id="13716" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13728" href="plfa.part2.Confluence.html#13685" class="Bound">p1</a> <a id="13731" href="plfa.part2.Confluence.html#13700" class="Bound">p2</a>
<a id="13734" class="Symbol">...</a> <a id="13738" class="Symbol">|</a> <a id="13740" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13742" href="/19.08/Confluence/#13742" class="Bound">N₃</a> <a id="13745" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13747" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13749" href="plfa.part2.Confluence.html#13749" class="Bound">p5</a> <a id="13752" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13754" href="plfa.part2.Confluence.html#13754" class="Bound">p6</a> <a id="13757" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13759" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="13767" class="Keyword">with</a> <a id="13772" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13784" class="Bound">p3</a> <a id="13787" class="Bound">p4</a>
<a id="13790" class="Symbol">...</a> <a id="13796" class="Symbol">|</a> <a id="13798" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13800" href="/19.08/Confluence/#13800" class="Bound">M₃</a> <a id="13803" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13805" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13807" href="plfa.part2.Confluence.html#13807" class="Bound">p7</a> <a id="13810" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13812" href="plfa.part2.Confluence.html#13812" class="Bound">p8</a> <a id="13815" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13817" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13819" class="Symbol">=</a>
<a id="13829" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13831" class="Bound">N₃</a> <a id="13834" href="/19.08/Untyped/#7491" class="Function Operator">[</a> <a id="13836" href="/19.08/Confluence/#13800" class="Bound">M₃</a> <a id="13839" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a> <a id="13841" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13843" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13845" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a> <a id="13851" class="Bound">p5</a> <a id="13854" href="plfa.part2.Confluence.html#13807" class="Bound">p7</a> <a id="13857" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13859" href="plfa.part2.Confluence.html#12517" class="Function">sub-par</a> <a id="13867" class="Bound">p6</a> <a id="13870" href="plfa.part2.Confluence.html#13812" class="Bound">p8</a> <a id="13873" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13875" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="13877" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13889" class="Symbol">(</a><a id="13890" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a> <a id="13896" href="plfa.part2.Confluence.html#13896" class="Bound">p1</a> <a id="13899" href="plfa.part2.Confluence.html#13899" class="Bound">p3</a><a id="13901" class="Symbol">)</a> <a id="13903" class="Symbol">(</a><a id="13904" href="plfa.part2.Confluence.html#2830" class="InductiveConstructor">papp</a> <a id="13909" class="Symbol">(</a><a id="13910" href="plfa.part2.Confluence.html#2750" class="InductiveConstructor">pabs</a> <a id="13915" href="plfa.part2.Confluence.html#13915" class="Bound">p2</a><a id="13917" class="Symbol">)</a> <a id="13919" href="plfa.part2.Confluence.html#13919" class="Bound">p4</a><a id="13921" class="Symbol">)</a>
<a id="13927" class="Keyword">with</a> <a id="13932" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="13944" href="plfa.part2.Confluence.html#13896" class="Bound">p1</a> <a id="13947" href="plfa.part2.Confluence.html#13915" class="Bound">p2</a>
<a id="13950" class="Symbol">...</a> <a id="13954" class="Symbol">|</a> <a id="13956" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13958" href="/19.08/Confluence/#13958" class="Bound">N₃</a> <a id="13961" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13963" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="13965" href="plfa.part2.Confluence.html#13965" class="Bound">p5</a> <a id="13968" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="13970" href="plfa.part2.Confluence.html#13970" class="Bound">p6</a> <a id="13973" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="13975" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="13983" class="Keyword">with</a> <a id="13988" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="14000" class="Bound">p3</a> <a id="14003" class="Bound">p4</a>
<a id="14006" class="Symbol">...</a> <a id="14012" class="Symbol">|</a> <a id="14014" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14016" href="/19.08/Confluence/#14016" class="Bound">M₃</a> <a id="14019" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14021" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14023" href="plfa.part2.Confluence.html#14023" class="Bound">p7</a> <a id="14026" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14028" href="plfa.part2.Confluence.html#14028" class="Bound">p8</a> <a id="14031" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14033" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14035" class="Symbol">=</a>
<a id="14045" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14047" class="Symbol">(</a><a id="14048" class="Bound">N₃</a> <a id="14051" href="/19.08/Untyped/#7491" class="Function Operator">[</a> <a id="14053" href="/19.08/Confluence/#14016" class="Bound">M₃</a> <a id="14056" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a><a id="14057" class="Symbol">)</a> <a id="14059" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14061" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14063" href="plfa.part2.Confluence.html#12517" class="Function">sub-par</a> <a id="14071" class="Bound">p5</a> <a id="14075" href="plfa.part2.Confluence.html#14023" class="Bound">p7</a> <a id="14078" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14080" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a> <a id="14086" class="Bound">p6</a> <a id="14089" href="plfa.part2.Confluence.html#14028" class="Bound">p8</a> <a id="14092" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14094" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="14096" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="14108" class="Symbol">{</a><a id="14109" href="plfa.part2.Confluence.html#14109" class="Bound">Γ</a><a id="14110" class="Symbol">}{</a><a id="14112" href="plfa.part2.Confluence.html#14112" class="Bound">A</a><a id="14113" class="Symbol">}</a> <a id="14115" class="Symbol">(</a><a id="14116" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a> <a id="14122" href="plfa.part2.Confluence.html#14122" class="Bound">p1</a> <a id="14125" href="plfa.part2.Confluence.html#14125" class="Bound">p3</a><a id="14127" class="Symbol">)</a> <a id="14129" class="Symbol">(</a><a id="14130" href="plfa.part2.Confluence.html#2936" class="InductiveConstructor">pbeta</a> <a id="14136" href="plfa.part2.Confluence.html#14136" class="Bound">p2</a> <a id="14139" href="plfa.part2.Confluence.html#14139" class="Bound">p4</a><a id="14141" class="Symbol">)</a>
<a id="14147" class="Keyword">with</a> <a id="14152" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="14164" href="plfa.part2.Confluence.html#14122" class="Bound">p1</a> <a id="14167" href="plfa.part2.Confluence.html#14136" class="Bound">p2</a>
<a id="14170" class="Symbol">...</a> <a id="14174" class="Symbol">|</a> <a id="14176" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14178" href="/19.08/Confluence/#14178" class="Bound">N₃</a> <a id="14181" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14183" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14185" href="plfa.part2.Confluence.html#14185" class="Bound">p5</a> <a id="14188" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14190" href="plfa.part2.Confluence.html#14190" class="Bound">p6</a> <a id="14193" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14195" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="14203" class="Keyword">with</a> <a id="14208" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="14220" class="Bound">p3</a> <a id="14223" class="Bound">p4</a>
<a id="14226" class="Symbol">...</a> <a id="14232" class="Symbol">|</a> <a id="14234" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14236" href="/19.08/Confluence/#14236" class="Bound">M₃</a> <a id="14239" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14241" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14243" href="plfa.part2.Confluence.html#14243" class="Bound">p7</a> <a id="14246" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14248" href="plfa.part2.Confluence.html#14248" class="Bound">p8</a> <a id="14251" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14253" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14255" class="Symbol">=</a>
<a id="14265" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14267" class="Bound">N₃</a> <a id="14270" href="/19.08/Untyped/#7491" class="Function Operator">[</a> <a id="14272" href="/19.08/Confluence/#14236" class="Bound">M₃</a> <a id="14275" href="plfa.part2.Untyped.html#7491" class="Function Operator">]</a> <a id="14277" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14279" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="14281" href="plfa.part2.Confluence.html#12517" class="Function">sub-par</a> <a id="14289" class="Bound">p5</a> <a id="14292" href="plfa.part2.Confluence.html#14243" class="Bound">p7</a> <a id="14295" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="14297" href="plfa.part2.Confluence.html#12517" class="Function">sub-par</a> <a id="14305" class="Bound">p6</a> <a id="14308" href="plfa.part2.Confluence.html#14248" class="Bound">p8</a> <a id="14311" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="14313" 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="16733" href="/19.08/Confluence/#16733" class="Function">strip</a> <a id="16739" class="Symbol">:</a> <a id="16741" class="Symbol">∀{</a><a id="16743" href="plfa.part2.Confluence.html#16743" class="Bound">Γ</a> <a id="16745" href="plfa.part2.Confluence.html#16745" class="Bound">A</a><a id="16746" class="Symbol">}</a> <a id="16748" class="Symbol">{</a><a id="16749" href="plfa.part2.Confluence.html#16749" class="Bound">M</a> <a id="16751" href="plfa.part2.Confluence.html#16751" class="Bound">N</a> <a id="16753" href="plfa.part2.Confluence.html#16753" class="Bound">N′</a> <a id="16756" class="Symbol">:</a> <a id="16758" href="plfa.part2.Confluence.html#16743" class="Bound">Γ</a> <a id="16760" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="16762" href="plfa.part2.Confluence.html#16745" class="Bound">A</a><a id="16763" class="Symbol">}</a>
<a id="16767" class="Symbol">→</a> <a id="16769" href="/19.08/Confluence/#16749" class="Bound">M</a> <a id="16771" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="16773" href="plfa.part2.Confluence.html#16751" class="Bound">N</a>
<a id="16777" class="Symbol">→</a> <a id="16779" href="/19.08/Confluence/#16749" class="Bound">M</a> <a id="16781" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="16784" href="plfa.part2.Confluence.html#16753" class="Bound">N′</a>
<a id="16791" class="Comment">------------------------------------</a>
<a id="16830" class="Symbol">→</a> <a id="16832" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="16835" href="/19.08/Confluence/#16835" class="Bound">L</a> <a id="16837" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="16839" href="plfa.part2.Confluence.html#16743" class="Bound">Γ</a> <a id="16841" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="16843" href="plfa.part2.Confluence.html#16745" class="Bound">A</a> <a id="16845" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="16847" class="Symbol">(</a><a id="16848" href="plfa.part2.Confluence.html#16751" class="Bound">N</a> <a id="16850" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="16853" href="plfa.part2.Confluence.html#16835" class="Bound">L</a><a id="16854" class="Symbol">)</a> <a id="16857" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="16860" class="Symbol">(</a><a id="16861" href="plfa.part2.Confluence.html#16753" class="Bound">N′</a> <a id="16864" href="plfa.part2.Confluence.html#2637" class="Datatype Operator">⇛</a> <a id="16866" href="plfa.part2.Confluence.html#16835" class="Bound">L</a><a id="16867" class="Symbol">)</a>
<a id="16869" href="/19.08/Confluence/#16733" class="Function">strip</a><a id="16874" class="Symbol">{</a><a id="16875" href="plfa.part2.Confluence.html#16875" class="Bound">Γ</a><a id="16876" class="Symbol">}{</a><a id="16878" href="plfa.part2.Confluence.html#16878" class="Bound">A</a><a id="16879" class="Symbol">}{</a><a id="16881" href="plfa.part2.Confluence.html#16881" class="Bound">M</a><a id="16882" class="Symbol">}{</a><a id="16884" href="plfa.part2.Confluence.html#16884" class="Bound">N</a><a id="16885" class="Symbol">}{</a><a id="16887" href="plfa.part2.Confluence.html#16887" class="Bound">N′</a><a id="16889" class="Symbol">}</a> <a id="16891" href="plfa.part2.Confluence.html#16891" class="Bound">mn</a> <a id="16894" class="Symbol">(</a><a id="16895" href="plfa.part2.Confluence.html#16881" class="Bound">M</a> <a id="16897" href="plfa.part2.Confluence.html#3790" class="InductiveConstructor Operator">∎</a><a id="16898" class="Symbol">)</a> <a id="16900" class="Symbol">=</a> <a id="16902" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16904" href="plfa.part2.Confluence.html#16884" class="Bound">N</a> <a id="16906" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16908" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16910" href="plfa.part2.Confluence.html#16884" class="Bound">N</a> <a id="16912" href="plfa.part2.Confluence.html#3790" class="InductiveConstructor Operator">∎</a> <a id="16914" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16916" href="plfa.part2.Confluence.html#16891" class="Bound">mn</a> <a id="16919" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16921" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="16923" href="/19.08/Confluence/#16733" class="Function">strip</a><a id="16928" class="Symbol">{</a><a id="16929" href="plfa.part2.Confluence.html#16929" class="Bound">Γ</a><a id="16930" class="Symbol">}{</a><a id="16932" href="plfa.part2.Confluence.html#16932" class="Bound">A</a><a id="16933" class="Symbol">}{</a><a id="16935" href="plfa.part2.Confluence.html#16935" class="Bound">M</a><a id="16936" class="Symbol">}{</a><a id="16938" href="plfa.part2.Confluence.html#16938" class="Bound">N</a><a id="16939" class="Symbol">}{</a><a id="16941" href="plfa.part2.Confluence.html#16941" class="Bound">N′</a><a id="16943" class="Symbol">}</a> <a id="16945" href="plfa.part2.Confluence.html#16945" class="Bound">mn</a> <a id="16948" class="Symbol">(</a><a id="16949" href="plfa.part2.Confluence.html#16935" class="Bound">M</a> <a id="16951" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⇛⟨</a> <a id="16954" href="plfa.part2.Confluence.html#16954" class="Bound">mm&#39;</a> <a id="16958" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⟩</a> <a id="16960" href="plfa.part2.Confluence.html#16960" class="Bound">m&#39;n&#39;</a><a id="16964" class="Symbol">)</a>
<a id="16970" class="Keyword">with</a> <a id="16975" href="/19.08/Confluence/#13046" class="Function">par-diamond</a> <a id="16987" href="plfa.part2.Confluence.html#16945" class="Bound">mn</a> <a id="16990" href="plfa.part2.Confluence.html#16954" class="Bound">mm&#39;</a>
<a id="16994" class="Symbol">...</a> <a id="16998" class="Symbol">|</a> <a id="17000" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17002" href="/19.08/Confluence/#17002" class="Bound">L</a> <a id="17004" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17006" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17008" href="plfa.part2.Confluence.html#17008" class="Bound">nl</a> <a id="17011" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17013" href="plfa.part2.Confluence.html#17013" class="Bound">m&#39;l</a> <a id="17017" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17019" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17027" class="Keyword">with</a> <a id="17032" href="/19.08/Confluence/#16733" class="Function">strip</a> <a id="17038" href="plfa.part2.Confluence.html#17013" class="Bound">m&#39;l</a> <a id="17042" class="Bound">m&#39;n&#39;</a>
<a id="17047" class="Symbol">...</a> <a id="17053" class="Symbol">|</a> <a id="17055" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17057" href="/19.08/Confluence/#17057" class="Bound">L′</a> <a id="17060" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17062" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17064" href="plfa.part2.Confluence.html#17064" class="Bound">ll&#39;</a> <a id="17068" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17070" href="plfa.part2.Confluence.html#17070" class="Bound">n&#39;l&#39;</a> <a id="17075" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17077" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17079" class="Symbol">=</a>
<a id="17089" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17091" href="/19.08/Confluence/#17057" class="Bound">L′</a> <a id="17094" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17096" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17098" class="Symbol">(</a><a id="17099" class="Bound">N</a> <a id="17101" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⇛⟨</a> <a id="17104" class="Bound">nl</a> <a id="17107" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⟩</a> <a id="17109" href="plfa.part2.Confluence.html#17064" class="Bound">ll&#39;</a><a id="17112" class="Symbol">)</a> <a id="17114" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17116" href="plfa.part2.Confluence.html#17070" class="Bound">n&#39;l&#39;</a> <a id="17121" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17123" 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="17280" href="/19.08/Confluence/#17280" class="Function">par-confluence</a> <a id="17295" class="Symbol">:</a> <a id="17297" class="Symbol">∀{</a><a id="17299" href="plfa.part2.Confluence.html#17299" class="Bound">Γ</a> <a id="17301" href="plfa.part2.Confluence.html#17301" class="Bound">A</a><a id="17302" class="Symbol">}</a> <a id="17304" class="Symbol">{</a><a id="17305" href="plfa.part2.Confluence.html#17305" class="Bound">L</a> <a id="17307" href="plfa.part2.Confluence.html#17307" class="Bound">M₁</a> <a id="17310" href="plfa.part2.Confluence.html#17310" class="Bound">M₂</a> <a id="17313" class="Symbol">:</a> <a id="17315" href="plfa.part2.Confluence.html#17299" class="Bound">Γ</a> <a id="17317" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="17319" href="plfa.part2.Confluence.html#17301" class="Bound">A</a><a id="17320" class="Symbol">}</a>
<a id="17324" class="Symbol">→</a> <a id="17326" href="/19.08/Confluence/#17305" class="Bound">L</a> <a id="17328" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="17331" href="plfa.part2.Confluence.html#17307" class="Bound">M₁</a>
<a id="17336" class="Symbol">→</a> <a id="17338" href="/19.08/Confluence/#17305" class="Bound">L</a> <a id="17340" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="17343" href="plfa.part2.Confluence.html#17310" class="Bound">M₂</a>
<a id="17350" class="Comment">------------------------------------</a>
<a id="17389" class="Symbol">→</a> <a id="17391" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="17394" href="/19.08/Confluence/#17394" class="Bound">N</a> <a id="17396" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="17398" href="plfa.part2.Confluence.html#17299" class="Bound">Γ</a> <a id="17400" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="17402" href="plfa.part2.Confluence.html#17301" class="Bound">A</a> <a id="17404" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="17406" class="Symbol">(</a><a id="17407" href="plfa.part2.Confluence.html#17307" class="Bound">M₁</a> <a id="17410" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="17413" href="plfa.part2.Confluence.html#17394" class="Bound">N</a><a id="17414" class="Symbol">)</a> <a id="17416" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="17418" class="Symbol">(</a><a id="17419" href="plfa.part2.Confluence.html#17310" class="Bound">M₂</a> <a id="17422" href="plfa.part2.Confluence.html#3740" class="Datatype Operator">⇛*</a> <a id="17425" href="plfa.part2.Confluence.html#17394" class="Bound">N</a><a id="17426" class="Symbol">)</a>
<a id="17428" href="/19.08/Confluence/#17280" class="Function">par-confluence</a> <a id="17443" class="Symbol">{</a><a id="17444" href="plfa.part2.Confluence.html#17444" class="Bound">Γ</a><a id="17445" class="Symbol">}{</a><a id="17447" href="plfa.part2.Confluence.html#17447" class="Bound">A</a><a id="17448" class="Symbol">}{</a><a id="17450" href="plfa.part2.Confluence.html#17450" class="Bound">L</a><a id="17451" class="Symbol">}{</a><a id="17453" class="DottedPattern Symbol">.</a><a id="17454" href="plfa.part2.Confluence.html#17450" class="DottedPattern Bound">L</a><a id="17455" class="Symbol">}{</a><a id="17457" href="plfa.part2.Confluence.html#17457" class="Bound">N</a><a id="17458" class="Symbol">}</a> <a id="17460" class="Symbol">(</a><a id="17461" href="plfa.part2.Confluence.html#17450" class="Bound">L</a> <a id="17463" href="plfa.part2.Confluence.html#3790" class="InductiveConstructor Operator">∎</a><a id="17464" class="Symbol">)</a> <a id="17466" href="plfa.part2.Confluence.html#17466" class="Bound">L⇛*N</a> <a id="17471" class="Symbol">=</a> <a id="17473" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17475" href="plfa.part2.Confluence.html#17457" class="Bound">N</a> <a id="17477" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17479" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17481" href="plfa.part2.Confluence.html#17466" class="Bound">L⇛*N</a> <a id="17486" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17488" href="plfa.part2.Confluence.html#17457" class="Bound">N</a> <a id="17490" href="plfa.part2.Confluence.html#3790" class="InductiveConstructor Operator">∎</a> <a id="17492" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17494" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17496" href="/19.08/Confluence/#17280" class="Function">par-confluence</a> <a id="17511" class="Symbol">{</a><a id="17512" href="plfa.part2.Confluence.html#17512" class="Bound">Γ</a><a id="17513" class="Symbol">}{</a><a id="17515" href="plfa.part2.Confluence.html#17515" class="Bound">A</a><a id="17516" class="Symbol">}{</a><a id="17518" href="plfa.part2.Confluence.html#17518" class="Bound">L</a><a id="17519" class="Symbol">}{</a><a id="17521" href="plfa.part2.Confluence.html#17521" class="Bound">M₁′</a><a id="17524" class="Symbol">}{</a><a id="17526" href="plfa.part2.Confluence.html#17526" class="Bound">M₂</a><a id="17528" class="Symbol">}</a> <a id="17530" class="Symbol">(</a><a id="17531" href="plfa.part2.Confluence.html#17518" class="Bound">L</a> <a id="17533" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⇛⟨</a> <a id="17536" href="plfa.part2.Confluence.html#17536" class="Bound">L⇛M₁</a> <a id="17541" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⟩</a> <a id="17543" href="plfa.part2.Confluence.html#17543" class="Bound">M₁⇛*M₁′</a><a id="17550" class="Symbol">)</a> <a id="17552" href="plfa.part2.Confluence.html#17552" class="Bound">L⇛*M₂</a>
<a id="17562" class="Keyword">with</a> <a id="17567" href="/19.08/Confluence/#16733" class="Function">strip</a> <a id="17573" href="plfa.part2.Confluence.html#17536" class="Bound">L⇛M₁</a> <a id="17578" href="plfa.part2.Confluence.html#17552" class="Bound">L⇛*M₂</a>
<a id="17584" class="Symbol">...</a> <a id="17588" class="Symbol">|</a> <a id="17590" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17592" href="/19.08/Confluence/#17592" class="Bound">N</a> <a id="17594" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17596" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17598" href="plfa.part2.Confluence.html#17598" class="Bound">M₁⇛*N</a> <a id="17604" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17606" href="plfa.part2.Confluence.html#17606" class="Bound">M₂⇛N</a> <a id="17611" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17613" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17621" class="Keyword">with</a> <a id="17626" href="/19.08/Confluence/#17280" class="Function">par-confluence</a> <a id="17641" class="Bound">M₁⇛*M₁′</a> <a id="17649" href="plfa.part2.Confluence.html#17598" class="Bound">M₁⇛*N</a>
<a id="17655" class="Symbol">...</a> <a id="17661" class="Symbol">|</a> <a id="17663" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17665" href="/19.08/Confluence/#17665" class="Bound">N′</a> <a id="17668" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17670" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17672" href="plfa.part2.Confluence.html#17672" class="Bound">M₁′⇛*N′</a> <a id="17680" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17682" href="plfa.part2.Confluence.html#17682" class="Bound">N⇛*N′</a> <a id="17688" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17690" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17692" class="Symbol">=</a>
<a id="17702" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17704" href="/19.08/Confluence/#17665" class="Bound">N′</a> <a id="17707" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17709" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17711" href="plfa.part2.Confluence.html#17672" class="Bound">M₁′⇛*N′</a> <a id="17719" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17721" class="Symbol">(</a><a id="17722" class="Bound">M₂</a> <a id="17725" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⇛⟨</a> <a id="17728" class="Bound">M₂⇛N</a> <a id="17733" href="plfa.part2.Confluence.html#3846" class="InductiveConstructor Operator">⟩</a> <a id="17735" href="plfa.part2.Confluence.html#17682" class="Bound">N⇛*N′</a><a id="17740" class="Symbol">)</a> <a id="17742" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17744" 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="18473" href="/19.08/Confluence/#18473" class="Function">confluence</a> <a id="18484" class="Symbol">:</a> <a id="18486" class="Symbol">∀{</a><a id="18488" href="plfa.part2.Confluence.html#18488" class="Bound">Γ</a> <a id="18490" href="plfa.part2.Confluence.html#18490" class="Bound">A</a><a id="18491" class="Symbol">}</a> <a id="18493" class="Symbol">{</a><a id="18494" href="plfa.part2.Confluence.html#18494" class="Bound">L</a> <a id="18496" href="plfa.part2.Confluence.html#18496" class="Bound">M₁</a> <a id="18499" href="plfa.part2.Confluence.html#18499" class="Bound">M₂</a> <a id="18502" class="Symbol">:</a> <a id="18504" href="plfa.part2.Confluence.html#18488" class="Bound">Γ</a> <a id="18506" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="18508" href="plfa.part2.Confluence.html#18490" class="Bound">A</a><a id="18509" class="Symbol">}</a>
<a id="18513" class="Symbol">→</a> <a id="18515" href="/19.08/Confluence/#18494" class="Bound">L</a> <a id="18517" href="/19.08/Untyped/#11267" class="Datatype Operator">—↠</a> <a id="18520" href="plfa.part2.Confluence.html#18496" class="Bound">M₁</a>
<a id="18525" class="Symbol">→</a> <a id="18527" href="/19.08/Confluence/#18494" class="Bound">L</a> <a id="18529" href="/19.08/Untyped/#11267" class="Datatype Operator">—↠</a> <a id="18532" href="plfa.part2.Confluence.html#18499" class="Bound">M₂</a>
<a id="18539" class="Comment">-----------------------------------</a>
<a id="18577" class="Symbol">→</a> <a id="18579" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="18582" href="/19.08/Confluence/#18582" class="Bound">N</a> <a id="18584" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="18586" href="plfa.part2.Confluence.html#18488" class="Bound">Γ</a> <a id="18588" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="18590" href="plfa.part2.Confluence.html#18490" class="Bound">A</a> <a id="18592" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="18594" class="Symbol">(</a><a id="18595" href="plfa.part2.Confluence.html#18496" class="Bound">M₁</a> <a id="18598" href="plfa.part2.Untyped.html#11267" class="Datatype Operator">—↠</a> <a id="18601" href="plfa.part2.Confluence.html#18582" class="Bound">N</a><a id="18602" class="Symbol">)</a> <a id="18604" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="18606" class="Symbol">(</a><a id="18607" href="plfa.part2.Confluence.html#18499" class="Bound">M₂</a> <a id="18610" href="plfa.part2.Untyped.html#11267" class="Datatype Operator">—↠</a> <a id="18613" href="plfa.part2.Confluence.html#18582" class="Bound">N</a><a id="18614" class="Symbol">)</a>
<a id="18616" href="/19.08/Confluence/#18473" class="Function">confluence</a> <a id="18627" href="plfa.part2.Confluence.html#18627" class="Bound">L↠M₁</a> <a id="18632" href="plfa.part2.Confluence.html#18632" class="Bound">L↠M₂</a>
<a id="18641" class="Keyword">with</a> <a id="18646" href="/19.08/Confluence/#17280" class="Function">par-confluence</a> <a id="18661" class="Symbol">(</a><a id="18662" href="plfa.part2.Confluence.html#4942" class="Function">betas-pars</a> <a id="18673" href="plfa.part2.Confluence.html#18627" class="Bound">L↠M₁</a><a id="18677" class="Symbol">)</a> <a id="18679" class="Symbol">(</a><a id="18680" href="plfa.part2.Confluence.html#4942" class="Function">betas-pars</a> <a id="18691" href="plfa.part2.Confluence.html#18632" class="Bound">L↠M₂</a><a id="18695" class="Symbol">)</a>
<a id="18697" class="Symbol">...</a> <a id="18701" class="Symbol">|</a> <a id="18703" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18705" href="/19.08/Confluence/#18705" class="Bound">N</a> <a id="18707" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18709" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18711" href="plfa.part2.Confluence.html#18711" class="Bound">M₁⇛N</a> <a id="18716" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18718" href="plfa.part2.Confluence.html#18718" class="Bound">M₂⇛N</a> <a id="18723" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18725" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18727" class="Symbol">=</a>
<a id="18735" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18737" href="/19.08/Confluence/#18705" class="Bound">N</a> <a id="18739" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18741" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18743" href="plfa.part2.Confluence.html#6888" class="Function">pars-betas</a> <a id="18754" href="plfa.part2.Confluence.html#18711" class="Bound">M₁⇛N</a> <a id="18759" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18761" href="plfa.part2.Confluence.html#6888" class="Function">pars-betas</a> <a id="18772" href="plfa.part2.Confluence.html#18718" class="Bound">M₂⇛N</a> <a id="18777" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18779" 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="/19.08/Untyped/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part2/Confluence.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/BigStep/">Next</a>
</p>
</article>
</div>
</main><footer class="site-footer h-card">
<data class="u-url" href="/19.08/"></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="/19.08/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="/19.08/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="/19.08/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 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="/19.08/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="/19.08/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="/19.08/assets/jquery.js"></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="/19.08/assets/katex.js"></script>
<!-- Script which renders TeX using KaTeX -->
<script type="text/javascript">
$("script[type='math/tex']").replaceWith(
function(){
var tex = $(this).text();
return "<span class=\"inline-equation\">" +
katex.renderToString(tex) +
"</span>";
});
$("script[type='math/tex; mode=display']").replaceWith(
function(){
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
return "<div class=\"equation\">" +
katex.renderToString("\\displaystyle "+tex) +
"</div>";
});
</script>
</body>
</html>
Reference in a new issue View git blame Copy permalink