# Why are there two not operators in lambda calculus?

From Wikipedia:

$$\mathrm{true} = \lambda a. \lambda b. a$$
$$\mathrm{false} = \lambda a. \lambda b. b$$

Because true and false choose the first or second parameter they may be combined to provide logic operators. Note that there are two version of not, depending on the evaluation strategy that is chosen.

$$\mathrm{and} = \lambda p . \lambda q . p \, q \, p$$
$$\mathrm{or} = \lambda p . \lambda q . p \, p \, q$$

$$\mathrm{not}_A = \lambda p . \lambda a . \lambda b . p \, b \, a$$   (This is only a correct implementation if the evaluation strategy is applicative order.)

$$\mathrm{not}_N = \lambda p . p \, (\lambda a . \lambda b . b) \, (\lambda a . \lambda b . a) = \lambda p . p \, \mathrm{false} \, ⁡\mathrm{true}⁡$$   (This is only a correct implementation if the evaluation strategy is normal order.)

I know what applicative order and normal order are (eager evaluation vs lazy evaluation of arguments to functions). But I don’t understand why the two nots don’t work in both of these evaluation strategies.

• Doesn't make sense to me either. The lambda calculus is confluent and all terms involved are normalizable, so why would the reduction strategy matter? You aren't the first to wonder. Jan 2 '19 at 22:53

The lambda-calculus is confluent. All the terms involved are strongly normalizing (these boolean encodings only work on booleans; they could do anything if applied to a lambda-term that doesn't reduce to $$\mathrm{true}$$ or $$\mathrm{false}$$). So the choice of reduction strategy is not relevant.

When something looks weird or incomprehensible on Wikipedia, check the history. Sometimes things get deformed over successive edits, and sometimes an edit is just wrong. WikiBlame can be very useful for that.

The edit that introduced the distinction between two evaluation strategy is from September 2012. It has no edit description, its content doesn't make sense (it implies that call-by-value is not an applicative-order strategy), and even the author was clearly not sure what they wrote (they left a comment with an interrogation).

The bit about normal order was added in December 2013 which was part of a series of edits mainly to improve the formatting and the wording. It doesn't look to me like the editor meant to change the meaning of the article, but they were mislead by the previous edit.

Hopefully someone will soon edit this article to rectify it, ideally with references for both of the not functions.

Incidentally, the choice of reduction strategy does matter if you want to extend these functions outside the booleans. For example, if you want to have $$\mathrm{if}\,b\,M\,N$$ where $$b$$ is a boolean (a term that reduces to $$\mathrm{true}$$ or $$\mathrm{false}$$) and $$M$$ and $$N$$ are arbitrary terms, then this behaves differently depending on the evaluation strategy. With call-by-value, this only terminates if $$M$$ and $$N$$ terminates. With call-by-name, this terminates if whichever of $$M$$ or $$N$$ is selected terminates, and the one that isn't selected doesn't matter. This is the reason why if can be defined as a function in languages that use call-by-name or lazy evaluation such as Haskell, but it needs to be a special form in languages that use eager evaluation such as Lisp and ML.

Another case where the evaluation strategy matters is if you want to work on partial booleans, that is, terms that either reduce to one of $$\mathrm{true}$$ or $$\mathrm{false}$$ or don't terminate ($$\bot$$). For $$\mathrm{not}$$, the choice of evalation strategy doesn't matter: $$\mathrm{not}\,\bot = \bot$$ anyway. For an operator like $$\mathrm{or}$$, the evaluation order does matter: $$\mathrm{or} \, \mathrm{true} \, \bot$$ could be either $$\mathrm{true}$$ or $$\bot$$, and likewise for $$\mathrm{or} \, \bot \, \mathrm{true}$$. With eager evaluation, they're both $$\bot$$, but with left-to-right normal order $$\mathrm{or} \, \mathrm{true} \, \bot \to \mathrm{true}$$ while $$\mathrm{or} \, \bot \, \mathrm{true}$$ does not terminate. It's natural to wonder if there could be a more clever implementation of $$\mathrm{or}$$ that always picks its terminating argument regardless of the evaluation strategy. This problem is known as Plotkin's parallel or, and it's an important result in the theory of the lambda calculus that there is no such term. There is no way for a lambda calculus function to take two arguments and evaluate them “in parallel”, reducing them and stopping as soon as one of them terminates. The function can be weakly normalizing (it terminates in some evaluation strategies) but not strongly normalizing (there are evaluation strategies where it doesn't terminate). Thus the lambda calculus is said to be inherently sequential. It's a very nice model of sequential computation, but if you want to model parallelism or concurrency, you need other tools.

• I don’t understand how lambda calculus can’t do concurrency; Wouldn’t this void the Church-Turing thesis? Jan 3 '19 at 6:07
• My experience with editing Wikipedia articles is entirely negative. I suspect I am not alone, which is why nonsense on $\lambda$-calculus can go unedited for years. Jan 3 '19 at 7:26
• @HappyFace The Church-Turing thesis says that all methods of computation are equivalent, but that's based on observing only the inputs and the result. Concurrency looks at the steps to get to the result, and is even usually not particularly interested in the final result, but at the steps to getting there. Computation methods are not equivalent when you consider internal steps important. Jan 3 '19 at 7:27
• @Gilles So there should be an or operator in lambda calculus whose output is the same as the parallel or, shouldn’t there? Jan 3 '19 at 7:31
• @HappyFace No, if you add a parallel or operator then what you get is no longer equivalent to the lambda calculus and other methods of sequential computation. Unlike the case of sequential computation, for which all models are different ways to express the same things, there are a lot of different concurrent calculi with different expressive power. Concurrency is intrinsically more diverse and more complex than sequential computation. Jan 3 '19 at 7:39