Encodes Church numerals in simple type theory.
Church numerals are defined as lambda-abstractions which take a successor function $S_{\iota\to\iota}$ and a starting point $Z_\iota$ and returns the n-fold application of the successor function to the starting point. I.e., in our encoding, numerals are represented as a term of type $(\iota\to\iota)\to\iota\to\iota$.
Simple arithmetic operators can be defined ontop of this encoding as Church numerals correspond to iterators. Some examples of this are implemented in this module.
Note
Some functions are not definable without polymorphism. This includes for example the predecessor function, subtraction and exponentiation.
Some examples ($S^{\circ n}$ represents that $S$ is applied $n$ times):
| Number | Encoding |
|---|---|
| 0 | $\lambda SZ.\text{ }Z$ |
| 1 | $\lambda SZ.\text{ }S\text{ }Z$ |
| 2 | $\lambda SZ.\text{ }S\text{ }(S\text{ }Z)$ |
| 3 | $\lambda SZ.\text{ }S\text{ }(S\text{ }(S\text{ }Z))$ |
| $\vdots$ | $\vdots$ |
| $n$ | $\lambda SZ.\text{ }S^{\circ n}\text{ }Z$ |
Summary
Functions
Returns the simple type corresponding to an encoded numeral, i.e., $(\iota\to\iota)\to\iota\to\iota$.
Generates the Church numeral corresponding to the given natural number. Returns the ID of the generated term.
Generates a variable term with the given name corresponding to a church numeral.
Checks whether the term corresponding to the given ID is a valid Church numeral.
Operators
Generates the Church numeral corresponding to the multiplication of the terms with the given IDs. Returns the ID of the resulting term.
Generates the Church numeral corresponding to the addition of the terms with the given IDs. Returns the ID of the resulting term.
Generates the successor of the Church numeral term corresponding to the given ID. Returns the ID of the generated term.
Functions
@spec n_type() :: ShotDs.Data.Type.t()
Returns the simple type corresponding to an encoded numeral, i.e., $(\iota\to\iota)\to\iota\to\iota$.
@spec num(non_neg_integer()) :: ShotDs.Data.Term.term_id()
Generates the Church numeral corresponding to the given natural number. Returns the ID of the generated term.
@spec num_var(ShotDs.Data.Declaration.var_name_t()) :: ShotDs.Data.Term.term_id()
Generates a variable term with the given name corresponding to a church numeral.
@spec numeral?(ShotDs.Data.Term.term_id()) :: boolean()
Checks whether the term corresponding to the given ID is a valid Church numeral.
Operators
@spec mult(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()
Generates the Church numeral corresponding to the multiplication of the terms with the given IDs. Returns the ID of the resulting term.
$$ \mathtt{mult} := \lambda MNSZ.\text{ }M\text{ }(N\text{ }S)\text{ }Z $$
@spec plus(ShotDs.Data.Term.term_id(), ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()
Generates the Church numeral corresponding to the addition of the terms with the given IDs. Returns the ID of the resulting term.
$$ \mathtt{plus} := \lambda MNSZ.\text{ }M\text{ }S\text{ }(N\text{ }S\text{ }Z) $$
@spec succ(ShotDs.Data.Term.term_id()) :: ShotDs.Data.Term.term_id()
Generates the successor of the Church numeral term corresponding to the given ID. Returns the ID of the generated term.
$$ \mathtt{succ} := \lambda NSZ.\text{ }S\text{ }(N\text{ }S\text{ }Z) $$