# ShotDs

**ShotDs** defines data structures representing objects from higher-order logic
(HOL). It uses efficient caching of terms via the
[Erlang Term Storage (ETS)](https://www.erlang.org/doc/apps/stdlib/ets.html).
Full semantics, parsing with type inference and pretty-printing are included.

This library adapts the original formulation of the data structures from the
library [HOL](https://hexdocs.pm/hol/readme.html) and the parsing algorithm
from [BeHOLd](https://hexdocs.pm/behold/BeHOLd.html).

## Classical HOL

Classical HOL is an extension of Church's simple type theory (STT) and concerns
the types generated by the following BNF:

$$\tau \coloneqq \iota \mid o \mid \tau\to\tau$$

$o$ is the type for booleans, containing the values $\mathtt{T}$ and
$\mathtt{F}$ while $\iota$ denotes the (nonempty) set of individuals.
UNote that type construction is right-associative, i.e.,
$\alpha\to(\beta\to\gamma) = \alpha\to\beta\to\gamma$.

The terms of classical HOL are those from STT with respect to some HOL
signature containing the necessary logical connectives. We thus have
application and abstraction in the usual sense.

The HOL signature defined by this library contains the following constant
symbols:

$$
\top_o \quad \bot_o \quad \neg_{o\to o} \quad \lor_{o\to o\to o} \quad
\land_{o\to o\to o} \quad \supset_{o\to o\to o} \quad \equiv_{o\to o\to o}
$$

$$
=_{\tau\to\tau\to o} \quad \Pi_{(\tau\to o)\to o}
\quad \Sigma_{(\tau\to o)\to o}
$$

Due to this polymorphism, the parsing algorithm might not be able to infer some
types. Those are assigned unique _type variables_ (represented by references).
However, if the goal type of an entire term (only on the outermost layer) is
unknown, it is unified with type $o$ as terms are assumed to be of boolean type
unless specified otherwise.

## Term Representation

Terms are internally represented as Elixir structs, whereas HOL opted for
Erlang records. Even though structs are slightly less efficient, they offer a
far superior developper experience and are the preferred option in the Elixir
ecosystem. The module
[`ShotDs.Data.Term`](https://hexdocs.pm/shot_ds/ShotDs.Data.Term.html)
describes this representation in detail.

Terms which are created using the provided API are always ensured to be in
$\beta\eta$-normal form, i.e., fully $\beta$-reduced and $\eta$-expanded.
Additionally, bound variables are represented as
[de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index), handling
$\alpha$-equivalence and capture-avoiding substitution implicitly.

Note that terms are represented in _uncurried_ format, i.e.,
$(f\text{ }a\text{ }b)$ will become $f(a, b)$ where $f$ corresponds to the
_head_ and $a$ and $b$ are considered the _arguments_ of the term.

## Term Construction and DSL

Term construction is internally entirely handeled by the modules
[`ShotDs.Stt.TermFactory`](https://hexdocs.pm/shot_ds/ShotDs.Stt.TermFactory.html)
and
[`ShotDs.Stt.Semantics`](https://hexdocs.pm/shot_ds/ShotDs.Stt.Semantics.html).
There are, however, more expressive options available which are implemented on
top of these modules. A domain-specific language (DSL) for constructing HOL
terms is introduced in
[`ShotDs.Hol.Dsl`](https://hexdocs.pm/shot_ds/ShotDs.Hol.Dsl.html). It uses the
unused Elixir operators `&&&`, `|||`, `~>` and `<~>` as shorthand constructors.
The following example illustrates this API:

```elixir
import ShotDs.Hol.Dsl         # contains lambea/2, neg/1, |||/2 and &&&/2
import ShotDs.Hol.Definitions # contains type_o/0

def exclusive_or do
  lambda([type_o(), type_o()], fn x, y ->
    (x ||| y) &&& neg(x &&& y)
  end)
end
```

## TPTP Parsing

Classical HOL with simple types can be represented in the syntax of TPTP's
[TH0](https://doi.org/10.1007/s10817-017-9407-7). A parser for this syntax is
implemented with two different entry points. All connectives and features in
TH0 are supported. Additionally, full type inference is implemented.

The module [`ShotDs.Parser`](https://hexdocs.pm/shot_ds/ShotDs.Parser.html)
handles simple formula strings such as `"?[X : $o]: X => $true"`.

File parsing for TPTP problem files is handeled by
[`ShotDs.Tptp`](https://hexdocs.pm/shot_ds/ShotDs.Tptp.html). Note that parsing
or including files from the [TPTP problem library](https://tptp.org/TPTP/)
requires an environment variable `TPTP_ROOT` which points to the root directory
of the TPTP problem library (may require a reboot for Elixir to recognize).

## Installation

This package can be installed by adding `shot_ds` to your list of dependencies
in `mix.exs`:

```elixir
def deps do
  [
    {:shot_ds, "~> 0.1.0"}
  ]
end
```