Hey Reuben,

First of all, excellent job!

Second, I should offer some explanation. I was cheating a bit. Let me explain.

If \$$f\$$ is monotonic on some meet-complete semi lattice \$$L\$$, then \$$\mu f := \bigwedge \\{x\ :\ f(x) \leq_L x \\}\$$ is called \$$f\$$'s "Least Fixed Point". This is from the [Knaster-Tarski Theorem](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem).

Now \$$\mu f\$$ obeys the equation:

$$\mu f = f (\mu f)$$

In general in mathematics, when \$$f(x) = x\$$, we say \$$x\$$ is a fixed-point for \$$f\$$. So \$$\mu\$$ is often referred to as the "least fixed point operator". In Haskell, it is defined in the prelude and it is called fix.

This operator is essentially the same as the \$$\mathbf{Y}\$$ combinator. The \$$\mathbf{Y}\$$ combinator is also known as the [fixed-point combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator). In particular, it obeys the equation, for any \$$\lambda\$$-term \$$F\$$:

$$Y F \rightleftharpoons_\beta F (Y F)$$

Where \$$\rightleftharpoons_\beta\$$ expresses \$$\beta\$$-equivalence.

Now to how I was cheating. The fact is \$$\mu\$$ is a fixed-point operator for a rather special partial order. For instance, fix (\x -> 2*x-1) will not return 1. See this [stack overflow](https://stackoverflow.com/questions/4787421/how-do-i-use-fix-and-how-does-it-work) for more discussion. The gist is because *undefined*, denoted ⊥, is a possible value and least fixed point for \x -> 2*x - 1. The Haskell wiki has an [introduction to denotational semantics](https://en.wikibooks.org/wiki/Haskell/Denotational_semantics) which presents the relevant partial order \$$\sqsubseteq\$$. Denotational semantics provides the partial order \$$\sqsubseteq\$$ that \$$\mu\$$ operates as a fixed point on.

***In fact, the proper definition of \$$\mu\$$ given the partial order \$$\sqsubseteq\$$ in denotational semantics is:***

\$$\mu f := \bigvee_{\sqsubseteq} \left\\{ \underbrace{f(f(f(\cdots(f}_n(\bot)\cdots))) \ :\ n\in \mathbb{N} \right\\}\$$

...where \$$f\$$ is a special kind of monotonic function called [Scott Continuous](https://en.wikipedia.org/wiki/Scott_continuity). In denotational semantics we only have a [*Directed Complete Partial Order* (**dcpo**)](https://en.wikipedia.org/wiki/Complete_partial_order#Definitions). Arbitrary joins are only guaranteed to exist for [directed sets](https://en.wikipedia.org/wiki/Directed_set). This is why in domain theory we write \$$\bigvee_{\sqsubseteq}\$$ or \$$\text{sup}_{\sqsubseteq}\$$.

*Arbitrary meets are not guaranteed at all!*

With a little coaxing the two fixed-point definitions do coincide. But it involves a little heavy lifting:

**Puzzle 7 (Maybe Hard):** Let \$$(P, \subseteq, \bigvee_{\sqsubseteq})\$$ be a **dcpo**. For a set \$$A \subseteq P\$$ define \$$A^u := \\{p \in P\ :\ \forall a \in A. a \sqsubseteq p\\}\$$ and \$$A^d := \\{p \in P\ :\ \forall a \in A. p \sqsubseteq a\\}\$$. Define the [Dedekind-Macneill completion](https://en.wikipedia.org/wiki/Dedekind%E2%80%93MacNeille_completion) \$$\mathbf{DM}(P) := \\{ A \subseteq P\ :\ A = (A^u)^d \\} \$$; we have \$$\left(\mathbf{DM}(P),\subseteq, \bigcup, \bigcap\right)\$$ is a complete lattice. There is an embedding \$$\downarrow: P \to \mathbf{DM}(P) \$$ where \$$x\downarrow := \\{x\\}^d\$$. Further, all Scott continuous functions \$$f: P \to P\$$ can be lifted into monotonic functions \$$f^\mathbf{DM}: \mathbf{DM}(P) \to \mathbf{DM}(P)\$$ with \$$f^\mathbf{DM}(A) := ((f_!(A))^u)^d\$$ (where \$$f_!\$$ is the push-forward of \$$f\$$ that John Baez introduces in [lecture 9](https://forum.azimuthproject.org/discussion/1931/lecture-9-the-logic-of-subsets)). *Show as an exercise*:

$$\left(\bigvee_{\sqsubseteq} \left\\{ \underbrace{f(f(f(\cdots(f}_n(\bot)))) \ :\ n\in \mathbb{N} \right\\}\right)\Bigg\downarrow = \bigcap\\{A \in \mathbf{DM}(P)\ :\ f^\mathbf{DM}(A) \subseteq A \\}$$

...So least fixed points from the Knaster-Tarski theorem coincide with least fixed points from domain theory in the Dedekind-Macneil Completion of a **dcpo**.

However, this is a purely mathematical construction. In programming we can't take Dedekind-Macneil completions and we can't compute arbitrary suprema or minima.

In Haskell when we deal with adjunctions or least fixed points, they are defined by construction.

---------------------------------------------------------------------------------------

There are still connections between least fixed points and adjunctions worth exploring, but I chat about them elsewhere since I think since they are pure math.

There are least fixed point and greatest fixed point type constructors Mu and Nu. [Ralf Hinz (2010)](http://www.cs.ox.ac.uk/ralf.hinze/SSGIP10/AdjointFolds.pdf) has an excellent paper on this worth exploring. Hinz touches on the adjoint relationship between the least fixed point and greatest fixed point.

However, the least fixed point operator for a **dcpo** is a special case of a more general construction in category theory.

Hopefully tomorrow or the day after I will give an exercise where we can build up to this, as well as see the fixed point operator's role in recursion.

[Edit: Added side condition for domain theory fixed point definition that \$$f\$$ needs to be Scott continuous, and using proper definition of \$$f^{\mathbf{DM}}\$$]