Knights of the Lambda Calculus infinity written as lisp code

Question

Knights of the Lambda Calculus logo have infinity written as (Y F) = (F (Y F))

is this lisp code the same and is it represent infinity too?

(Y (λ (F) (Y F)))

Answer 1

by eta contraction your expression Y (λ f. Y f) is Y Y. Since Y f reduces to f (Y f), we get

Y Y --> Y (Y Y) --> Y Y (Y (Y Y)) --> Y (Y Y) (Y (Y Y)) --> ...

so it is a divergent lambda term.

Y f is not a divergent term in itself. It reduces to f (Y f), where f now takes over. If f ever uses its argument, and is forced to do so by its caller, only then the chain will continue.

Answer 2

Y here is a fixed-point combinator. Given a function f, it returns a value x for which x = f(x). When, instead of writing x, we write Y(f), we have Y(f) = f(Y(f)). In the traditional lambda calculus notation, this is (F (Y F)) = (Y F), which is what you see in the image.

Some numerical functions have one or more fixed points. E.g., fixed point of the (positive) square root function, as well as the square function are 1 and 0.. Some numerical functions, e.g., f(x) → x+1 doesn't have a fixed point. In some formalisms, including the untyped lambda calculus, every function has a fixed point.

This particular fixed-point operator is the Y-combinator, and is described in more detail in various places, including the Wikipedia article linked above. Fixed point operators are important because, among other things, they allow recursive functions to be defined in formalisms such as the untyped lambda calculus.

Answer 3

This equation of the y-combinator actually can be derived via 4-5 reductions starting from this equation, which is also called the canonical combinator,

((lambda (self) (self self)) (lambda (self) (self self)))

To see a concrete result of this infinite recursion one needs to insert a final criterion for the recursion, for example in this kind of primitive-recursive equation:

((lambda(s) (s s 100))
 (lambda(s n)
   (if (zero? n)
     0
     (+ n (s s (- n 1))))))

;Value: 5050

The picture actually represents either the y-combinator or merely this canonical combinator.

This picture was drawn at MIT by implementing an embedded programming language in scheme that had pictures as atomic objects and simple ways to combine pictures, see here .

And at this link is a detailed description of the functional geometry language of the computer scientist Peter Henderson who tried to create a programming language to generate the pictures of Escher and was also used to generate the logo of MIT-SCHEME: