Skip to content

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book

License

Notifications You must be signed in to change notification settings

iwilare/church-rosser

Repository files navigation

Formalizations of the Church-Rosser Theorem in Agda

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.

Files structure

Terms

Semantics

  • 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.

Confluence

  • 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.

Version

Tested with Agda 2.6.2.

About

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book

Topics

Resources

License

Stars

Watchers

Forks

Languages