I'm taking a graduate course on the theory of functional programming, based on Paul Taylor's "Practical Foundations of Mathematics." I understand the statement of Tarski's theorem about how for any $\omega$-compelte poset $X$, and any $\omega$-continuous function $T:X\rightarrow X$, that $T$ has a fixed point which is the join of (The statement and proof can be found here).

What I want to know is, how is this applicable, other than being a proof that the Y-combinator exists? It just seems to me that it says "we can use recursion to build a function that is defined for all natural numbers", where we could use some other recursive type for numbers. Doesn't the existence of the Y-combinator show the same thing?


1 Answer 1


If by Tarski's fix point theorem you mean the Knaster–Tarski fixpoint theorem, then it's widely applicable and very general. All you need is a complete lattice and a monotone function on the lattice. There are many rather different examples of those. Tarski-Knaster is for example used in the coinductive definition of bisimilarity. Another application is to construct models of logical formulae (e.g. for logics with fixpoints, such as the modal $\mu$-calculus and the various fixpoint logics that are used to characterise complexity classes). It is also used in set theory and in program analysis.

The Y-combinator on the other hand is a specific piece of syntax in the $\lambda$-calculus. You don't need to prove the existence of the Y-combinator.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.