# `ShotDs.Stt.Numerals`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/stt/numerals.ex#L1)

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 {: .info}
>
> 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$             |

# `n_type`

```elixir
@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$.

# `num`

```elixir
@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.

# `num_var`

```elixir
@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.

# `numeral?`

```elixir
@spec numeral?(ShotDs.Data.Term.term_id()) :: boolean()
```

Checks whether the term corresponding to the given ID is a valid Church
numeral.

# `mult`

```elixir
@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$$

# `plus`

```elixir
@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)$$

# `succ`

```elixir
@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)$$

---

*Consult [api-reference.md](api-reference.md) for complete listing*