| |
SPECIAL ISSUE:
Selected Papers of the Conference "Typed Lambda Calculi and Applications 2007" (in progress)
|
The Omega Rule is Π11-Complete in the λβ-Calculus
|
©Benedetto Intrigila, University of Rome 2, Italy
©Richard Statman, Carnegie-Mellon University, Pittsburgh, PA, USA
|
Abstract
In a functional calculus, the so called ω-rule states that if two terms
P and Q applied to any closed term N return the same value
(i.e. PN = QN), then they are equal (i.e. P = Q
holds). As it is well known, in the λβ-calculus the ω-rule does
not hold, even when the η-rule (weak extensionality) is added to the
calculus. A long-standing problem of H. Barendregt (1975) concerns the
determination of the logical power of the ω-rule when added to the
λβ-calculus. In this paper we solve the problem, by showing that the
resulting theory is Π11-complete.
|
Publication date: April 27, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(2:6)2009
Hit Counts: 1215 |
 Creative Commons | |
