Part 2: Lean's `Part` Monad

In the previous section we studied the mathematics of domain theory. In this section we will see some code, in the form of Lean’s Part monad, a type constructor which models potentially-nonterminating computations. This section assumes you know functional programming.

1. Introduction

Partiality and nontermination show up all the time in programming, since many programs are designed to run indefinitely (event loops, servers, REPLs), or iterate until some condition that may never be reached. A partial recursive function is a model of a computable function in classical computability theory, and is allowed to be undefined on some of its inputs.

As we discussed in the intro, the core calculus of Lean, the calculus of inductive constructions, is total, and this is needed for consistency of Lean as a proof assistant. To talk about nontermination, Lean provides a type of partial values Part α for any type α.

A value of type Part α is either some value a : α, or a unique undefined value none. This allows us to define partial functions of type α → Part β, or α →. β for short. In Mathlib’s computability theory library, Gödel’s partial recursive functions are defined as a certain class of functions ℕ →. ℕ, where partiality allows for unbounded search, which is the last feature needed for Turing-completeness.

Why not Option?

We said that a value of type Part α is either a value a : α or the special none value, and this sounds a lot like what Option (or Maybe, if you’re a Haskeller) provides. So why do we use Part and how is it different?

An important fact is that nontermination is undecidable; Turing’s halting problem says that in general there is no algorithm which decides whether a given program halts. Nontermination is a special type of failure state in that the program can not tell it is diverging. Given a value a : Option α, we can just pattern match on whether it is some x or none, so this tells us that Option isn’t really capturing nontermination.

On the other hand, a value of type Part α consists of an undecidable proposition asserting its definedness, and a way of extracting a value from a proof of its definedness. Because of this, we can not computably check if a Part value is defined, so this seems to be the right way to express divergence.

2. Part: Its Definition

We described the definition of Part above, but here is the official definition from Mathlib:

structure Part.{u} (α : Type u) : Type u where
  Dom : Prop
  get : Dom → α

It is precisely what we said above, a : Part α consists of a proposition asserting its definedness (Dom), and a way of extracting a value of type α given a proof of Dom (get). The none value has False as its proposition and the principle of explosion as its extraction method:

def none : Part α :=
  ⟨False, False.rec⟩

As you may expect, when Dom is decidable, we can convert a Part value to an Option value:

def toOption (o : Part α) [Decidable o.Dom] : Option α :=
  if h : Dom o then some (o.get h) else none

Importantly, Part α possesses a particular ordering. We begin with a relation $x \in a$ for x : α and a : Part α:

/-- `a ∈ o` means that `o` is defined and equal to `a` -/
protected def Mem (o : Part α) (a : α) : Prop :=
  ∃ h, o.get h = a
instance : Membership α (Part α) :=
  ⟨Part.Mem⟩

If a is undefined, then no x satisfies $x \in a$. If a is defined with value $x_0$, then $x \in a \iff x = x_0$.

Mathlib then makes Part α into a partial ordering as follows:

instance : PartialOrder (Part α) where
  le x y := ∀ i, i ∈ x → i ∈ y
  le_refl _ _ := id
  le_trans _ _ _ f g _ := g _ ∘ f _
  le_antisymm _ _ f g := Part.ext fun _ => ⟨f _, g _⟩

That is, $a \leq b \iff \forall x,\ x \in a \to x \in b$. When $a$ is undefined the hypothesis is vacuous so $a \leq b$, and if $a$ is defined with value $x$ then $a \leq b$ forces $b$ to be defined with the same $x$. If you paid attention to the domain theory section, you may notice that Part α is exactly the flat domain on α, sometimes denoted $\alpha_\bot$. $\bot \leq$ anything, and two defined values are comparable only when they are equal. Immediately we see where domain theory begins to play a role here.

The type constructor which takes a type to its flat domain turns out to be a monad, whose API we will explore next.

3. Part as a Monad

