Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

More Church-Rosser Proofs in BELUGA

Alberto Momigliano, Martina Sassella

TL;DR

This paper presents a Beluga-based formalization of the Church-Rosser property for lambda-calculus, extending from CR($\beta$) to CR($\eta$) and CR($\beta\eta$), and shows the same proof structure can be ported to System $F$ using intrinsically-typed terms. It leverages HOAS and Beluga's contextual reasoning to achieve modular, elegant encodings of reduction and confluence, including a meta-level discussion and a logic-programming style counterexample search. The results demonstrate Beluga's suitability for mechanizing meta-theoretic proofs and for teaching lambda-calculus, while also highlighting practical limits of meta-level encodings. The work suggests a pathway for more Church-Rosser proofs and for integrating counterexample search into proof environments via tools like QuickChick.

Abstract

We report on yet another formalization of the Church-Rosser property in lambda-calculi, carried out with the proof environment Beluga. After the well-known proofs of confluence for beta-reduction in the untyped settings, with and without Takahashi's complete developments method, we concentrate on eta-reduction and obtain the result for beta-eta modularly. We further extend the analysis to typed-calculi, in particular System F. Finally, we investigate the idea of pursuing the encoding directly in Beluga's meta-logic, as well as the use of Beluga's logic programming engine to search for counterexamples.

More Church-Rosser Proofs in BELUGA

TL;DR

This paper presents a Beluga-based formalization of the Church-Rosser property for lambda-calculus, extending from CR() to CR() and CR(), and shows the same proof structure can be ported to System using intrinsically-typed terms. It leverages HOAS and Beluga's contextual reasoning to achieve modular, elegant encodings of reduction and confluence, including a meta-level discussion and a logic-programming style counterexample search. The results demonstrate Beluga's suitability for mechanizing meta-theoretic proofs and for teaching lambda-calculus, while also highlighting practical limits of meta-level encodings. The work suggests a pathway for more Church-Rosser proofs and for integrating counterexample search into proof environments via tools like QuickChick.

Abstract

We report on yet another formalization of the Church-Rosser property in lambda-calculi, carried out with the proof environment Beluga. After the well-known proofs of confluence for beta-reduction in the untyped settings, with and without Takahashi's complete developments method, we concentrate on eta-reduction and obtain the result for beta-eta modularly. We further extend the analysis to typed-calculi, in particular System F. Finally, we investigate the idea of pursuing the encoding directly in Beluga's meta-logic, as well as the use of Beluga's logic programming engine to search for counterexamples.
Paper Structure (10 sections, 3 theorems, 2 figures)

This paper contains 10 sections, 3 theorems, 2 figures.

Table of Contents

  1. Introduction
  2. Sketch of the Formal Development
  3. CR($\beta$)
  4. CR($\eta$)
  5. CR($\beta\eta$)
  6. Typed Calculi
  7. CR($\beta$) at the Meta-Level
  8. Conclusions
  9. Acknowledgments
  10. Appendix: Counterexamples Search

Key Result

Lemma 2.1

(Strengthening) If $\Gamma, x \vdash M \mathrel{\,\longrightarrow_\eta\,} N$, and $M$ does not depend on $x$, neither does $N$ and $\Gamma \vdash M \mathrel{\,\longrightarrow_\eta\,} N$.

Figures (2)

  • Figure 1: Reflexivity of vs
  • Figure :

Theorems & Definitions (3)

  • Lemma 2.1
  • Lemma 2.2
  • Lemma 2.3: Commutative Union