Demo of the BeHOLd package

Mix.install([
  {:kino, "~> 0.17.0"},
  {:behold, "~> 1.1.2"},
  {:hol, "~> 1.0.2"}
])

Setup

Definitions and patterns of e.g., HOL connectives, are defined in the modules BeHOLd.ClassicalHOL.Definitions and BeHOLd.ClassicalHOL.Patterns as macros. To use them in Livebook, we hence need the use keyword which handles the imports and ensures the macros are usable. Aliasing can be handled when passing the as option.

# Definitions and patterns are defined as macros.
# For usage in a livebook, we hence need the use keyword.
use BeHOLd.ClassicalHOL.Definitions, as: Definitions
use BeHOLd.ClassicalHOL.Patterns, as: Patterns
alias BeHOLd.ClassicalHOL.Equality
alias BeHOLd.Data.Context
alias BeHOLd.{Parser, TPTP}

As BeHOLd is an extention of the library HOL, some functionality, e.g., the definition of additional types, require some of its modules. To use macros for pattern matching in Livebook, we need to require the desired module. The records for types and terms are internally defined as macros for tuples.

require HOL.Data
alias HOL.Data
alias PrettyPrint

Per default, HOL prints debug logs to the console when calling functions from its API, mainly on levels :info and :notice. This behavior can be disabled by setting the level to :error or disable logging entirely.

Logger.put_application_level(:hol, :error)

form =
  Kino.Control.form(
    [
      name: Kino.Input.checkbox("Print debug logs")
    ],
    report_changes: true
  )

Kino.listen(form, fn event ->
  if event.data.name == true do
    Logger.put_application_level(:hol, :info)
  else
    Logger.put_application_level(:hol, :error)
  end
end)

form

Types

Types are instances of the data structure HOL.Data.type() and represents types as records which in turn internally use tuples. The type $\iota$ is hence representable (and can be pattern matched) as:

Definitions.type_i()

match?(HOL.Data.type(goal: :i, args: []), Definitions.type_i())

More complex types are stored in their curried, flattened representation, where the field :args contains the list of argument types. E.g., the type $(\iota\to o)\to(\iota\to o)\to(\iota\to o)$ can be curried as $(\iota\to o)\to(\iota\to o)\to\iota\to o$, where $o$ is the goal type and $(\iota\to o)$, $(\iota\to o)$ and $\iota$ are the argument types.

Definitions.type_io_io_io()

match?(
  HOL.Data.type(goal: :o, args: [
    Definitions.type_io(),
    Definitions.type_io(),
    Definitions.type_i()
  ]),
  Definitions.type_io_io_io()
)

Definitions and Patterns for HOL Symbols

The module BeHOLd.ClassicalHOL.Definitions also contains the usual connectives of classical HOL as signature symbols and defines other common connectives like XOR in terms of these symbols. The signature spans the following connectives:

$$ \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} \quad \Pi_{(\alpha\to o)\to o} \quad \Sigma_{(\alpha\to o)\to o} \quad =_{\alpha\to\alpha\to o} $$

Definitions.signature_symbols()

In combination with the functions from HOL.Data and HOL.Terms, these can be used to construct logical terms. The HOL library also includes a PrettyPrint module which can convert various data structures to a readable string representation, with or without type annotation.

x = HOL.Terms.mk_free_var_term("X", Definitions.type_o())
c = HOL.Terms.mk_const_term("c", Definitions.type_o())

x_and_c = Definitions.and_term()
  |> HOL.Terms.mk_appl_term(x)
  |> HOL.Terms.mk_appl_term(c)

PrettyPrint.pp_term x_and_c

PrettyPrint.pp_term x_and_c, false

Note that the connectives are implemented both as HOL.Data.declaration() and HOL.Data.hol_term() for different use cases, e.g., term construction or pattern matching.

match?(Definitions.and_const(), HOL.Data.get_head(x_and_c))

$\lambda$-abstractions are also supported by specifying the variable (as HOL.Data.declaration()) to capture.

x_var = HOL.Data.mk_free_var("X", Definitions.type_o())

HOL.Terms.mk_abstr_term(x_and_c, x_var)
  |> PrettyPrint.pp_term(false)

The module BeHOLd.ClassicalHOL.Patterns provides various convenient macros to pattern-match on HOL terms.

match?(Patterns.conjunction(_, _), x_and_c)

For other common connectives, shorthand constructors are also available which define them in terms of the symbols from the signature.

Definitions.xor_term()
  |> PrettyPrint.pp_term