To get a monad on the type Part α, we need a way of lifting pure values of type α into the monad (pure), and a way of sequencing monadic computations (bind). The monadic “effect” here is nontermination, so the intuition is that bind propagates nontermination. That is, given s1 : Part α and s2 : α → Part β, sequencing them as

do
  let x ← s1
  s2 x

should evaluate as “if s1 diverges, then diverge; otherwise extract its value x and run s2 x.”

The pure function (called some in the Mathlib API) is pretty trivial, per usual. Its type is some : α → Part α, and is defined as $a \mapsto \langle \text{True},\ \lambda _.\ a\rangle$:

def some (a : α) : Part α :=
  ⟨True, fun _ => a⟩

bind : Part α → (α → Part β) → Part β is a bit trickier, but makes sense once you break it down. Given a partial value p : Part α and a function f : α → Part β, p >>= f should be defined when p is defined, and should apply f to the extracted value. Mathlib defines a helper function assert:

/-- `assert p f` is a bind-like operation which appends an additional condition
  `p` to the domain and uses `f` to produce the value. -/
def assert (p : Prop) (f : p → Part α) : Part α :=
  ⟨∃ h : p, (f h).Dom, fun ha => (f ha.fst).get ha.snd⟩

and bind is then:

/-- The bind operation has value `g (f.get)`, and is defined when all the
  parts are defined. -/
def bind (f : Part α) (g : α → Part β) : Part β :=
  assert (Dom f) fun b => g (f.get b)

Since Part is a monad, it is in particular a functor, meaning you can map functions over partial values:

def map (f : α → β) (o : Part α) : Part β :=
  ⟨o.Dom, f ∘ o.get⟩

4. Continuity, Least Fixed Points, and Scott Induction with Part

We have now seen that Part is a flat domain and a monad. In this section we apply the domain theory from Part 1 and define a (possibly) nonterminating function as a least fixed point of a continuous functional on α → Part β (Kleene’s theorem), and Scott induction gives us a way to reason about it. Mathlib packages the ω-cpo structure and the fixpoint operator Part.fix, but Scott induction is missing, so we prove it ourselves and apply it to a classic example.

Part.fix and Kleene’s theorem

The type α → Part β is exactly the “partial functions from $X$ to $Y$” domain from the first example in Part 1, with $\bot$ the nowhere-defined function.

Mathlib’s fixed-point operator is Part.fix, which takes a functional g : (α → Part β) → (α → Part β) and produces a candidate least fixed point. When g is ω-Scott continuous, Mathlib’s fix_eq_ωSup_of_ωScottContinuous says Part.fix g is the lub of the approximation chain $\bot,\ g\,\bot,\ g\,(g\,\bot),\ \ldots$ So Part.fix is the least fixed point of g. What’s missing is a principle for reasoning about it.

Scott induction

Most generally we can define lfp and Scott induction on an arbitrary ω-cpo with bottom, and then instantiate the result to Part.fix. Fix an ω-Scott continuous f : α →𝒄 α and define the least fixed point per Kleene:

def lfp : α := ωSup (iterateChain f.toOrderHom ⊥ bot_le)

Mathlib already has the two parts of the least-fixed-point property for this construction: that lfp f is a fixed point, and that it sits below every other fixed point.

theorem map_lfp : f (lfp f) = lfp f :=
  ωSup_iterate_mem_fixedPoint f ⊥ bot_le

theorem lfp_le_fixed {a : α} (h : f a = a) : lfp f ≤ a :=
  ωSup_iterate_le_fixedPoint f ⊥ bot_le h bot_le

theorem isLeast_lfp : IsLeast (fixedPoints f) (lfp f) :=
  ⟨map_lfp f, fun _ ha => lfp_le_fixed f ha⟩

Scott induction now follows by unfolding the definition of lfp and reducing to an induction over the approximation chain:

