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

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:***

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