<p>I think you'll find that the exact same proof of Lemma 3 in [1] (the proof itself appears in [2]) concerning $\rightarrow^\infty_\beta$ also holds for $\rightarrow^\infty_{\beta\bot}$: indeed, they are defined in the same way from $\rightarrow^*_\beta$ and $\rightarrow^*_{\beta\bot}$ respectively, which are transitive by definition!</p>

<p>The lemma holds for an arbitrary reflexive-transitive congruence relation in place of $\rightarrow^*_{\beta\bot}$, as you can verify in [2] without needing to go into the detail of the coinductive proofs. In particular, the proofs of lemmas 4.1-5 in [2] are unchanged (with extra <em>induction</em> cases in 4.4).</p>

CC BY-SA 3.0
2015-07-08T07:53:11.203Z
Ah thanks! 4.4 is indeed the main step I was missing. Intuitively, even though (by definition) you only do a finite number of steps before recursing into subterms, you can later do more steps at the root.
Blaisorblade
CC BY-SA 3.0
2015-07-08T13:07:52.600Z
Morally yes. The lemma says you never actually have to.
cody
CC BY-SA 3.0
2015-07-07T19:19:36.207Z
2015-07-07T19:19:36.207Z
cody
<p>I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't work), and because I couldn't find a relevant lemma in the papers themselves.</p>

<p>I'm referring in particular to the definition by Czajka [1] of the relation $\rightarrow^\infty_{\beta\bot}$, called infinitary Böhm-reduction. I've looked at [2], which however does not include Böhm-reduction (such that the defined relation isn't confluent IIUC, which is a problem for me).</p>

<p>Rationale: Defining reduction for infinitary $\lambda$-calculus is tricky. In particular, you cannot create an "infinite transitive closure" which allows an infinite number of transitivity steps, but you need to be more careful. In particular, if you define multi-step reduction coinductively, you cannot include a transitive rule, lest your relation becomes total and thus degenerate. So one ends up doing <em>transitivity elimination</em>, which is not always trivial; and given how unintuitive coinduction is, I'm afraid I'd fool myself when attempting a proof.</p>

<p>[1] Łukasz Czajka, 2014. A Coinductive Confluence Proof for Infinitary Lambda-Calculus. Proc. of Rewriting and Typed Lambda Calculi, Springer. <a href="http://www.mimuw.edu.pl/~lukaszcz/coind.pdf" rel="nofollow">http://www.mimuw.edu.pl/~lukaszcz/coind.pdf</a></p>

<p>[2] Jorg Endrullis and Andrew Polonsky, 2011. Infinitary Rewriting Coinductively. In Proc. of TYPES, volume 19 of LIPIcs, pages 16–27. Schloss Dagstuhl. <a href="http://drops.dagstuhl.de/opus/volltexte/2013/3897/" rel="nofollow">http://drops.dagstuhl.de/opus/volltexte/2013/3897/</a></p>

<p>[3] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries, 1997. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93–125. <a href="http://www.sciencedirect.com/science/article/pii/S0304397596001715" rel="nofollow">http://www.sciencedirect.com/science/article/pii/S0304397596001715</a></p>

<pl.programming-languages><lambda-calculus><term-rewriting-systems>
Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?
Blaisorblade
# Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

(Asked by: username_0 on 2015-07-06)

I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't work), and because I couldn't find a relevant lemma in the papers themselves.

I'm referring in particular to the definition by Czajka [1] of the relation $\rightarrow^\infty\_{\beta\bot}$, called infinitary Böhm-reduction. I've looked at [2], which however does not include Böhm-reduction (such that the defined relation isn't confluent IIUC, which is a problem for me).

Rationale: Defining reduction for infinitary $\lambda$-calculus is tricky. In particular, you cannot create an "infinite transitive closure" which allows an infinite number of transitivity steps, but you need to be more careful. In particular, if you define multi-step reduction coinductively, you cannot include a transitive rule, lest your relation becomes total and thus degenerate. So one ends up doing *transitivity elimination*, which is not always trivial; and given how unintuitive coinduction is, I'm afraid I'd fool myself when attempting a proof.

[1] Łukasz Czajka, 2014. A Coinductive Confluence Proof for Infinitary Lambda-Calculus. Proc. of Rewriting and Typed Lambda Calculi, Springer. <http://www.mimuw.edu.pl/~lukaszcz/coind.pdf>

[2] Jorg Endrullis and Andrew Polonsky, 2011. Infinitary Rewriting Coinductively. In Proc. of TYPES, volume 19 of LIPIcs, pages 16–27. Schloss Dagstuhl. <http://drops.dagstuhl.de/opus/volltexte/2013/3897/>

[3] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries, 1997. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93–125. <http://www.sciencedirect.com/science/article/pii/S0304397596001715>

**Tags:** pl.programming-languages, lambda-calculus, term-rewriting-systems


---

## 1 answers

### Answer by username_1 on 2015-07-07. Score: 2 | Accepted answer

I think you'll find that the exact same proof of Lemma 3 in [1] (the proof itself appears in [2]) concerning $\rightarrow^\infty\_\beta$ also holds for $\rightarrow^\infty\_{\beta\bot}$: indeed, they are defined in the same way from $\rightarrow^\*\_\beta$ and $\rightarrow^\*\_{\beta\bot}$ respectively, which are transitive by definition!

The lemma holds for an arbitrary reflexive-transitive congruence relation in place of $\rightarrow^\*\_{\beta\bot}$, as you can verify in [2] without needing to go into the detail of the coinductive proofs. In particular, the proofs of lemmas 4.1-5 in [2] are unchanged (with extra *induction* cases in 4.4).

> **Comments:**
> **username_0**: Ah thanks! 4.4 is indeed the main step I was missing. Intuitively, even though (by definition) you only do a finite number of steps before recursing into subterms, you can later do more steps at the root.  
> **username_1**: Morally yes. The lemma says you never actually have to.  

---

