ShotDs

ShotDs defines data structures representing objects from higher-order logic (HOL). It uses efficient caching of terms via the Erlang Term Storage (ETS). 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 and the parsing algorithm from BeHOLd.

This package was developed at the University of Bamberg with the Chair for AI Systems Engineering.

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:

$$ \topo \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 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, 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 and ShotDs.Stt.Semantics. 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. It uses the unused Elixir operators &&&, |||, ~> and <~> as shorthand constructors. The following example illustrates this API:

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. 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 handles simple formula strings such as "?[X : $o]: X => $true".

File parsing for TPTP problem files is handeled by ShotDs.Tptp. Note that parsing or including files from the TPTP problem library 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:

def deps do
  [
    {:shot_ds, "~> 0.2.0"}
  ]
end