Must a function in lambda-calculus which inputs a boolean function be defined in a certian way?

Question

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$)

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.)