Editing Fixed-point combinator (section)

=== Non-standard fixed-point combinators ===

If F is a fixed-point combinator in untyped lambda calculus, then there is:

:<math>\mathsf F=\lambda x. F x = \lambda x. x (F x)= \lambda x. x (x (F x)) = \cdots </math>

Terms that have the same [[Böhm tree]] as a fixed-point combinator, i.e., have the same infinite extension <math>\lambda x.x (x (x \cdots ))</math>, are called ''non-standard fixed-point combinators''. Any fixed-point combinator is also a non-standard one, but not all non-standard fixed-point combinators are fixed-point combinators because some of them fail to satisfy the fixed-point equation that defines the "standard" ones. These combinators are called ''strictly non-standard fixed-point combinators''; an example is the following combinator:
: <math>\mathsf{N = B U (B (B U) B)}</math>
where
: <math>\mathsf B = \lambda x y z.x (y z)</math>
: <math>\mathsf U = \lambda x.x x\ </math>
since
<!-- Ng = (U . (U .) . (.)) g
             = (U . (g .)) (U . (g .)) = 
             =  U (  g .    U . (g .))
             =       g (    U ( (g . g . U . (g .)) ))
             =       g          (g ( g ( U (  g .  g . g . U . (g .) ))))
 -->
:<math>\mathsf N=\lambda x. N x = \lambda x. x (N_2 x)= \lambda x. x (x (x (N_3 x))) = \lambda x. x (x (x (x (x (x (N_4 x)))))) = \cdots </math>
where <math>\mathsf N_i</math> are modifications of <math>\mathsf N</math> created on the fly which add <math>i</math> instances of <math>x</math> at once into the chain while being replaced with <math>\mathsf N_{i+1}</math>.

The set of non-standard fixed-point combinators is not [[recursively enumerable]].<ref name=gold/>