# "union" or "disjunction" in pure untyped lambda calculus

In the untyped lambda calculus (with variables, abstraction and application as the only constructors), we have a "pair" construct, given by $$(a, b) = \lambda x, x a b$$. The projections are then $$\pi_i = \lambda x_1 x_2, x_i$$ and there is a product function $$\langle f, g \rangle = \lambda x, (f x, g x)$$.

TL; DR; Do we also have something like that, but for a copair/disjunction/union?

In the essay Relating Theories of the lambda-calculus, Scott constructs (from page 418) a category $$R$$, consisting of all idempotent functions $$A \circ A = A$$. To each of the objects $$A$$, we can attach a 'set of elements', consisting of all the terms $$a$$ such that $$A a = a$$. This category has binary products $$A \times B = \langle A \circ \pi_1, B \circ \pi_2 \rangle$$, with a set of elements consisting of $$x$$ that are equal to $$(a, b)$$ for some element $$a$$ of $$A$$ and $$b$$ of $$B$$. Note that $$A \times B$$ is exactly the product function of the two projections onto $$A$$ and $$B$$.

My main question here is: does this category have binary coproducts $$A \sqcup B$$? Is there a type $$X$$ such that $$X x = x$$ means "$$A x = x$$ or $$B x = x$$" or something like that? Can we construct an idempotent "Bool" which has exactly two elements?

I noticed that we can create injection functions $$\iota_1 = \lambda a x_1 x_2, x_1 (A a)$$ and $$\iota_1 = \lambda b x_1 x_2, x_2 (B b)$$ from $$A$$ and $$B$$ into a coproduct, and that given functions $$f: A \to C$$ and $$g: B \to C$$, we can combine them into a sum function $$[f, g] = \lambda x, x f g$$. However, when I try to take $$A \sqcup B = [\iota_1, \iota_2]$$, just like with the binary product, I sadly get something which is not idempotent. Is what I am trying to do just impossible?

• I thought about it for a week. I can't even find a terminal object without adjoining constants; I'm not sure if we can have 2 = 1 + 1 if we can't even have 1. Excellent question, thanks. Apr 2 at 19:14
• @Corbin Thank you for your time. The terminal object is already given by Scott. It is given by a "constant" function: $\lambda x_1 x_2, x_2$. There is no initial object by the way, because there are always multiple possible functions (for example, all the constant functions) to $\lambda x_1, x_1$. Apr 3 at 12:48

The usual way to encode coproducts is as:

$$ι_1\ x = λk_1\ k_2.\ k_1\ x \\ ι_2\ y = λk_1\ k_2.\ k_2\ y$$

Matching is then, as you said, $$[f,g]= λs.\ s\ f\ g$$.

The obvious problem with idempotence is that you didn't dualize the product. For the product you wrote:

$$A × B = \langle A \circ π_1, B \circ π_2 \rangle$$

The dual of this would be:

$$A + B = [ι_1 \circ A, ι_2 \circ B]$$

However, this still isn't idempotent. For arbitrary $$z$$, we get:

$$(A+B)((A+B)z) = z (ι_1 \circ A) (ι_2 \circ B) (ι_1 \circ A) (ι_2 \circ B)$$

There's no obvious way for the repeated applications to interact and reduce unless $$z$$ is already a 'good' value from the set we haven't yet established.

The obvious difference is that $$A×B$$ always produces something like a pair, but whether the above $$A+B$$ produces something like a disjunct is entirely up to $$z$$. So, we should try to take that out of $$z$$'s hands. If we imagine what $$A+B$$ does in a more standard light, we'd get:

$$(A+B)z = \mathsf{match}\ z\ \mathsf{with} \\ ι_1 x → λl\ r. l\ x \\ ι_2 y → λl\ r. r\ y$$

So, an idea is to instead write this as:

$$(A + B)z = λ l\ r. \mathsf{match}\ z\ \mathsf{with} \\ ι_1 x → l\ x \\ ι_2 y → r\ y$$

Or, in just lambda terms:

$$(A+B) = λs\ l\ r. [l \circ A, r \circ B]\ s$$

Now this is idempotent:

\begin{align} (A&+B)((A+B)z) \\ &= (A+B)(λ l\ r. [l \circ A, r \circ B]\ z) \\ &= λ l\ r. (λ l'\ r'. [l' \circ A, r' \circ B]\ z)\ (l \circ A)\ (r \circ B) \\ &= λ l\ r. [l \circ A \circ A, r \circ B \circ B]\ z \\ &= λ l\ r. [l \circ A, r \circ B]\ z \end{align}

The two constructors also satisfy $$(A+B)(ι_i x) = ι_i x$$ as long as $$x$$ satisfies the relevant equation. For example:

\begin{align} (A &+ B)(ι_1\ x) \\ &= λ l\ r. (λ l'\ r'. l' x) (l \circ A) (r \circ B) \\ &= λ l\ r. l (A x) \\ &= λ l\ r. l x \\ &= ι_1 x\end{align}

I don't know if it satisfies all the properties you want, but perhaps it will work out better.

• This seems to work. Why didn't I think of this myself‽ Apr 3 at 23:25
• It works up to the last part. I only wasn't able to show uniqueness of the coproduct arrow. I.e. I was not able to show that for $f: A \to C$ and $g: B \to C$, for all arrows $h: A + B \to C$ such that $h \circ \iota_1 = f$ and $h \circ \iota_2 = g$, we have $h = C \circ [f, g]$. One of the complications here is that the product arrow $\langle f, g \rangle$ satisfies $\langle f, g \rangle \circ a = \langle f \circ a, g \circ a \rangle$, but the coproduct arrow does not satisfy (afaik) $a \circ [f, g] = [a \circ f, a \circ g]$. Apr 5 at 7:33
• Yeah, it may just not work out. One other thing I noticed is that if you do this for booleans, you get $\mathsf{Bool}\ b = λ f\ t. b\ f\ t$. But then $\mathsf{Bool}\ b = b$ is just the eta rule that all lambda terms are expected to satisfy. Apr 5 at 15:19
• Oh, that is not what we wanted indeed. I also realized that Paul Taylor in his dissertation proved that the category of retracts cannot have coproducts (if we have a "nontrivial" lambda-calculus. I.e., if there are at least two distinct lambda-terms): paultaylor.eu/domains/recdic.pdf, 1.5.12, the corollary. Apr 5 at 17:31