From 74966bd31368b3392117fcdb10b6c06940aee874 Mon Sep 17 00:00:00 2001
From: Norman Ramsey <nr@cs.tufts.edu>
Date: Tue, 23 Jul 2024 21:08:55 -0400
Subject: [PATCH 1/2] motivate and explain parallel reduction, plus
 wordsmithing

---
 src/plfa/part2/Confluence.lagda.md | 54 ++++++++++++++++++++++++++++--
 1 file changed, 52 insertions(+), 2 deletions(-)

diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md
index abdd97d8c..ebae2f287 100644
--- a/src/plfa/part2/Confluence.lagda.md
+++ b/src/plfa/part2/Confluence.lagda.md
@@ -46,7 +46,14 @@ diamond property. Here is a counter example.
 Both terms can reduce to `a a`, but the second term requires two steps
 to get there, not one.
 
-To side-step this problem, we'll define an auxiliary reduction
+If we abstract this example, whenever `N —→ N'`,
+we have two ways to reduce a term of the form `(λ x. M) N`:
+
+    (λ x. M) N —→ (λ x. M) N′
+    (λ x. M) N —→ M [ x := N ]
+
+To bring these two reductions back together in a single step,
+we'll define an auxiliary reduction
 relation, called _parallel reduction_, that can perform many
 reductions simultaneously and thereby satisfy the diamond property.
 Furthermore, we show that a parallel reduction sequence exists between
@@ -72,7 +79,50 @@ open import plfa.part2.Untyped
 
 ## Parallel Reduction
 
-The parallel reduction relation is defined as follows.
+The problem with the example above is that when we reduce
+
+    (λ x. M) N —→ M [ x := N ]
+
+we make _two_ copies of `N`.  That's why bringing the terms back
+together requires two reduction steps, not one.  Because `M` is `x x`,
+
+    M [ x := N ]
+      ≡
+    N N 
+      —→
+    N' N
+      —→
+    N' N'
+
+Parallel reduction turns this sequence into a single step by allowing
+both function and argument to be reduced in the same step:
+
+    N N ⇛ N' N'
+
+To make reduction work in parallel, all that's needed is to change the
+rule for reducing a term of the form `L · M`.
+Ordinary reduction must reduce `L` _or_ `M`, but parallel reduction
+may reduce both `L` _and_ `M`.  Given a term `M [x := N ]` 
+where `N —→ N'`, parallel reduction can reduce every copy of `N`
+in a single step.
+
+Parallel reduction has one other fine point: in a term of the form
+
+    (λ x. M) N,
+
+it may be that `M [x := N ]` contains _no_ copies of `N` (because `x`
+does not occur free in `M`).  In this case,
+to match the reduction
+
+    (λ x. M) N —→ (λ x. M) N′
+
+it must be possible for `M [x := N]` to parallel-reduce to itself.
+(It is sufficient to allow a variable to parallel-reduce to itself;
+the rest is taken care of by
+structural rules for reducing abstractions and applications.)
+
+Using these two ideas, reflexive reduction and simultaneous reduction,
+the parallel-reduction relation is defined as follows.
 
 ```agda
 infix 2 _⇛_

From af8e16a46a02c5f55c28f109049f7a09b73a3630 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci[bot]"
 <66853113+pre-commit-ci[bot]@users.noreply.github.com>
Date: Fri, 26 Jul 2024 19:45:24 +0000
Subject: [PATCH 2/2] [pre-commit.ci] auto fixes from pre-commit.com hooks

for more information, see https://pre-commit.ci
---
 src/plfa/part2/Confluence.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md
index ebae2f287..e21c49740 100644
--- a/src/plfa/part2/Confluence.lagda.md
+++ b/src/plfa/part2/Confluence.lagda.md
@@ -88,7 +88,7 @@ together requires two reduction steps, not one.  Because `M` is `x x`,
 
     M [ x := N ]
       ≡
-    N N 
+    N N
       —→
     N' N
       —→
@@ -102,7 +102,7 @@ both function and argument to be reduced in the same step:
 To make reduction work in parallel, all that's needed is to change the
 rule for reducing a term of the form `L · M`.
 Ordinary reduction must reduce `L` _or_ `M`, but parallel reduction
-may reduce both `L` _and_ `M`.  Given a term `M [x := N ]` 
+may reduce both `L` _and_ `M`.  Given a term `M [x := N ]`
 where `N —→ N'`, parallel reduction can reduce every copy of `N`
 in a single step.