2 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 ; 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