Editing System F (section)

== Logic and predicates ==
The <math>\mathsf{Boolean}</math> type is defined as:
<math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, where <math>\alpha</math> is a [[type variable]]. This means: <math>\mathsf{Boolean}</math> is the type of all functions which take as input a type &alpha; and two expressions of type &alpha;, and produce as output an expression of type &alpha; (note that we consider <math>\to</math> to be [[right-associative]].)

The following two definitions for the boolean values <math>\mathbf{T}</math> and <math>\mathbf{F}</math> are used, extending the definition of [[Church encoding#Church Booleans|Church booleans]]:

: <math>\mathbf{T} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^\alpha{.}x</math> <!-- These didn't render without the {}-wrapped around the . -->
: <math>\mathbf{F} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^{\alpha}{.}y</math>

(Note that the above two functions require ''three'' &mdash; not two &mdash; arguments. The latter two should be lambda expressions, but the first one should be a type. This fact is reflected in the fact that the type of these expressions is <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>; the universal quantifier binding the &alpha; corresponds to the &Lambda; binding the alpha in the lambda expression itself. Also, note that <math>\mathsf{Boolean}</math> is a convenient shorthand for <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, but it is not a symbol of System F itself, but rather a "meta-symbol". Likewise, <math> \mathbf{T}</math> and <math> \mathbf{F}</math> are also "meta-symbols", convenient shorthands, of System F "assemblies" (in the [https://books.google.com/books?id=IL-SI67hjI4C&q=Nicolas+Bourbaki Bourbaki sense]); otherwise, if such functions could be named (within System F), then there would be no need for the lambda-expressive apparatus capable of defining functions anonymously and for the [[fixed-point combinator]], which works around that restriction.)

Then, with these two <math>\lambda</math>-terms, we can define some logic operators (which are of type <math> \mathsf{Boolean} \rightarrow \mathsf{Boolean} \rightarrow \mathsf{Boolean}</math>):
: <math>\begin{align}
\mathrm{AND} &= \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, y\, \mathbf{F}\\
\mathrm{OR}  &= \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, \mathbf{T}\, y\\
\mathrm{NOT} &= \lambda x^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, \mathbf{F}\, \mathbf{T} 
\end{align}</math>

Note that in the definitions above, <math>\mathsf{Boolean}</math> is a type argument to <math>x</math>, specifying that the other two parameters that are given to <math>x</math> are of type <math>\mathsf{Boolean}</math>. As in Church encodings, there is no need for an {{mono|IFTHENELSE}} function as one can just use raw <math>\mathsf{Boolean}</math>-typed terms as decision functions. However, if one is requested:
: <math>\mathrm{IFTHENELSE} = \Lambda \alpha.\lambda x^{\mathsf{Boolean}}\lambda y^{\alpha}\lambda z^{\alpha}. x \alpha y z </math>
will do.
A ''predicate'' is a function which returns a <math>\mathsf{Boolean}</math>-typed value. The most fundamental predicate is {{mono|ISZERO}} which returns <math>\mathbf{T}</math> if and only if its argument is the [[Church encoding#Church numerals|Church numeral]] {{mono|0}}:
: <math>\mathrm{ISZERO} = \lambda n^{\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha}{.}n \, \mathsf{Boolean} \, (\lambda x^{\mathsf{Boolean}}{.}\mathbf{F})\, \mathbf{T}</math>