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}}\\)]