BeHOLd

BeHOLd is a library implementing syntax for classical higher-order logic (HOL). It extends the implementation of the simply-typed lambda calculus from the library HOL by logical constants. BeHOLd should only be used together with HOL as custom term and type construction is otherwise not supported. This module also includes a parser for TPTP TH0 syntax.

An overview over the included modules is given in the documentation of the root module.

A demonstration of the package which includes the implementation of classical HOL and the parser can be found in this Livebook.

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

Classical HOL

The type system of classical HOL is given by the following grammar, where it is possible to introduce additional user-defined base types:

$$ \alpha, \beta \coloneqq \iota \mid o \mid \alpha\to\beta $$

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

The parsing algorithm might not be able to infer some types. Those are assigned unique type variables (prefixed with "__uk_") denoting unknown types. 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.

In addition to the simply-typed lambda calculus, classical HOL contains the following constants with the usual interpretation:

$$ \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} $$

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

Note that ${=}_{\alpha\to\alpha\to o}$ (short ${=}^\alpha$), $\Pi_{(\alpha\to o)\to o}$ (short $\Pi^\alpha$) and $\Sigma_{(\alpha\to o)\to o}$ (short $\Sigma^\alpha$) represent families of constants, i.e., there is one of each symbol for every type.

Term Representation

The term representation is entirely handled by the HOL library and described in detail in its documentation. To give a short summary, terms are ensured to always be in $\beta\eta$-normal form, i.e. maximally $\eta$-expanded and $\beta$-reduced until no $\beta$-reductions are possible. Additionally, bound variables in $\lambda$-abstractions are named via de Bruijn indices, i.e., $(\lambda X. \lambda Y. X\text{ }Y)$ is represented as $(\lambda. \lambda. 2\text{ }1)$. This process names bound variables with respect to their scope. I.e., in abstractions occuring in the body of another abstraction, the index of the outer bound variable is raised to match the scope of the inner abstraction.

Internally, terms are represented by the data structure HOL.Data.hol_term() as records with accessor fields for the term's head, arguments, bound variables, free variables, type and highest de Bruijn index. The term head and arguments fields correspond to a flattened representation of the term, e.g. $((f\text{ }a)\text{ }b)$ is repesented as $(f\text{ }a\text{ }b)$ where $f$ is the head and $a$ and $b$ are the arguments. This means, that a term's head is always given as a HOL.Data.declaration() of a constant, bound or free variable.

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.

The module BeHOLd.Parser handles simple formula strings like "?[X : $o]: X => $true".

The module BeHOLd.TPTP handles file parsing for TPTP problem files and contains functionality to convert the internal term representation back to a string in TH0 format. Note that when parsing or including files from the TPTP problem library, a environment variable TPTP_ROOT must be specified pointing to the root folder of the TPTP library (this may require a reboot for Elixir to recognize).

Installation

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

def deps do
  [
    {:behold, "~> 1.1.2"}
  ]
end