Church's encoding of Booleans in simple type theory (STT).
Church defines Booleans as lambda-abstractions which take a value for truth
and a value for falsity. Conversely, the term denoting truth (tt) projects
the first value, the term for falsity (ff) projects the second.
Note
Some standard encodings like if-then-else are only definable as parameterized family of terms in STT, not as polymorphic statements.
Summary
Functions
Returns the simple type of an encoded Boolean, i.e. $\iota\to\iota\to\iota$.
Generates a variable term with the given name corresponding to a Church Boolean.
Operators
Generates the Church Boolean corresponding to the logical conjunction of the Boolean terms associated with the given IDs.
Generates the Church Boolean corresponding to the negation of the Boolean term associated with the given ID.
Generates the Church boolean corresponding to the logical disjunction of the Boolean terms associated with the given IDs.
Functions
@spec b_type() :: ShotDs.Data.Type.t()
Returns the simple type of an encoded Boolean, i.e. $\iota\to\iota\to\iota$.
@spec b_var(ShotDs.Data.Declaration.var_name_t()) :: ShotDs.Data.Term.term_id()
Generates a variable term with the given name corresponding to a Church Boolean.
Operators
@spec b_and(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()
Generates the Church Boolean corresponding to the logical conjunction of the Boolean terms associated with the given IDs.
$$ \mathtt{b\_and} := \lambda PQAB.\text{ }P\text{ }(Q\text{ }A\text{ }B)\text{ }B $$
@spec b_not(ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()
Generates the Church Boolean corresponding to the negation of the Boolean term associated with the given ID.
$$ \mathtt{b\_not} := \lambda PAB.\text{ }P\text{ }B\text{ }A $$
@spec b_or(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()
Generates the Church boolean corresponding to the logical disjunction of the Boolean terms associated with the given IDs.
$$ \mathtt{b\_or} := \lambda PQAB.\text{ }P\text{ }A\text{ }(Q\text{ }A\text{ }B) $$
Values
@spec ff() :: ShotDs.Data.Term.term_id()
Returns the ID of the term corresponding to the Boolean value false.
$$ \mathtt{ff} := \lambda AB.\text{ }B $$
@spec tt() :: ShotDs.Data.Term.term_id()
Returns the ID of the term corresponding to the Boolean value true.
$$ \mathtt{tt} := \lambda AB.\text{ }A $$