--- title: "Compare Eval Relations" description: "Compare Eval Relations - URL: https://chatgpt.com/c/6a85a372-3f0c-83ea-b4aa-9c7f2021fb02 - Created: 2026-08-19T12:37:47.020Z --- [image: sediment://file00000000d370822fbd4abdcb8aad8f0f] [image: se…" doc_version: 1 last_updated: 2026-09-26 canonical_url: "http://parc.yolo.scapegoat.dev/note/transcripts/2026/08/19/chatgpt-transcript-compare-eval-relations" --- # Compare Eval Relations Compare Eval Relations - URL: https://chatgpt.com/c/6a85a372-3f0c-83ea-b4aa-9c7f2021fb02 - Created: 2026-08-19T12:37:47.020Z --- > [image: sediment://file00000000d370822fbd4abdcb8aad8f0f] > [image: se… ## Content # Compare Eval Relations - URL: https://chatgpt.com/c/6a85a372-3f0c-83ea-b4aa-9c7f2021fb02 - Created: 2026-08-19T12:37:47.020Z --- > [image: sediment://file_00000000d370822fbd4abdcb8aad8f0f] > [image: sediment://file_00000000eb30822f9a0b41f81a26f259] > [image: sediment://file_00000000b478822fa86449434bf9725b] > Help me understand the diff between eval = and eval ->>
💭 Thinking **Clarifying evaluators** I’m distinguishing the underlying relations: the equational evaluator uses the symmetric equivalence closure, while the directional evaluator follows reductions forward. They coincide only when the rewrite system is confluent and terminating, ensuring unique results. **Clarified evaluators**
Yes — your note is basically pointing at the right distinction. The important difference is **what relation is used to connect a program $B$ to its result $R$**. ### 1. $eval^{=_{r}}_r$: the equational evaluator This evaluator uses the **equivalence relation generated by the rules $r$**. Roughly, $$ eval^{=_{r}}_r(B)=R \quad\text{when}\quad B =_r R $$ Here $=_r$ is built by taking the rules and allowing **reflexivity, symmetry, and transitivity**. So if a rule says $$ B_1 \to_r B_2 $$ then equational reasoning lets you use it in either direction: $$ B_1 =_r B_2 \qquad\text{and}\qquad B_2 =_r B_1. $$ That's why it feels "non-directional." You're saying two expressions are **equal according to the language's equations**, not describing a sequence of computation steps. --- ### 2. $eval^{\twoheadrightarrow_r}_r$: the directional evaluator This one uses the **reduction relation**: $$ eval^{\twoheadrightarrow_r}_r(B)=R \quad\text{when}\quad B \twoheadrightarrow_r R $$ where $$ B \twoheadrightarrow_r R $$ means something like: $$ B \to_r B_1 \to_r B_2 \to_r \cdots \to_r R. $$ This is the reflexive-transitive closure of reduction, plus the compatible/contextual machinery described in your notes. Crucially, **there is no symmetry**. If $$ B_1 \to_r B_2 $$ you cannot automatically conclude $$ B_2 \to_r B_1. $$ So this one really describes **computation going forward**. --- ### Why can the two evaluators nevertheless be equal? This is the point the textbook is setting up. Although $$ =_r $$ is a much larger relation than $$ \twoheadrightarrow_r, $$ the evaluator only cares about one particular question: $$ \text{"What result } R \text{ does } B \text{ produce?"} $$ For example, suppose $t$ and $f$ are the only final results. The book wants to prove that $$ eval^{=_{r}}_r(B)=R \iff eval^{\twoheadrightarrow_r}_r(B)=R. $$ So: $$ B =_r t \iff B \twoheadrightarrow_r t $$ and likewise for $f$. The **relations themselves are not the same**: $$ =_r \neq \twoheadrightarrow_r. $$ But when you restrict attention to "does this program evaluate to this final result?", they can give the same answer. ### A useful mental model Think of $$ =_r $$ as **reasoning about equality**: $$ A = B = C = D $$ and $$ \twoheadrightarrow_r $$ as **actually running the program**: $$ A \to B \to C \to D. $$ The first lets you move equations around mathematically. The second respects the intended computational direction. So your sentence that equivalence closure "removes the directionality" is correct. The one adjustment I'd make is: **it doesn't just add transitivity**. The important extra ingredient is **symmetry**. $$ \boxed{ \begin{array}{c|c} eval^{=_{r}}_r & eval^{\twoheadrightarrow_r}_r\\ \hline \text{equational} & \text{operational/reduction}\\ \text{uses equivalence} & \text{uses forward reduction}\\ \text{reflexive + symmetric + transitive} & \text{reflexive + transitive}\\ \text{can reason backwards} & \text{cannot reduce backwards} \end{array}} $$ And the theorem the page is heading toward is essentially: **despite those different definitions, they compute the same result.** --- > Why is = larger than ->> what does it mean? “Larger” means **it contains more related pairs of expressions**. A relation is just a set of pairs. So if we have: $$ A \to B \to C $$ then the reflexive-transitive reduction relation $\twoheadrightarrow$ contains pairs like $$ (A,A), (B,B), (C,C), (A,B), (B,C), (A,C). $$ It says: “starting from the left expression, I can reduce forward to the right expression.” But $=$ is an **equivalence relation**, so it also has symmetry. Therefore from $$ A = B $$ you also get $$ B = A. $$ So in this example, $=$ would additionally contain things like $$ (B,A), (C,B), (C,A). $$ In fact: $$ \{(A,A),(A,B),(A,C),(B,B),(B,C),(C,C)\} $$ is the sort of thing $\twoheadrightarrow$ gives, while $=$ can contain $$ \{(A,A),(A,B),(A,C),(B,A),(B,B),(B,C),(C,A),(C,B),(C,C)\}. $$ So we write informally: $$ \twoheadrightarrow \subseteq = $$ and say $=$ is “larger.” The key reason is **symmetry**: $$ A \twoheadrightarrow B $$ does **not** imply $$ B \twoheadrightarrow A, $$ but $$ A = B $$ does imply $$ B = A. $$ So “larger” does not mean the $=$ evaluator is somehow better or computes more. It means the underlying relation identifies **more pairs of expressions** as related. A good mental picture is: $$ A \to B \to C $$ for reduction: arrows only go forward. For equality: $$ A \leftrightarrow B \leftrightarrow C $$ because once they are considered equivalent, you can reason in either direction. That is exactly why the book later has to prove that even though $=$ is a larger relation than $\twoheadrightarrow$, they still give the **same final evaluation result**. --- > And the reason we study ->> in the first place is that it’s actually easier to implement ? Yes — that’s one of the main reasons. The directional relation $$ B \twoheadrightarrow_r R $$ looks like an actual computation: $$ B \to B_1 \to B_2 \to \cdots \to R. $$ So an interpreter can essentially follow those arrows: find the next reducible expression, apply the appropriate rule, repeat until a result is reached. By contrast, the equational relation $$ B =_r R $$ allows reasoning both forwards **and backwards** because of symmetry. That is useful mathematically, but it is not an obvious execution strategy. If you know $$ B =_r B' $$ you might be allowed to transform $B$ into $B'$ or $B'$ into $B$, and there may be many possible equations you could apply. That is much less like “run the program.” So a useful distinction is: $$ \boxed{\text{equational semantics: what expressions mean / are equivalent}} $$ versus $$ \boxed{\text{reduction semantics: how computation proceeds}} $$ And that explains why the book wants to prove $$ eval^{=_r}_r = eval^{\twoheadrightarrow_r}_r. $$ If they give the same answers, then you get the best of both worlds: use $=_r$ when doing convenient mathematical reasoning, and use $\twoheadrightarrow_r$ when thinking about or implementing an evaluator. So “easier to implement” is correct, but an even better phrase is: **$\twoheadrightarrow$ is closer to an executable description of the language.** --- > What does consistency of the equational calculus mean? In this chapter, **consistency of the equational calculus** means: > The equations cannot make one program equal to two different final results. Formally, if $$ eval^{=_r}_r(B)=R_1 $$ and also $$ eval^{=_r}_r(B)=R_2, $$ then necessarily $$ R_1=R_2. $$ Suppose the only results are $t$ and $f$. An **inconsistent** equational calculus could somehow derive both $$ B =_r t $$ and $$ B =_r f. $$ Then, by symmetry and transitivity, you'd effectively get $$ t =_r f, $$ which is disastrous: the calculus can no longer distinguish the two answers. Consistency guarantees that cannot happen. This is exactly what **Theorem 2.1** on your page is saying: $$ eval^{=_r}_r(B_0)=R_1 \quad\text{and}\quad eval^{=_r}_r(B_0)=R_2 \implies R_1=R_2. $$ So the theorem establishes that $eval^{=_r}_r$ really is a **function**: one input cannot have two different outputs. One subtle point: **consistency does not say every program has an answer.** It only says that if a program has an answer, it can't have two different ones. So: $$ \boxed{\text{consistency} = \text{at most one result}} $$ whereas a later question is: $$ \boxed{\text{termination/totality} = \text{does every program have a result?}} $$ --- > Where do these words consistency and equational calculus come from historically / mathematically ```json {"system1_search_query":[{"q":"Stanford Encyclopedia consistency formal systems Hilbert history consistency"},{"q":"Birkhoff 1935 On the Structure of Abstract Algebras equations formal equational logic"},{"q":"equational logic history Birkhoff universal algebra equations"},{"q":"calculus etymology Latin pebble calculation mathematics"}],"response_length":"medium"} ```
💭 Thinking **Searched 14 websites** **Clarifying terminology** I’m distinguishing ordinary logical consistency from this textbook’s specialized use: unique evaluation results show the calculus preserves distinctions. “Calculus” means a formal symbolic system, while “consistent” reflects equations fitting together without collapsing intendedly different outcomes. **Clarified terminology**
Both terms come from older mathematics and logic, and the way your book uses them is closely related to those older meanings. ### “Consistency” The ordinary idea behind **consistent** is that a collection of statements can “stand together” without conflicting. In mathematical logic this became: $$ \boxed{\text{A formal system is consistent if it cannot derive a contradiction.}} $$ For example, a logical system would be inconsistent if it could prove both $$ P $$ and $$ \neg P. $$ Consistency became especially central in the foundations of mathematics around the late 19th and early 20th centuries. Hilbert's program in the 1920s explicitly sought proofs that formalized mathematical systems were consistent—that their rules could never lead to contradiction. citeturn486900search0turn486900academia91 Your book is using a **closely related, slightly specialized version** of that idea. Suppose your language has two genuinely different answers: $$ t \neq f. $$ If the equational rules allowed $$ B =_r t $$ and $$ B =_r f, $$ then because equality is symmetric and transitive, $$ t =_r B =_r f, $$ so you'd derive $$ t =_r f. $$ The calculus has now collapsed two things that were supposed to be different. So when your page says it is establishing **“consistency for the equational calculus”**, you can read it as: > Our equations don't collapse distinct observable answers into one another. That's why Theorem 2.1 has the form $$ eval^{=_r}_r(B)=R_1 \quad\land\quad eval^{=_r}_r(B)=R_2 \quad\Longrightarrow\quad R_1=R_2. $$ In programming-language language, we might also call this **uniqueness of results** or **determinacy**. --- ### “Equational calculus” Here **calculus does not mean derivatives and integrals**. Historically, Latin *calculus* meant a small stone or pebble used for counting, and from that came the meaning of **reckoning/calculation**. Eventually mathematicians began using “calculus” more generally for a **system in which you manipulate symbols according to rules**. That's why mathematics and logic have names such as: $$ \text{propositional calculus},\qquad \lambda\text{-calculus},\qquad \text{sequent calculus}. $$ citeturn486900search7turn486900search5 So an **equational calculus** literally means approximately: > a rule-governed system for calculating/reasoning with equations. You start with equations supplied by the language, such as $$ (\text{some expression}) =_r (\text{some other expression}), $$ and you're allowed to derive new equations using principles such as $$ \frac{}{B = B} \quad\text{reflexivity} $$ $$ \frac{B_1=B_2}{B_2=B_1} \quad\text{symmetry} $$ $$ \frac{B_1=B_2\qquad B_2=B_3}{B_1=B_3} \quad\text{transitivity}, $$ plus rules allowing equations inside surrounding expressions (congruence/compatible closure). The modern mathematical theory of this kind of reasoning is usually called **equational logic**, and it is fundamental to **universal algebra**. Garrett Birkhoff's 1935 work was foundational in showing how algebraic structures can be characterized and reasoned about through equations; I wouldn't say he invented the phrase “equational calculus,” but his work is a major source of the modern formal theory behind it. citeturn486900search12turn486900search21 So the phrase on your page, > **“consistency of the equational calculus”** can almost be translated into plain English as: $$ \boxed{ \text{Do our rules for manipulating equations ever force contradictory/distinct answers to become equal?} } $$ And Theorem 2.1 says **no**: if the equations say that $B$ evaluates to $R_1$ and also to $R_2$, those results must actually be the same result. That connection to 20th-century mathematical logic is why the author says they are “following history.” --- > [image: sediment://file_000000003ea081f7a67a9e2ccf69edbd] > How does this relate (goldblatt topoi)
💭 Thinking **Connecting semantics** Goldblatt’s formal-language semantics interprets formulas in structures, while equational or reduction semantics interprets programs by computation. Both separate syntax from meaning: models validate equations; evaluators produce values. Topos semantics generalizes this by interpreting contexts, terms, and formulas categorically. **Connected semantics**
This is the same **syntax-vs-semantics pattern**, but Goldblatt is doing **model-theoretic semantics for logic**, whereas your other book is doing **semantics of programs by equations/reduction**. On the Goldblatt page, you have a formal language $\mathcal L$: symbols such as $R,c,v_1,v_2,\ldots$, together with rules for building formulas. By themselves these are just syntax. Then Goldblatt gives them meaning by choosing a model $$ \mathfrak A=\langle A,R,c\rangle. $$ Here $A$ is the universe of things variables can range over, $R$ interprets the relation symbol $R$, and $c$ interprets the constant symbol $c$. For formulas with free variables you also need a **valuation** $$ x=(x_1,x_2,\ldots), $$ which says $$ v_1\mapsto x_1,\quad v_2\mapsto x_2,\ldots $$ So the semantic question becomes something like $$ \mathfrak A,x \models \varphi. $$ That means: > Under interpretation $\mathfrak A$, and with variables assigned according to $x$, the syntactic formula $\varphi$ is true. This is very close in shape to evaluating a programming-language expression in an environment: $$ \llbracket e\rrbracket_\rho = v, $$ where $\rho$ tells you what the free variables mean. So the correspondence is roughly: | Goldblatt / logic | Programming languages | |---|---| | formula $\varphi$ | expression/program $B$ | | model $\mathfrak A$ | interpretation of primitive operations | | valuation $x$ | variable environment $\rho$ | | sentence | closed program/expression | | $\mathfrak A,x\models\varphi$ | evaluation gives some result | | truth value $T/F$ | result $R$ | The particularly important connection to your earlier discussion is that **equational calculus is on the syntactic side**, while Goldblatt's models are on the semantic side. For example, suppose a calculus proves $$ \varphi = \psi $$ or, in logic, $$ \vdash \varphi. $$ That is a statement about what can be obtained by manipulating symbols according to formal rules. By contrast, $$ \mathfrak A\models \varphi $$ is saying something about what the formula **means under an interpretation**. That gives the classic distinction: $$ \boxed{\text{syntax: what can be formally derived}} $$ versus $$ \boxed{\text{semantics: what is true in models}} $$ And then mathematics asks whether the two agree. In logic this leads to **soundness and completeness**: $$ \vdash\varphi \quad\Rightarrow\quad \models\varphi $$ for soundness, and, for suitable logical systems, $$ \models\varphi \quad\Rightarrow\quad \vdash\varphi $$ for completeness. That is strongly analogous to what your programming-languages book was doing with $$ eval^{=_r}_r $$ and $$ eval^{\twoheadrightarrow_r}_r. $$ There you have **two different formal ways of assigning behavior to the same program syntax**, and you prove that they give the same result. There is also a deeper connection to **topos theory**. Goldblatt is building toward the idea that the ordinary set-theoretic semantics shown on this page can be generalized. In ordinary first-order semantics, variables range over elements of a set $A$, relations are subsets such as $$ R\subseteq A\times A, $$ and formulas are interpreted as truth conditions. Categorically, these become: $$ A \quad\rightsquigarrow\quad \text{an object} $$ $$ R\subseteq A\times A \quad\rightsquigarrow\quad R\hookrightarrow A\times A $$ where the relation is represented by a **subobject**. And a formula with free variables $$ \varphi(v_1,\ldots,v_n) $$ can be interpreted as a subobject of the possible assignments: $$ \llbracket\varphi\rrbracket \hookrightarrow A^n. $$ In **Set**, that subobject is literally the set $$ \{(a_1,\ldots,a_n)\in A^n: \varphi(a_1,\ldots,a_n)\text{ is true}\}. $$ So Goldblatt's valuation $x$ is especially important: it's the elementary set-theoretic precursor of the categorical idea of plugging an assignment/generalized element into the interpretation of a formula. For instance, if $$ \varphi(v_1)=v_1Rc, $$ then classically its interpretation is $$ \llbracket \varphi\rrbracket = \{a\in A:aRc\} \subseteq A. $$ A valuation saying $v_1\mapsto a$ makes $\varphi$ true precisely when $$ a\in\llbracket\varphi\rrbracket. $$ That's the bridge to topoi: **logical formulas become geometric objects—subobjects—rather than merely strings that receive $T/F$.** So the big picture connecting both books is $$ \boxed{ \text{formal syntax} \;\longrightarrow\; \text{some mathematical interpretation} } $$ and then you prove that the syntactic rules faithfully capture that interpretation. Goldblatt does this through **models and categorical semantics**; the reduction-semantics text does it through **equations and computation relations**. --- > [image: sediment://file_000000003bec81f79ac3de911adc49c2] > [image: sediment://file_000000006ef4820c93f298b1e5c7f95b] > I don’t understand that proof modulo proof and also where did we assume the diamond property earlier?
💭 Thinking **Explaining proof structure** “Proof modulo proof” means the argument is complete assuming a separate claim is established. The diamond property is introduced here as that needed assumption, not something previously proved. The following Church–Rosser lemma then establishes it for the reduction relation. **Explained the proof structure**
You’re reading it correctly: **the diamond property was not proved earlier.** The author reaches a point where the current proof would work *if* another fact were available, so they temporarily isolate that fact as a new proof obligation. The phrase > “we have finished the proof modulo the proof of yet another claim” means roughly: $$ \boxed{\text{The current proof is complete, except that we still owe a proof of one subsidiary lemma.}} $$ Here is exactly where that happens. In Lemma 2.2, the goal is essentially: $$ M =_r N \quad\Longrightarrow\quad \exists L\;(M\twoheadrightarrow_r L\ \text{and}\ N\twoheadrightarrow_r L). $$ They prove this by induction on the derivation of $M=_rN$. The difficult case is **transitivity**. Suppose $$ M =_r L_0 \qquad\text{and}\qquad L_0 =_r N. $$ By the induction hypothesis, you get: $$ M\twoheadrightarrow L_1 \qquad L_0\twoheadrightarrow L_1 $$ and $$ L_0\twoheadrightarrow L_2 \qquad N\twoheadrightarrow L_2. $$ So the picture is: $$ \begin{array}{ccccc} M && L_0 && N\\ \downarrow && \swarrow\quad\searrow && \downarrow\\ L_1 &&&& L_2 \end{array} $$ Now you need one common $L_3$ so that $$ L_1\twoheadrightarrow L_3 \qquad\text{and}\qquad L_2\twoheadrightarrow L_3. $$ But notice: the induction hypothesis **does not give you that**. It only gave you $L_1$ and $L_2$. What you know is that $L_0$ reduces in two ways: $$ L_0\twoheadrightarrow L_1 \qquad\text{and}\qquad L_0\twoheadrightarrow L_2. $$ So the author says, essentially: > Suppose whenever this branching happens, the two branches can later be brought back together. That is: $$ L_0\twoheadrightarrow L_1 \;\land\; L_0\twoheadrightarrow L_2 $$ implies there exists $L_3$ such that $$ L_1\twoheadrightarrow L_3 \;\land\; L_2\twoheadrightarrow L_3. $$ And **that is the diamond / Church–Rosser property being introduced**. So your question “where did we assume this earlier?” has the answer: **We didn’t. The author assumes it temporarily right at the sentence “Now suppose that…” in order to see what remaining theorem would make Lemma 2.2 go through.** Then they stop and say: okay, now we need to actually prove that assumption. That becomes Lemma 2.3: $$ L\twoheadrightarrow M \quad\text{and}\quad L\twoheadrightarrow N $$ implies $$ \exists L'\; (M\twoheadrightarrow L' \;\land\; N\twoheadrightarrow L'). $$ That is Church–Rosser/confluence. So the proof structure is: $$ \text{Theorem 2.1} $$ depends on $$ \text{Lemma 2.2} $$ which, during its proof, turns out to depend on $$ \text{Lemma 2.3 (Church–Rosser)}. $$ The author is effectively **discovering the lemmas backward from what is needed**. And “modulo” is being used in the mathematical sense of **“up to / except for / conditional on.”** So: > “proof finished modulo proof of $X$” means > “the proof is finished assuming $X$; now we must separately prove $X$.” One subtle terminology point: the picture is often informally called the **diamond property**, while for the multi-step reduction relation $\twoheadrightarrow$, the standard broader term is **confluence** or **Church–Rosser**. The essential idea in this chapter is simply: **different reduction paths can be joined again.** --- > Oh I thought it was the induction assumption, but I guess the induction assumption only applies to M and N, not L1 and L2 ? Exactly, with one correction: the induction hypothesis does **not** apply just to the expressions $M$ and $N$; it applies to the **smaller equality derivations** that are premises of the current derivation. In the transitivity case, the current derivation ends like this: $$ \frac{M =_r L_0 \qquad L_0 =_r N}{M =_r N}. $$ Because the two premises are smaller derivations, the induction hypothesis applies to each: $$ M =_r L_0 \quad\Rightarrow\quad \exists L_1: M\twoheadrightarrow L_1,\; L_0\twoheadrightarrow L_1, $$ and $$ L_0 =_r N \quad\Rightarrow\quad \exists L_2: L_0\twoheadrightarrow L_2,\; N\twoheadrightarrow L_2. $$ So now you have: $$ \begin{array}{ccccc} M && L_0 && N\\ \downarrow && \swarrow\quad\searrow && \downarrow\\ L_1 &&&& L_2 \end{array} $$ Your temptation is: “Great, now use the induction hypothesis on $L_1$ and $L_2$.” But you **can't**, because the induction hypothesis isn't: $$ \text{for arbitrary }X,Y,\; X=_rY \Rightarrow \cdots $$ with no restriction. If it were, that would already be the entire theorem you're trying to prove. Rather, it says: > the theorem holds for equality derivations **strictly smaller than the current derivation**. And you haven't been given a smaller derivation whose conclusion is $$ L_1 =_r L_2. $$ What you do know about $L_1,L_2$ is instead: $$ L_0\twoheadrightarrow L_1 \qquad\text{and}\qquad L_0\twoheadrightarrow L_2. $$ That's information about the **reduction relation**, not an appropriate smaller equality derivation. And that's exactly where Church–Rosser enters: $$ L_0\twoheadrightarrow L_1,\quad L_0\twoheadrightarrow L_2 $$ should imply $$ \exists L_3: L_1\twoheadrightarrow L_3,\quad L_2\twoheadrightarrow L_3. $$ Then everything connects: $$ M\twoheadrightarrow L_1\twoheadrightarrow L_3 $$ and $$ N\twoheadrightarrow L_2\twoheadrightarrow L_3. $$ So the key lesson is: $$ \boxed{\text{Induction hypotheses apply to smaller derivations, not arbitrary new expressions.}} $$ That distinction is why $L_1,L_2$ require a separate property of reduction—the diamond/Church–Rosser property. --- > What’s “smaller derivation” in this context? Is it derivations I can construct out of applying the definition of r?
💭 Thinking **Clarifying derivation induction** I’m distinguishing the rewrite relation $r$ from the judgement $=_r$. A smaller derivation means a proper subtree of the proof that $M=_rN$, usually an immediate premise, not a smaller term. **Clarified derivation induction**
Yes, but with an important distinction: **“smaller derivation” means a smaller proof tree for the judgment $M =_r N$**, not necessarily a derivation using fewer applications of $r$ itself. Suppose $=_r$ is defined inductively by rules like base equations from $r$, reflexivity, symmetry, transitivity, compatibility, etc. A proof that $$ M =_r N $$ is then a finite tree made by applying those rules. For example, in the transitivity case: $$ \frac{ \underbrace{M =_r L_0}_{D_1} \qquad \underbrace{L_0 =_r N}_{D_2} }{ M =_r N } \text{ trans} $$ The whole tree is the derivation $D$ of $M=_rN$. The two premise trees $D_1$ and $D_2$ are **smaller derivations** because they are proper subtrees of $D$. Equivalently, they have smaller height / fewer inference-rule applications. So induction on derivations works like structural induction on a syntax tree: $$ \boxed{\text{Assume the property holds for the premise derivations; prove it for the conclusion.}} $$ The base case might indeed come directly from $r$, e.g. $$ M\,r\,N \quad\Rightarrow\quad M =_r N. $$ But the later derivations are built from the **rules defining $=_r$**, not merely by repeatedly applying $r$. This is also why you couldn't just invoke the induction hypothesis on $L_1,L_2$. Even if you can somehow prove $$ L_1 =_r L_2, $$ that proof is not automatically a **subderivation of the original proof $D$**. It may be newly constructed and could even be larger. The induction hypothesis only comes for free on the smaller trees already sitting underneath the current inference. A useful picture is: $$ \boxed{ r \;\text{provides the primitive steps/equations} \quad\longrightarrow\quad =_r \;\text{is generated by inference rules} \quad\longrightarrow\quad \text{a derivation is a proof tree} } $$ So “induction on the derivation” literally means induction on the shape/height of that proof tree. --- > How do I know that M =r L0 is “smaller” Strictly speaking, **$M =_r L_0$ itself is not “smaller.”** The **derivation proving it** is smaller. In the transitivity case, the derivation of $$ M =_r N $$ has the form $$ \frac{ \boxed{\text{derivation }D_1\text{ of }M=_rL_0} \qquad \boxed{\text{derivation }D_2\text{ of }L_0=_rN} }{ M=_rN } \text{ transitivity}. $$ The whole proof tree is $D$. The proofs $D_1$ and $D_2$ are literally **subtrees** of $D$: $$ D= \begin{array}{c} D_1\qquad D_2\\ \hline M=_rN \end{array} $$ So if “size” means number of inference-rule applications, $$ |D| = 1+|D_1|+|D_2|, $$ and therefore $$ |D_1|<|D|, \qquad |D_2|<|D|. $$ Or, if you're inducting on height, their heights are also strictly less than the height of $D$. ### But how do you know the proof has that shape? Because you're doing **induction on the derivation of $M=_rN$**. You ask: > What was the **last rule** used to produce $M=_rN$? One possibility is transitivity. If the last rule was transitivity, then by the definition of the transitivity inference rule, the proof must have arisen from two earlier proofs: $$ M=_rL_0 \qquad\text{and}\qquad L_0=_rN. $$ Those earlier proofs are necessarily contained inside the current proof tree. This is exactly analogous to structural induction on a syntax tree. If you have $$ e = e_1 + e_2, $$ then $e_1$ and $e_2$ are smaller because they are subexpressions used to construct $e$. Here it's: $$ \frac{M=_rL_0\qquad L_0=_rN}{M=_rN}. $$ The two premises are the “children,” and the conclusion is the larger tree constructed from them. So the safest wording is: $$ \boxed{\text{The derivation of }M=_rL_0\text{ is smaller because it is a proper subderivation of the derivation of }M=_rN.} $$ Not because $M$, $L_0$, or $N$ themselves are smaller expressions. --- > But isn’t M =r N over N =r M also a subtree?
💭 Thinking **Clarifying subtree direction** I’m distinguishing the derivation tree from the equality itself. If symmetry concludes $N =_r M$ from $M =_r N$, then $M =_r N$ is the premise subtree. If symmetry is reversed, the opposite judgment is the conclusion, not a subtree. **Clarified subtree direction**
Yes — **if symmetry is the last rule used**, then the opposite equality is a smaller subderivation. For example: $$ \frac{ \boxed{D_0:\;N =_r M} }{ M =_r N }\;\text{sym} $$ Here $D_0$, the derivation of $N=_rM$, is literally a subtree of the derivation of $M=_rN$. So the induction hypothesis applies to $D_0$. The subtlety is that this is **not true for every derivation of $M=_rN$**. It depends on how that particular proof was constructed. Suppose instead your current derivation is the transitivity one: $$ \frac{ D_1:M=_rL_0 \qquad D_2:L_0=_rN }{ M=_rN }\;\text{trans} $$ Its subtrees are $D_1$ and $D_2$. There is no derivation of $N=_rM$ sitting inside this tree. Of course, because symmetry is available, you can **construct** one: $$ \frac{ \boxed{D:M=_rN} }{ N=_rM }\;\text{sym} $$ But notice what happened: the original derivation $D$ is now **inside** the new derivation. So $$ \operatorname{size}(\text{proof of }N=_rM) = \operatorname{size}(D)+1. $$ It's **larger**, not smaller. That's the key distinction: $$ \boxed{\text{“I can derive }N=_rM\text{”} \neq \text{“the derivation of }N=_rM\text{ is a subderivation of my current proof.”}} $$ When doing induction on a derivation, you only get the induction hypothesis automatically for the **premise derivations actually used in the final inference step**. So when analyzing a derivation of $M=_rN$, you inspect its last rule: - if last rule = **symmetry**, $N=_rM$ is the smaller premise; - if last rule = **transitivity**, $M=_rL_0$ and $L_0=_rN$ are the smaller premises; - etc. This “specific proof tree, not merely the proposition being proved” point is the main conceptual trick in induction on derivations. --- > So up to the church rosser lemma we can have a proof tree that derives from the definition of r, in fact two proof trees that arrive to the conclusions of the existence of L1 and L2 , but at that point we cannot apply induction because this is actually a new term in itself? We have two proof trees we proved using induction, but then we have to start “ fresh” to prove the existence of L3? Yes. That is essentially the structure, with one terminology adjustment: the two things you get after applying the induction hypothesis are **reduction derivations**, not new equality proof trees. Start with one equality derivation whose last rule is transitivity: $$ \frac{ D_1:\ M=_r L_0 \qquad D_2:\ L_0=_r N }{ M=_r N } $$ Because $D_1,D_2$ are smaller subderivations, the induction hypothesis applies to each. From $D_1$, IH gives some $L_1$ and reduction derivations $$ M\twoheadrightarrow_r L_1 \qquad L_0\twoheadrightarrow_r L_1. $$ From $D_2$, IH gives some $L_2$ and reduction derivations $$ L_0\twoheadrightarrow_r L_2 \qquad N\twoheadrightarrow_r L_2. $$ So now the situation is $$ \begin{array}{ccccc} M && L_0 && N\\ \downarrow && \swarrow\quad\searrow && \downarrow\\ L_1 &&&& L_2 \end{array} $$ The induction hypothesis has done everything it is entitled to do. Now you need to finish the original goal, which requires a **single** $L$ such that $$ M\twoheadrightarrow L \qquad N\twoheadrightarrow L. $$ You would like to fill in: $$ L_1 \twoheadrightarrow L_3 \qquad L_2 \twoheadrightarrow L_3. $$ But there is no smaller equality subderivation available whose conclusion concerns $L_1$ and $L_2$. So induction on the original $=_r$ proof tree has nothing more to say. That's the exact point where you need a **different theorem about the reduction relation itself**: $$ L_0\twoheadrightarrow L_1 \quad\land\quad L_0\twoheadrightarrow L_2 $$ implies $$ \exists L_3.\; L_1\twoheadrightarrow L_3 \land L_2\twoheadrightarrow L_3. $$ That's Church–Rosser/confluence. Then you can concatenate paths: $$ M\twoheadrightarrow L_1\twoheadrightarrow L_3 $$ so $$ M\twoheadrightarrow L_3, $$ and similarly $$ N\twoheadrightarrow L_2\twoheadrightarrow L_3, $$ so $$ N\twoheadrightarrow L_3. $$ And now the transitivity case is complete. So your “start fresh” intuition is good. More precisely: $$ \boxed{ \text{The induction on }=_r\text{ has reached the limit of what its IH gives us.} } $$ We then temporarily leave that proof and prove a **separate lemma about $\twoheadrightarrow_r$**. Once that lemma is established, we plug it back into the unfinished transitivity case. The only part I'd change in your wording is “because $L_1,L_2$ are a new term.” The obstacle isn't that they're new *terms*. The obstacle is that **we do not possess smaller $=_r$-derivations involving $L_1$ and $L_2$** to which the induction hypothesis could apply. --- > What does a full proof treee for the theorem look like?
💭 Thinking **Structuring the proof** I’m treating the request as the full induction tree for Lemma 2.2. I’ll separate the object-level derivation from the meta-level induction and show how the transitivity case uses Church–Rosser. **Structured the proof** **Mapping induction cases** I’m identifying the likely cases: reduction, reflexivity, symmetry, transitivity, and compatibility. The first three are direct; transitivity combines two induction hypotheses, while compatibility lifts a common reduct through the surrounding context.
For the result you’ve been discussing—**Lemma 2.2** $$ M =_r N \quad\Longrightarrow\quad \exists L.\;M\twoheadrightarrow_r L\ \land\ N\twoheadrightarrow_r L, $$ there are actually **two different “trees” to keep separate**. ### 1. The input is a proof tree of $M=_rN$ For example, suppose the particular proof of $M=_rN$ ends with transitivity: $$ \frac{ \boxed{D_1:\;M=_rL_0} \qquad \boxed{D_2:\;L_0=_rN} }{ M=_rN } \;\text{trans} $$ The boxes $D_1,D_2$ might themselves be huge proof trees. They are the smaller subderivations. The induction says: > Assume Lemma 2.2 already works for $D_1$ and $D_2$, and use that to prove it for the whole tree. So applying the IH to $D_1$: $$ \frac{D_1:M=_rL_0} { \exists L_1.\; M\twoheadrightarrow L_1 \land L_0\twoheadrightarrow L_1 } \text{ IH} $$ and to $D_2$: $$ \frac{D_2:L_0=_rN} { \exists L_2.\; L_0\twoheadrightarrow L_2 \land N\twoheadrightarrow L_2 } \text{ IH}. $$ At this point you have $$ \begin{array}{ccccc} M && L_0 && N\\ \downarrow && \swarrow\quad\searrow && \downarrow\\ L_1 &&&& L_2 \end{array} $$ and **the induction has given you everything it can**. Now comes the extra lemma. From $$ L_0\twoheadrightarrow L_1 \qquad L_0\twoheadrightarrow L_2 $$ Church–Rosser gives: $$ \frac{ L_0\twoheadrightarrow L_1 \qquad L_0\twoheadrightarrow L_2 }{ \exists L_3.\; L_1\twoheadrightarrow L_3 \land L_2\twoheadrightarrow L_3 } \text{ Church–Rosser}. $$ So now: $$ M\twoheadrightarrow L_1\twoheadrightarrow L_3 $$ and therefore, by transitivity of $\twoheadrightarrow$, $$ M\twoheadrightarrow L_3. $$ Likewise, $$ N\twoheadrightarrow L_2\twoheadrightarrow L_3 $$ gives $$ N\twoheadrightarrow L_3. $$ Thus: $$ \boxed{ \exists L_3.\; M\twoheadrightarrow L_3 \land N\twoheadrightarrow L_3 } $$ which is exactly what Lemma 2.2 wanted. So schematically, the **transitivity branch of the proof** looks like: $$ \require{AMScd} \begin{array}{ccc} D_1:M=_rL_0 && D_2:L_0=_rN\\[3pt] \downarrow IH && \downarrow IH\\[3pt] \begin{matrix} M\twoheadrightarrow L_1\\ L_0\twoheadrightarrow L_1 \end{matrix} && \begin{matrix} L_0\twoheadrightarrow L_2\\ N\twoheadrightarrow L_2 \end{matrix}\\[8pt] &\searrow\quad\quad\swarrow&\\[-2pt] &\text{Church--Rosser}&\\ &\downarrow&\\ & \begin{matrix} L_1\twoheadrightarrow L_3\\ L_2\twoheadrightarrow L_3 \end{matrix} &\\[8pt] &\downarrow\text{ compose}&\\ & \boxed{ M\twoheadrightarrow L_3 \;\land\; N\twoheadrightarrow L_3 } & \end{array} $$ ### 2. The complete induction has several cases Because $=_r$ is generated from reduction by reflexivity, symmetry, and transitivity, the induction branches according to the **last rule of the $=_r$ proof**: - **Base reduction:** if $M\to_rN$, choose $L=N$. Then $M\twoheadrightarrow N$ and $N\twoheadrightarrow N$. - **Reflexivity:** $M=_rM$. Choose $L=M$. - **Symmetry:** if the premise is $N=_rM$, use the IH on that premise; the same common $L$ works. - **Transitivity:** use IH twice, then Church–Rosser as above. That is the full proof schema for Lemma 2.2. There isn't one gigantic concrete tree because the lemma is saying **whatever finite $=_r$ proof tree you hand me, I can recursively transform it into evidence that the two endpoints have a common reduct.** And then the dependency structure for the book's overall consistency theorem is roughly: $$ \boxed{\text{Theorem 2.1: uniqueness of evaluation}} $$ depends on $$ \boxed{\text{Lemma 2.2: }M=_rN\Rightarrow M,N\text{ have a common reduct}} $$ which depends, in its transitivity case, on $$ \boxed{\text{Lemma 2.3: Church--Rosser}} $$ which the book then proves separately. That's exactly what “proof finished **modulo** another proof” means: **we have built the upper part of the proof tree, but one of its branches is currently a box labeled “Church–Rosser”; now we go prove what's inside that box.** ## Sitemap - [Home](http://parc.yolo.scapegoat.dev/) - [Home markdown mirror](http://parc.yolo.scapegoat.dev/index.md) - [Markdown sitemap](http://parc.yolo.scapegoat.dev/sitemap.md)