3 results
Benedetto Intrigila ; Richard Statman.
In a functional calculus, the so called \Omega-rule states that if two terms P and Q applied to any closed term <i>N</i> return the same value (i.e. PN = QN), then they are equal (i.e. P = Q holds). As it is well known, in the \lambda\beta-calculus the \Omega-rule does not hold, even when the […]
Published on April 27, 2009
Benedetto Intrigila ; Richard Statman.
<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 […]
Published on October 18, 2006
Benedetto Intrigila ; Giulio Manzonetto ; Andrew Polonsky.
The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between B\"ohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two lambda-terms whenever their B\"ohm trees […]
Published on January 29, 2019