theorem lfp_induction {p : α → Prop} (h_bot : p ⊥) (h_step : ∀ a, p a → p (f a))
    (h_sup : ∀ c : Chain α, (∀ n, p (c n)) → p (ωSup c)) : p (lfp f) := by
  apply h_sup
  intro n
  induction n with
  | zero => exact h_bot
  | succ k ih =>
    have hstep : iterateChain f.toOrderHom ⊥ bot_le (k + 1) =
        f (iterateChain f.toOrderHom ⊥ bot_le k) :=
      Function.iterate_succ_apply' ..
    rw [hstep]
    exact h_step _ ih

This is exactly the proof sketch from Part 1: every iterate $f^n(\bot)$ satisfies $p$ by induction on $n$, and chain-closure finishes.

Specializing Scott induction to Part.fix

To reuse lfp_induction for Part.fix g, we need Part.fix g = lfp (.ofFun g hc). Mathlib’s approximation chain for Part.fix turns out to be definitionally the same as our iterateChain, so once we identify them the rest is straightforward:

theorem fix_eq_lfp' (hc : ωScottContinuous g) :
    Part.fix g = ContinuousHom.lfp (.ofFun g hc) := by
  have h : approxChain (⟨g, hc.monotone⟩ : (∀ a, Part (β a)) →o _) =
      fixedPoints.iterateChain ⟨g, hc.monotone⟩ ⊥ bot_le := by
    apply Chain.ext
    funext n
    change Fix.approx _ n = g^[n] ⊥
    induction n with
    | zero => rfl
    | succ n ih =>
      change g (Fix.approx _ n) = g^[n + 1] ⊥
      rw [ih, ← Function.iterate_succ_apply' g n ⊥]
  rw [fix_eq_ωSup_of_ωScottContinuous hc]
  change _ = ωSup _
  rw [h]
  rfl

And now Scott induction for Part.fix.

theorem fix_scott_induction {p : (∀ a, Part (β a)) → Prop} (hc : ωScottContinuous g)
    (h_bot : p ⊥) (h_step : ∀ f, p f → p (g f))
    (h_sup : ∀ c : Chain (∀ a, Part (β a)), (∀ n, p (c n)) → p (ωSup c)) :
    p (Part.fix g) := by
  rw [fix_eq_lfp' hc]
  exact ContinuousHom.lfp_induction _ h_bot h_step h_sup

A useful corollary

Most of the time we don’t want to prove a property of the whole fixed-point function, we want to prove a property of specific values y ∈ Part.fix g x. Specializing Scott induction to a predicate of the form p f := ∀ x y, y ∈ f x → P x y is a nice setting because two of the three Scott-induction obligations collapse for free. Bottom is vacuous since ⊥ x = Part.none has no members. The chain case follows from how Part lubs work pointwise, namely y ∈ ωSup c x iff y ∈ c n x for some n. Only the step case is left for the user.

theorem fix_induction_mem_of_continuous (hc : ωScottContinuous g)
    {P : ∀ a, β a → Prop}
    (h_step : ∀ f, (∀ x y, y ∈ f x → P x y) → ∀ x y, y ∈ g f x → P x y)
    {x} {y : β x} (h : y ∈ Part.fix g x) : P x y := by
  apply fix_scott_induction (p := fun f => ∀ x y, y ∈ f x → P x y) hc
  · intro _ _ hy; exact absurd hy (Part.notMem_none _)
  · exact h_step
  · intro c ih x y hy
    have hy' : y ∈ ωSup (c.map (Pi.evalOrderHom x)) := hy
    rw [Part.mem_ωSup] at hy'
    obtain ⟨n, hn⟩ := hy'
    exact ih n x y (hn.symm ▸ Part.mem_some y)

This is the exact form we’ll use in Part 3 to discharge the while case of soundness for our toy language. The continuity hypothesis is real, but at use sites it’s discharged by showing the loop body is built from continuous pieces. Mathlib also has a continuity-free version that goes through the approximation chain directly, which is part of an in-flight Mathlib PR, but the Scott-induction route makes the connection to the principle we just built more visible.

Example: Collatz

To see what this buys us, consider the Collatz function:

The open Collatz conjecture says we don’t know whether c terminates on every input. Lean will give you a hard time if you try and define a function which doesn’t clearly terminate. In this case the recursion has no decreasing measure. But Part.fix just gives us a least fixed point of the main body of the function, which is a well-defined object. Below is the definition of the “collatz functional”, a continuous function on (ℕ → Part ℕ)

def collatzF (f : ℕ → Part ℕ) : ℕ → Part ℕ := fun n =>
  if n = 1 then Part.some 1
  else if n % 2 = 0 then f (n / 2)
  else f (3 * n + 1)

def collatz : ℕ → Part ℕ := Part.fix collatzF

Continuity is immediate: each branch is either a constant or a projection to a specific argument, and Mathlib’s ωScottContinuous API composes those automatically:

theorem collatzF_continuous : ωScottContinuous collatzF := by
  apply ωScottContinuous.of_apply₂
  intro n
  unfold collatzF
  split_ifs
  · exact ωScottContinuous.const
  · exact ωScottContinuous.apply (n / 2)
  · exact ωScottContinuous.apply (3 * n + 1)

So collatz is the least fixed point of collatzF:

theorem collatz_eq_lfp :
    collatz = ContinuousHom.lfp (.ofFun collatzF collatzF_continuous) :=
  fix_eq_lfp' collatzF_continuous

theorem collatz_isLeast : IsLeast (Function.fixedPoints collatzF) collatz := by
  rw [collatz_eq_lfp]
  exact ContinuousHom.isLeast_lfp (.ofFun collatzF collatzF_continuous)

Obviously we cannot prove collatz n = Part.some 1 for all n, as that would settle the Collatz conjecture. But we can prove partial correctness: if collatz n terminates with value $x$, then $x = 1$. In our notation this is x ∈ collatz n → x = 1, and we prove it using Scott induction.

The predicate we induct on is

Check that it is admissible:

• Bottom. At $f = \bot$, $x \in \bot(n)$ unfolds to $x \in$ Part.none, which is False. Vacuously true.
• Chain closure. If $x \in (\bigsqcup_i f_i)(n)$ then $x \in f_i(n)$ for some $i$ (lubs of Part chains are computed pointwise on the flat domain), and $P(f_i)$ gives $x = 1$.
• Step. Assume $P(f)$ and split collatzF f n on its three branches: in the $n = 1$ branch the value is literally $1$; in the other two the value comes from $f(n/2)$ or $f(3n+1)$, and $P(f)$ closes both.

The bottom and sup cases are the same boilerplate for any predicate of the form “every output value has property $Q$”, so Mathlib provides a pointwise specialization fix_scott_induction_pointwise that bundles them, leaving only the step:

theorem collatz_one_if_terminates (x n : ℕ) : x ∈ collatz n → x = 1 := by
  apply Part.fix_scott_induction_pointwise (P := fun _ y => y = 1)
  intro f ih n y hy
  unfold collatzF at hy
  split_ifs at hy with h1 h2
  · exact Part.mem_some_iff.mp hy
  · exact ih _ _ hy
  · exact ih _ _ hy

5. Conclusion

In this section we covered the Part definition, the flat-domain order, the monad structure, and Part.fix for defining functions by fixed-point equations. We also built Scott induction for Part.fix and used it to prove a property of the Collatz functiom.

In Part 3 we use all of this to give denotational semantics to a small imperative language with while loops. Commands will denote partial state transformers in State →. State, loops will be interpreted via Part.fix, and Scott induction will come back as the main reasoning principle.

6. References

• Mathlib4, the Lean community mathematical library, in particular Mathlib.Data.Part, Mathlib.Order.OmegaCompletePartialOrder, and Mathlib.Control.LawfulFix.