Confluence for the untyped lambda calculus, shown using Takahashi translation with three different methods: Tait and Martin-Löf (1971), Komori-Matsuda-Yamakawa (2014), and the proof by Dehornoy-van Oostrom (2008) later formalized in Nagele-van Oostrom-Sternagel (2016). This code reuses (a simplified version of) the infrastructure for λ-terms and substitutions provided by the PLFA book.
- DeBruijn: untyped lambda terms with De Bruijn indices.
- Substitution: a simplified version of the σ-calculus for explicit substitutions from PLFA, used to show the substitution lemma.
- Beta: β-reduction, both one-step and its transitive reflexive closure.
-
BetaSubstitutivity: β-reduction for substitutions and substitutivity of β-reduction, i.e.:
$M \to^*_\beta M'$ and$N \to^*_\beta N'$ implies$M[N] \to^*_\beta M'[N']$ . - Parallel: one-step and many-steps parallel reduction and conversion with β-reduction.
- Takahashi: Takahashi translation of a term.
- ConfluenceParallel: classic Tait and Martin-Löf method with parallel reduction.
- ConfluenceParallelTakahashi: parallel reduction with the diamond lemma on Takahashi translation.
- ConfluenceTakahashi: Komori-Matsuda-Yamakawa proof, just employing Takahashi translation and no parallel reduction.
- ConfluenceZ: (semi-)confluence by the Z property, using Takahashi translation as map.
Tested with Agda 2.6.2.