Fixed point combinator

Got it! This site "creationpie.com" uses cookies. You consent to this by clicking on "Got it!" or by continuing to use this website. Note: This appears on each machine/browser from which this site is accessed.

Consider the following puzzle (origin unknown, found Summer 1991) consisting of a self-referential sentence.

In this sentence, the number of occurrences of 0 is ________, of 1 is ________, of 2 is ________, of 3 is ________, of 4 is ________, of 5 is ________, of 6 is ________, of 7 is ________, of 8 is ________, and of 9 is ________.

Fill in the blanks with the appropriate numbers so that the sentence is true.

For example, if you put in 1 for the number of times 1 appears, then 1 now appears 2 times.
This puzzle is a simple constraint logic puzzle.
You are to find a MGU (Most General Unifier) that is a LFP (Least Fixed Point).

Whenever you write a paper, you are trying to achieve a fixed point in paper writing space. That is, you want to write a paper such that when you proof the entire paper, there are not changes to be made.

You paper is done either,

when you reach a fixed point in paper writing space,
or you give up and turn in what you have.

Alonzo Church (1903-1995) was an American logician who invented the lambda calculus.

E = C | X | ( E | E ) | λ x.E

Alan Turing (1912-1954) developed the ideas that proved the limits of computing before the first programmable digital computer was built.

The Church-Turing hypothesis forms the basis of the limits of computation.

Turing used an operational definition of a computing machine that become the basis of modern electronic digital computers.
Church used functions and mathematics for a language that became LISP and formed the foundation of modern functional programming languages.

Both systems can compute the same functions (and have the same limitations).

More: Alan Turing: halting problem

The lambda calculus is a very simple functional language.

E = C | X | ( E | E ) | λ x.E

An expression E is one of the following.

A constant C
A variable X
An application of an expression to an expression as ( E . E )
A function as λ x . E (where x is the argument and E the body of the function)

The purpose of a simple language like lambda calculus is that properties of programming languages need only be proved for a few constructs. Such a proof is called a structural induction proof.

The core text formatting part of a more general text formatting system is typically a functional string-rewriting system with abstraction mechanisms to manage redundancy.

A combinators is a λ expressions with no free variables. Three combinators (S, K and I.) are sufficient, though not efficient, to express the computation of all computable functions.

Combinators and reduction rules
S apply	K select	I identity	notation
S x y z → (x z) (y z)	K x y → x	I x → x	arrow (to/towards)
S = λ x y z . ((x z)(y z))	K = λ x y . x	I = λ x . x	lambda form
S = (λ x.(λ y.(λ z .(x z)(y z))))	K = (λ x. (λ y. x))	I = (λ x. x)	parenthesized

A fixed point is a x for function f (taking parameter x) such that f(x) = x.

Book: Introduction to combinators and lambda calculus. J. R. Hindley, J F Seldin. 978-0521318396.
A fixed point combinator, usually called Y (in lambda calculus, originally by Curry), is a higher order function that takes a function as an argument and returns a fixed point for the argument (if it exists). A combinator is a closed lambda expression in that it has no free variables. In lambda calculus terms, the fixed point combinator can be defined as follows.

Y = λ f . ( λ x . f ( x x )) ( λ x . f ( x x ))

If such a fixed point exists, then

Y(f) = f(Y f)

Y(f) = f(Y f) = f(f(Y(f)))

A text formatting system that can format itself can model this behavior (to any limit desired).