Demo of the ShotDs Package

Mix.install([
  {:shot_ds, "~> 1.0"}
])

Installation and Setup

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

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

Note: When parsing files from the TPTP problem library, it is additionally necessary to set up an environment variable TPTP_ROOT pointing to its root directory. This also enables parsing dependencies in TPTP files.

Core Concepts and Architecture

This library models various data structures from classical higher-order logic (HOL) and simple type theory (STT). It relies on (but is not limited to) the two base types $o$ for booleans and $\iota$ for individuals. Internally, types are represented as a struct composed of a goal type and a list of argument types:

alias ShotDs.Data.Type

Type.new(:i) |> IO.inspect(label: "type i")
Type.new(:o, [:i, :o]) |> IO.inspect(label: "type i->o->o")
:ok

Terms are stored as Elixir structs acting as directed acyclic graphs (DAGs). They are assigned a (concurrency-safe) ID which is processed by the ShotDs.Stt.TermFactory module. These IDs are used for a caching mechanism using the Erlang term storage (ETS) under the hood. Notice that terms are represented in $\beta\eta$-normal form and use de Bruijn indices.

alias ShotDs.Stt.TermFactory, as: TF
import ShotDs.Util.Formatter # pretty-printing

x_id = TF.make_free_var_term("X", Type.new(:i, [:i, :o])) |> IO.inspect(label: "assigned ID")
TF.get_term!(x_id) |> IO.inspect(label: "generated term")
format!(x_id, _hide_types=false) |> IO.inspect(label: "pretty-printed")
:ok

Term Construction with the DSL

The module ShotDs.Hol.Dsl introduces a domain-specific language for shorthand term construction. It utilizes the unused Elixir operators &&&, |||, ~> and <~> as infix-constructors. Together with the module ShotDs.Hol.Definitions, we can build the XOR operator as follows:

import ShotDs.Hol.Definitions
import ShotDs.Hol.Dsl

exclusive_or = lambda([type_o(), type_o()], fn p, q ->
  (p ||| q) &&& neg(p &&& q)
end)

format!(exclusive_or) |> IO.puts()

Parsing TH0 Strings

The module ShotDs.Parser offers powerful parsing capabilities with full type inference for inputs in TPTP (TH0) format:

alias ShotDs.Parser

Parser.parse!("?[X : $o]: X => $true")
|> format!() |> IO.puts()

Note that the type inference engine assumes type $o$ for the outermost type unless inferable otherwise. Other unknown types are treated as type variables and are assigned a unique ID:

Parser.parse!("X @ a")
|> format!(_hide_types = false) |> IO.puts()

To clear up ambiguities, we can pass in a type environment:

alias ShotDs.Data.Context

ctx = Context.new() |> Context.put_const("a", type_i())

Parser.parse!("X @ a", ctx)
|> format!() |> IO.puts()

Parsing is also available via Sigils for TH0 formula strings (~f), TPTP problems (~p) (wiht thf(...) tags) and type environments (~e), including a wrapper for providing context:

import ShotDs.Hol.Sigils

~f(?[X : $o]: X => $true) |> format!() |> IO.puts()

with_context(~e[X : $o, p : $o>$i], fn ->
  ~f(p @ X) |> format!(false) |> IO.puts()
end)

Advanced Utilities

Error Handling: Functions that can fail return a tuple {:ok, result} or {:error, reason} per default. There are “bang” versions (suffixed by !) of all functions that either return the result directly or raise an error. with-clauses offer idiomatic error handling when processing user input and are generally preferred over exceptions:

with {:ok, term_id} <- Parser.parse("a & b"),
     {:ok, formatted} <- format(term_id) do
  IO.puts(formatted)
else
  {:error, msg} -> IO.puts("ERROR: #{msg}")
end

with {:ok, term_id} <- Parser.parse("a &"),
     {:ok, formatted} <- format(term_id) do
  IO.puts(formatted)
else
  {:error, msg} -> IO.puts("ERROR: #{msg}")
end

try do
  Parser.parse!("a &")
rescue
  e in Parser.ParseError ->
    IO.puts(~s'Rescued Parser.ParseError with message: "#{e.message}"')
end

File Parsing: ShotDs.Tptp includes parsing capabilities for TPTP files. The collected information is aggregated in a ShotDs.Data.Problem struct.

problem = ~p"""
thf(e_type,type,
    e: $tType).

thf(p_type,type,
    p: e>$o).

thf(lma,lemma,
    ![X : e]: p @ X).

thf(conj,conjecture,
    ?[Y : e]: p @ Y).
"""

IO.inspect(problem)

format!(problem) |> IO.puts()

Term Manipulation: Various functions regarding the semantics of STT, e.g. substitutions, are handled by the ShotDs.Stt.Semantics module.

alias ShotDs.Data.Substitution
alias ShotDs.Stt.Semantics

x = var("X", type_ii())
a = const("a", type_i())
b = const("b", type_ii())

x_a = app(x, a)
x_a |> format!(true) |> IO.puts()

s = %Substitution{fvar: TF.get_term!(x).head, term_id: b}

Semantics.subst!(s, x_a) |> format!(true) |> IO.puts()

Church Encoding: ShotDs.Stt.Numerals provides an implementation of Church’s encoding of natural numbers, adapted to simple types. This can for example be used for benchmarking. Additionally, Church’s encoding of Booleans is implemented in the module ShotDs.Stt.Booleans.

import ShotDs.Stt.Numerals

plus(num(5), num(2)) |> format!() |> IO.puts()

import ShotDs.Stt.Booleans

b_and(tt(), b_var("P")) |> format!() |> IO.puts()

Traversals and Transformation: Transformations of terms mostly follow the same scheme. An optimized adaption of the combinators fold (fold_term/2, fold_term!/2) and map (map_term/5, map_term!/5) to the DAG representation of terms is implemented in the module ShotDs.Util.TermTraversal. Examples for the usage of these higher-order functions can be found in the source code of the ShotDs.Stt.Semantics module or in ShotDs.Util.Formatter.format_term/2.

Pattern Matching: ShotDs.Hol.Patterns provides macro definitions for pattern matching on various HOL terms.

use ShotDs.Hol.Patterns

case TF.get_term!(true_term() ||| false_term()) do
  disjunction(p, q) -> IO.puts("Disjunction of #{format!(p)} and #{format!(q)}")
  _ -> IO.puts("No match")
end

Garbage Collection: Wrapping code with ShotDs.Stt.TermFactory.with_scratchpad/1 ensures temporary terms created by that code to be garbage collected afterwards. In this process, terms are written to a local ETS table and only the final result is (recursively) committed to the global table.