What is the $\mu$ in the labmda calculus defined here?

Question

In the Lambda: Introduction to Lambda Calculus chapter of PLFA, it has the following definition for the lambda calculus, which includes a $\mu$ operator that I haven't seen before.

Syntax of terms

Terms have seven constructs. Three are for the core lambda calculus:

Variables ` x
Abstractions ƛ x ⇒ N
Applications L · M

Three are for the naturals:

Zero `zero
Successor `suc M
Case case L [zero⇒ M |suc x ⇒ N ]

And one is for recursion:

Fixpoint μ x ⇒ M

In above, the first group of terms are the classic lambda calculus. The second group seems to be an add-on for natural numbers. I can understand the first two groups. But the third group with the fixpoint and $\mu$ is what I don't understand.

There is also an example of using it:

plus : Term
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
         case ` "m"
           [zero⇒ ` "n"
           |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]

, which didn't have much explanation about the $\mu$.

I searched around trying to find out what the $\mu$ is. Is this the $\lambda\mu$-calculus discussed in this question? I saw a lot of discussions here and there about continuation, control and classic logic, and I don't really see how it's connected to the recursive definition of plus above.

My questions are:

What is the $\mu$ in above definition of lambda calculus (what is the associated formal system)?

Why is it necessary for defining recursion? Isn't it there already some Y combinator in the lambda calculus for defining recursion?

How does it work in the definition of plus?

Answer 1

What is the $\mu$ in above definition of lambda calculus (what is the associated formal system)?

This system is (a variation of) the language PCF. This language has been a landmark in the study of (denotational) semantic since its introduction by Plotkin in the 70's. The $\mu$ operation, also often named fix (or sometimes even $Y$) is a fixed point operator, similar to the $Y$ of the pure λ-calculus. The rest of the language is a pure functional part (similar to λ-calculus), and a few primitive operations for a base type of natural numbers. Moreover, programs in PCF have (simple) types: one is interested only in well-typed programs, which have type either $\mathbb{N}$ or $\sigma \to \tau$ where $\sigma$ and $\tau$ are two types. You can view PCF as some sort of very simplified version of languages of the ML family (standard ML, OCaml…).

This has nothing to do with the λμ-calculus which is a completely different system for a completely different purpose.

Why is it necessary for defining recursion? Isn't it there already some Y combinator in the lambda calculus for defining recursion?

Because PCF is a simply-typed language: under this restriction it is not possible to use the combinator $Y$ (or any other fixed-point operator from λ-calculus, actually), because it is ill-typed. Thus, the solution is to add to the language a primitive operation to take fixed points. Usually, one simply adds a constant of type $(\tau \to \tau) \to \tau$ for all types $\tau$ (so this is really a family of constants, one for each type). Here, it seems like things are done slightly differently, I would guess that $\mu$ takes a body of type $\tau$ in a context extended by a variable of type $\tau$, and build a term of type $\tau$. In other words, its typing rule is $$ \frac{\Gamma, x : \tau \vdash M : \tau}{\Gamma \vdash \mu x.M : \tau} $$ This $\mu x.M$ would behave roughly like $Y (\lambda x . M)$ in pure λ-calculus.

How does it work in the definition of plus?

We are defining + as a recursive function, such that + 0 y is y and + (suc x') y is suc (+ x' y). Defining such a recursive function is technically roughly the same as taking a fixed point. If you know OCaml, this definition is more or less equivalent to writing

let rec plus = fun x y ->
  match x with
  | 0 -> y
  | x -> 1 + (plus (x-1) y)

Answer 2

Here are a few rough and non-expert answers, I hope it will help at least a bit.

What is the μ in above definition of lambda calculus (what is the associated formal system)?

The $\mu$ classically denotes the least fix-point construction, see Wikipedia or the nLab for instance. (It is not the $\mu$ from the $λ\mu$-calculus; this ambiguity is an unfortunate accident.)

Intuitively, if you work with sets and you have a map $f$ taking sets $X$ to sets $f(X)$, then $\mu X.f(X)$ is the smallest set $X$ such that $X = f(X)$. Of course such a set doesn't always exist, but there are standard conditions ensuring it is the case (in a lattice- or category-theoretic setting). For instance $\mathbf{N} = \mu X.1+X$, where $+$ denotes disjoint union and $1 = \{0\}$.

Then given such a least fix-point, any map $a : f(Y) \to Y$ for some other set $Y$, defines a unique map $\mu a : \mu X.f(X) \to Y$. See here for instance for more details. The $\mu$ you are wondering about is this one (see below for the example of the addition).

Why is it necessary for defining recursion? Isn't it there already some Y combinator in the lambda calculus for defining recursion?

It is not necessary to define recursion, as you underline. But here you do not want to "encode" recursion: you want it built-in, hence you define an explicit constructor for recursion. This is what they write in the introduction: "Church had a minimal base type with no operations. We will instead echo Plotkin’s Programmable Computable Functions (PCF), and add operations on natural numbers and recursive function definitions."

The main benefit of this approach is that you can work in a (simply) typed setting, whereas it is not possible to give a simple type to $Y$.

How does it work in the definition of plus?

What they give is just the recursive construction of the addition. Thanks to currying, addition is defined as a map $\mathbf{N} \to (\mathbf{N} \to \mathbf{N})$, by induction on its first argument. Explicitely, the map $$\begin{array}{ccc} 1 + (\mathbf{N} \to \mathbf{N}) & \to & (\mathbf{N} \to \mathbf{N}) \\ 0 & \mapsto & (n \mapsto n) \\ \mathrm{add}_m & \mapsto & (n \mapsto \mathrm{succ}(\mathrm{add}_m(n))) \end{array}$$ defines a unique map $\mathrm{add} : \mathbf{N} \to (\mathbf{N} \to \mathbf{N})$, as said above. Observe that this exactly corresponds to the code you give.

---

(I know my answer is a bit blurry, I'll elaborate later when I have some more time. Please tell me what is unclear so that I can improve it the better I can.)