Quantors and equality symbols require types for term construction, not necessarily for pattern matching. Note that for quantors, a set type (i.e., a type with goal $o$) must be specified.

a = HOL.Terms.mk_const_term("a", Definitions.type_i())
b = HOL.Terms.mk_const_term("b", Definitions.type_i())

a_eq_b =
  Definitions.equals_term(Definitions.type_i())
  |> HOL.Terms.mk_appl_term(a)
  |> HOL.Terms.mk_appl_term(b)

match?(Patterns.equality(^a, ^b), a_eq_b)

TPTP Output

Terms and types can also be represented as TPTP strings via the BeHOLd.TPTP module. The BeHOLd.TPTP.term_to_tptp/1 function fully $\eta$-reduces terms and tries to reconstruct the syntactic sugar of TPTP, e.g., the XOR operator.

p = HOL.Terms.mk_free_var_term("P", Definitions.type_o())
q = HOL.Terms.mk_const_term("q", Definitions.type_o())

Definitions.xor_term()
  |> HOL.Terms.mk_appl_term(p)
  |> HOL.Terms.mk_appl_term(q)
  |> TPTP.term_to_tptp

Parser

The module BeHOLd.Parser contains parsing utility for types and terms in TPTP's TH0 syntax. The parser implements full type inference, where terms of unknown will be mapped to type $o$. Optionally, a context can be specified for types which can't be inferred by the term structure. The parser implements the standard TH0 precedence rules.

Parser.parse "~A & B"

The usage of quantors requires extra caution as their scope is influenced by parentheses.

"![X : $o]: $false => (X => $true)"
  |> Parser.parse
  |> HOL.Data.get_head

"![X : $o]: (f @ X) | (g @ X)"
  |> Parser.parse
  |> HOL.Data.get_head

A type environment (context) can be specified to clear up non-inferrable types. The type inference engine handles the rest.

"X = a" |> Parser.parse() |> PrettyPrint.pp_term(false)

ctx = Context.new()
  |> Context.put_var("X", Definitions.type_i())

"X = a" |> Parser.parse(ctx) |> PrettyPrint.pp_term(false)

Equality

From version 1.1.2, BeHOLd supports constructors for different notions of equality. These include Leibniz equality $\mathcal{L}^\tau$, Andrews equality $\mathcal{A}^\tau$ and extensional equality $\mathcal{E}^{\alpha\to\beta}$.

$\mathcal{L}^\tau$ states that two terms of type $\tau$ are equal because they share the same properties. It can be formulated using different connectives such as implication, equivalence or the converse of the implication. Default is equivalence.

$\mathcal{A}^\tau$ formulates equality stating that all reflexive binary relations on type $\tau$ hold for the two terms.

$\mathcal{E}^{\alpha\to\beta}$ is only defined on function types and states that two terms are equal because they share the same extensions.

a = HOL.Terms.mk_const_term("a", Definitions.type_ii())
b = HOL.Terms.mk_const_term("b", Definitions.type_ii())

ctx = Context.new()
  |> Context.put_const("a", Definitions.type_ii())
  |> Context.put_const("b", Definitions.type_ii())

(
  Equality.leibniz_equality(Definitions.type_ii())
  |> HOL.Terms.mk_appl_term(a)
  |> HOL.Terms.mk_appl_term(b)
) == Parser.parse("![P:($i>$i)>$o]: P @ a <=> P @ b")

(
  Equality.leibniz_equality(Definitions.type_ii(), Definitions.implies_term())
  |> HOL.Terms.mk_appl_term(a)
  |> HOL.Terms.mk_appl_term(b)
) == Parser.parse("![P:($i>$i)>$o]: P @ a => P @ b")

(
  Equality.leibniz_equality(Definitions.type_ii(), Definitions.implied_by_term())
  |> HOL.Terms.mk_appl_term(a)
  |> HOL.Terms.mk_appl_term(b)
) == Parser.parse("![P:($i>$i)>$o]: P @ a <= P @ b")

(
  Equality.andrews_equality(Definitions.type_ii())
  |> HOL.Terms.mk_appl_term(a)
  |> HOL.Terms.mk_appl_term(b)
) == Parser.parse("![Q:($i>$i)>($i>$i)>$o]: ((![X:$i>$i]: Q @ X @ X) => Q @ a @ b)")

(
  Equality.extensional_equality(Definitions.type_ii())
  |> HOL.Terms.mk_appl_term(a)
  |> HOL.Terms.mk_appl_term(b)
) == Parser.parse("![X:$i]: a @ X = b @ X", ctx)