Solution of a Problem of Barendregt on Sensible lambda-Theories
Benedetto Intrigila, Richard Statman
TL;DR
This paper proves Barendregt's conjecture that the provable equations in the closure of the theory H, which extends beta-conversion by identifying all closed unsolvables, form a -complete set, advancing understanding of lambda-theories.
Contribution
The paper confirms Barendregt's long-standing conjecture that the provable equations in H are -complete, providing a significant theoretical result in lambda-calculus.
Findings
Proves Barendregt's conjecture about H
Shows provable equations form a -complete set
Advances understanding of lambda-theories and their computational complexity
Abstract
<i>H</i> is the theory extending β-conversion by identifying all closed unsolvables. <i>H</i>ω is the closure of this theory under the ω-rule (and β-conversion). A long-standing conjecture of H. Barendregt states that the provable equations of <i>H</i>ω form Π<sub>1</sub><sup>1</sup>-complete set. Here we prove that conjecture.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.