More Church-Rosser Proofs in BELUGA

TL;DR

This paper presents new formalizations of the Church-Rosser property in lambda-calculi using Beluga, including proofs for beta, eta, and typed calculi like System F, and explores encoding and counterexample search within Beluga.

Contribution

It introduces novel formal proofs of confluence for beta and eta reductions in lambda-calculi within Beluga, extending to typed systems and meta-logic encoding techniques.

Findings

Confluence proofs for beta-reduction in untyped lambda-calculus.

Extension of proofs to eta-reduction and System F.

Use of Beluga's logic programming for counterexample search.

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.