[Solved]: What does Tarski's Fixed-Point theorem give us that that Y-Combinator does't

Problem Detail: 

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?

Asked By : jmite

Answered By : Martin Berger

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/23431

3.2K people like this

 Download Related Notes/Documents