[Next]  [Previous]  [Up]  

Problem # 4

Submitted by Richard Statman
Date: 1985
Statement. A fixed point combinator from B  and ω  alone?
Problem Origin. The problem was first posed by Raymond Smullyan.


The combinator ω  satisfies the reduction rule ωx  ⇒  xx  and the combinator B  is as usual Bxyz  ⇒  x(yz)  . Is there an applicative combination of B  and ω  which is a fixed point combinator? The problem was originally proposed in [Smullyan, 1985].

Comments by Richard Statman: Note that ω(Bx ω)  is always a fixed point of x  but it appears that x  cannot be abstracted to give a fixed point combinator Y  such that Y x = x(Y x)  . If it is required that Y x ↠  x(Y x)  as with Turing’s fixed point combinator then it can be shown [Statman, 1993, McCune and Wos, 1991] that no B  ,ω  combination works.

References for # 4

[McCune and Wos, 1991]    McCune, W. and Wos, L. (1991). The absence and the presence of fixed point combinators. Theoretical Computer Science, 87:221–228.

[Smullyan, 1985]    Smullyan, R. (1985). To Mock a Mockingbird. Knopf.

[Statman, 1993]    Statman, R. (1993). Some examples of non-existent combinators. Theoretical Computer Science, 121:441–448.

[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014