This question is my best attempt to get at a more general question about what one can get from terms in the lambda calculus.

Using the church encoding, we define booleans by $\texttt{true} = \lambda x,y.x$ and $\texttt{false} = \lambda x,y.y$

Define the set of terms $Bool = \{\texttt{true}, \texttt{false}\}$, and let $Bool \to Bool = \{g \; | \; \text{if } b \in Bool \text{ then } g \; b \in Bool\}$

Let $f$ be a term with the property that if $g \in Bool \to Bool$ then $f \; g$ normalizes to a boolean.

Intuitively, I believe $f$ can be either a constant function or it can use $g$. Precisely: Is it true that any such f satisfies one of the following properties:

  • There exists some term $b \in Bool$ so that for any $g \in Bool \to Bool$, $f \; g = b $

  • There exists some term $b \in Bool$ so that for any $g \in Bool \to Bool$, $f \; g = g \; b $

  • There exists some term $b \in Bool$ so that for any $g \in Bool \to Bool$, $f \; g = not (g \; b) $

  • EDIT: as Derik points out, the above three cases only capture 6 of the 16 set-theoretic functions of type (Bool -> Bool) -> Bool. The point was can $f$ be defined in a way other than those set theoretic ones.

(where $a = b$ means that $a$ normalizes to $b$)


1 Answer 1


If we assume that $g$ normalizes when applied to any Boolean input, then we can apply it to true and false, and then we can can compute any Boolean function of those two values. That is, we can readily produce all $16$ possible set theoretic functions, $2^{2^2}$. Your schemas only cover $6$ of those.

But the story goes further, your definition of $f\in(Bool\to Bool)\to Bool$ does not require that $f$ only apply its argument to Booleans. Similarly, $g\in Bool\to Bool$ does not restrict $g$'s behavior for all other inputs. At this point, there are all kinds of additional possibilities (even when restricting to $Bool\to Bool$ inputs) where $f$ applies its argument to other things and performs some other calculation to ultimately produce a Boolean. So there are many other potential terms. If you want tighter guarantees, you may want to consider looking at typed lambda calculi.

(As a tangent, but an interesting tangent, is the class of sequentially realizable functionals. These include functions which are mathematical functions but which aren't implementable in a "pure" way, i.e. they require things like exceptions or mutable state to be implemented.)

  • $\begingroup$ Thanks, but how is it possible to apply g to something not a boolean, and somehow get a boolean from that value? g applied to non-booleans can be any sort of output. This was the point of my question, even though I feel silly for missing 10 of the 16 set theoretic ones. $\endgroup$
    – while1fork
    Commented Mar 11, 2019 at 4:02
  • $\begingroup$ I think that a better question for me to have asked originally is "can I make a function f such that for any x, (f x) is a boolean other than the constant functions?" $\endgroup$
    – while1fork
    Commented Mar 11, 2019 at 4:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.