Chapter 2: Preliminaries

Mix.install([
  {:shot_ds, "1.3.1"},
  {:kino, "~> 0.19.0"}
])

Notation

We abbreviate a sequence $a_1, \dots, a_n$ by $\bar{a}_n$ where $n \geq 0$, write $()$ for the empty sequence, and write $\bar{a}, \bar{b}$ for concatenation. We drop the length subscript and write $\bar{a}$ when it is irrelevant or clear from context, and write $|\bar{a}|$ for the length of $\bar{a}$. $\bar{n}$ is the sequence $1,\dots,n$ and ${\bar{a}}$ is the set ${a_1, \dots, a_n}$. The reverse of a sequence $\bar{a}_n$ is denoted $\overleftarrow{a}n$. We denote the sequence $a_i,\dots,a_j$ by $\bar{a}{i..j}$ which we identify with $()$ when $i \ge j$.

_Under $\lambda \bar{\tau}n$, index $n + 1 - i$ denotes $\tau_i$, so a head applied to its own binders takes $\overleftarrow{n}$.

Relations and functions on sequences are interpreted pointwise, so $\bar{a}_n \mathrel{R} \bar{b}_n$ stands for $a_1 \mathrel{R} b_1, \dots, a_n \mathrel{R} b_n$ and $f(\bar{a}_n)$ for $f(a_1),\dots,f(a_n)$.

Note that parsing uses TPTP syntax [Sut17], in the typed higher-order dialects TH0 [SB10] and TH1 [KSR16], which differs from the notation established in this chapter. The higher-order TPTP dialects use currying and an explicit application symbol @ where we will use conventional application notation ($f(x, y)$ instead of $f \mathop{@} x \mathop{@} y$). Everything developed here is a more direct representation of the prover's internal data structures. The same goes for the formatting API of the prover, which uses more conventional type annotation (you may see $f_{\iota{\to}\iota{\to}\iota}$ instead of $f : (\iota,\iota){\to}\iota$ in the interactive outputs). This is a deliberate choice as this thesis is a system description more than it is developing a logic or calculus. The prover's output has a different aim, which is for teaching or visualisation of classical higher-order logic.

Three registers run through every chapter and are kept typographically distinct. Definition and Proposition blocks are the mathematics: implementation-independent, and the only material a soundness or completeness argument may appeal to. Ordinary prose motivates and explains, and carries no logical weight. Blockquoted paragraphs are implementation notes, recording what the Shot packages do, which module does it and which parameter governs it; a note may narrow a definition without the definition changing. Executable cells and quoted code belong to the third register as well: where the code is the precise statement, it is run rather than paraphrased.

Sigils (~f, ~g, ~t, ~e) enable quick parsing of TPTP notation into our internal data structures.

import ShotDs.Hol.Sigils
Kino.nothing

Types

Simple Type Theory (STT), in the formulation of Church [Chu40], is a language of terms and defines the semantics of the transformation of higher-order terms. It defines computation on a single reduction principle, $\beta$-reduction. An efficient implementation of STT is hence most relevant for the performance of a prover for higher-order logic. Its type layer is fixed in this section and its term layer in the sections that follow.

Definition (Base Type, Type). Let $\mathcal{S} = {\iota, o}$ be the set of sorts and let $\mathcal{A}$ be a countably infinite set of type variables ($\alpha$). The set of base types ($\varsigma$) is $\mathcal{B} = \mathcal{S} \uplus \mathcal{A}$. The set of types $\mathcal{T}$ ($\tau, \upsilon, \rho$), is defined inductively: if $\bar{\tau}_n \in \mathcal{T}$ with $n \geq 0$ and $\varsigma \in \mathcal{B}$, then $\bar{\tau}_n {\to} \varsigma \in \mathcal{T}$. We identify $() {\to} \varsigma$ with $\varsigma$.

Proposition (Canonical Decomposition). Every $\tau \in \mathcal{T}$ is of the form $\bar{\tau}_n {\to} \varsigma$ for a unique $n \geq 0$, a unique sequence $\bar{\tau}_n$ and a unique $\varsigma \in \mathcal{B}$.

Proof. The type grammar has a single production, whose goal component is required to lie in $\mathcal{B}$, so a type is an argument sequence paired with a base type and $n$ is the length of that sequence. Distinct pairs are distinct types, and the identification of $() {\to} \varsigma$ with $\varsigma$ places each base type at $n = 0$ rather than giving it a second decomposition. $\square$

Definition (Arity, Goal). For $\tau = \bar{\upsilon}_n {\to} \varsigma$ we call $n$ the arity $\operatorname{ar}(\tau)$ of $\tau$ and $\varsigma$ its goal $\operatorname{gl}(\tau)$.

Definition ($o$-Type, Pure $o$-Type). A type $\tau$ is an $o$-type if $\operatorname{gl}(\tau) = o$, so that a term of type $\tau$ is a formula once it is fully applied. The set $\mathcal{O} \subseteq \mathcal{T}$ of pure $o$-types is the least set with $o \in \mathcal{O}$ and $\bar{\tau}_n {\to} o \in \mathcal{O}$ whenever every $\tau_i \in \mathcal{O}$.

Proposition ($o$-Types and Pure $o$-Types). Every pure $o$-type is an $o$-type, and the inclusion is strict: $\iota {\to} o$ is an $o$-type and is not pure.

Proof. Induction on membership in $\mathcal{O}$: both clauses produce a type whose goal is $o$. For strictness, $\operatorname{gl}(\iota {\to} o) = o$, so $\iota {\to} o$ is an $o$-type, and it lies in $\mathcal{O}$ only if $\iota$ does, whereas every element of $\mathcal{O}$ has goal $o$ and $\operatorname{gl}(\iota) = \iota$. $\square$

The two notions do different work later and are not interchangeable. The weaker one selects the quantifiers a primitive substitution may be scheduled for (§ Primitive Substitution), where all that is required is that instantiating the variable eventually yields something of type $o$; the argument types are unconstrained. The pure one selects the types whose domain is finite and enumerable (§ Quantifier Rules), which is what allows quantification over them to expand linearly and what bounds the case analysis of the Boolean extensionality rules.

Definition (Type Substitution). A type substitution $\vartheta$ is a map from a finite subset of $\mathcal{A}$ to $\mathcal{T}$. Its application $\tau[\vartheta]$ is defined by recursion on $\tau$:

$$ \varsigma[\vartheta] = \begin{cases} \theta(\varsigma) & \varsigma \in \operatorname{dom}(\vartheta) \ \varsigma & \text{otherwise} \end{cases} \qquad\qquad (\bar{\tau}_n !\to! \varsigma)[\vartheta] = \bar{\tau}_n[\vartheta], \bar{\upsilon} {\to} \varsigma' \quad \text{where } \varsigma[\vartheta] = \bar{\upsilon} {\to} \varsigma' \text{ and } n \geq 1 $$

We write $[\bar{\alpha}_n \mapsto \bar{\rho}_n]$ for the substitution mapping $\alpha_i$ to $\rho_i$.

Proposition (Instantiation and Arity). $\operatorname{ar}(\tau[\vartheta]) \geq \operatorname{ar}(\tau)$, with equality if and only if $\operatorname{gl}(\tau)[\vartheta] \in \mathcal{B}$.

Proof. Write $\tau = \bar{\tau}_n {\to} \varsigma$ by Canonical Decomposition, so that $\operatorname{ar}(\tau) = n$ and $\operatorname{gl}(\tau) = \varsigma$. The substitution clause appends the argument sequence of $\varsigma[\vartheta]$ to $\bar{\tau}_n[\vartheta]$, giving $\operatorname{ar}(\tau[\vartheta]) = n + \operatorname{ar}(\varsigma[\vartheta])$, and the same identity holds at $n = 0$, where $\tau[\vartheta] = \varsigma[\vartheta]$. Arities are non-negative, which gives the inequality, and equality holds exactly when $\operatorname{ar}(\varsigma[\vartheta]) = 0$, by Canonical Decomposition exactly when $\varsigma[\vartheta] \in \mathcal{B}$. $\square$

Our implementation defines the following recursive data structure for a Type. We use a unique Erlang reference as identifier for variables:

defmodule Ch2.Type do
  @enforce_keys [:goal]
  defstruct [:goal, args: []]
  @type type_id() :: concrete_id() | variable_id()

  @type concrete_id() :: atom()
  @type variable_id() :: reference()

  @type t :: %__MODULE__{goal: type_id(), args: [t()]}
end

Kino.nothing

Definition (Type Scheme). A type scheme $\sigma \in \mathfrak{T}$ has the form $[\bar{\alpha}]., \tau$ with $n \geq 0$, where $\bar{\alpha}$ are pairwise distinct and every type variable occurring in $\tau$ is among $\bar{\alpha}$. Quantification occurs only at the outermost position. A type $\rho$ is an instance of $\sigma$ if $\rho = \tau[\bar{\alpha}_n \mapsto \bar{\rho}_n]$ for some $\bar{\rho}_n \in \mathcal{T}$.

A TypeScheme is implemented as a wrapper around a Type, explicitly pinning down quantified type variables:

defmodule Ch2.TypeScheme do
  @enforce_keys [:body]
  defstruct [:body, vars: []]

  @type t :: %__MODULE__{vars: [Ch2.Type.variable_id()], body: Ch2.Type.t()}
end

Kino.nothing

For example, the type $(\iota, (\iota {\to} o)) {\to} o$ is represented as follows:

# The sigils ~f (formulae with goal type o unless specified otherwise),
# ~g (terms which may have a type variable as goal type), ~t (types) and ~e (type contexts)
# internally invoke parsing of TPTP syntax, which uses curried representation.
~t| $i > ($i > $o) > $o | |> Kino.Tree.new

Terms

Definition (Signature). A signature $\Sigma$ is a finite set of declarations $c : \sigma$ with $\sigma \in \mathfrak{T}$, in which every constant symbol $c$ is declared at most once.

Definition (Free Variable, Parameter). Let $\mathcal{V} = \biguplus_{\tau \in \mathcal{T}} \mathcal{V}\tau$ and $\mathcal{P} = \biguplus{\tau \in \mathcal{T}} \mathcal{P}_\tau$ be families of countably infinite, pairwise disjoint sets with $\mathcal{V} \cap \mathcal{P} = \emptyset$. Elements of $\mathcal{V}$ are free variables ($X, Y$); elements of $\mathcal{P}$ are parameters ($p, q$).

Definition (Term). Given a signature $\Sigma$, the set of terms $\Lambda(\Sigma)$ ($s$, $t$, $u$, $v$) is defined by

$$ \Lambda(\Sigma) \ni s, t \coloneqq c\langle \bar{\rho} \rangle \mid X \mid p \mid i \mid \lambda \bar{\tau}., t \mid s(\bar{t}) $$

where $c \in \Sigma$ is a constant symbol, $\bar{\rho}, \bar{\tau} \in \mathcal{T}$ with $n \geq 0$, $X \in \mathcal{V}$, $p \in \mathcal{P}$, and $i \in \mathbb{N}_{>0}$ is a de Bruijn index [dB72]. We identify $\lambda ()., t$ with $t$ and $s()$ with $s$, and further identify $\lambda \bar{\tau}., \lambda \bar{\upsilon}., t$ with $\lambda \bar{\tau}, \bar{\upsilon}., t$.

Constants, variables and parameters are all implemented as Declaration. Note that we merge the definitions of constants and parameters and give parameters a unique reference as name. We also make the name of bound variables explicit and refer to them by their local index.

defmodule Ch2.Declaration do
  @enforce_keys [:kind, :name, :type]
  defstruct [:kind, :name, :type]

  @type t :: free_var_t() | bound_var_t() | const_t()

  @type free_var_t :: %__MODULE__{
          kind: :fv,
          name: var_name_t(),
          type: Ch2.Type.t()
        }
  @type bound_var_t :: %__MODULE__{
          kind: :bv,
          name: pos_integer(),
          type: Ch2.Type.t()
        }
  @type const_t :: %__MODULE__{
          kind: :co,
          name: const_name_t(),
          type: Ch2.Type.t()
        }

  @type var_name_t :: String.t() | reference() | pos_integer()
  @type const_name_t :: String.t() | reference()
end

Kino.nothing

Terms as the main data structure require more thought in their representation to optimise both space and time efficiency. We opt for hash-consed directed acyclic graphs (DAGs) [FC06] and rely on the Erlang term storage (ETS), a heavily optimised global hash table, for efficient and concurrency-safe lookup. Our term representation features 5 data fields and 4 metadata fields, optimised for caching and minimising recursive checks:

defmodule Ch2.Term do
  @enforce_keys [:id, :head, :type]
  defstruct [
    # Data fields
    :id,
    :head,
    :type,
    bvars: [],
    args: [],
    # Metadata fields
    fvars: MapSet.new(),
    consts: MapSet.new(),
    tvars: MapSet.new(),
    max_num: 0
  ]

  @type global_term_id :: pos_integer()
  @type local_term_id :: neg_integer()
  @type dummy_term_id :: 0

  @type term_id :: global_term_id() | local_term_id() | dummy_term_id()

  @type t :: %__MODULE__{
          # Data fields
          id: term_id(),
          bvars: [Ch2.Declaration.t()],
          head: Ch2.Declaration.t(),
          args: [term_id()],
          # Metadata fields
          type: Ch2.Type.t(),
          fvars: MapSet.t(Ch2.Declaration.t()),
          consts: MapSet.t(Ch2.Declaration.const_t()),
          tvars: MapSet.t(Ch2.Type.variable_id()),
          max_num: non_neg_integer()
        }
end

Kino.nothing

A constructed term shows the representation directly. Note that :args holds term IDs rather than nested terms, so the DAG is flat in the struct and unfolds only through the factory:

import ShotDs.Hol.Sigils
alias ShotDs.Stt.TermFactory, as: TF

t = with_context ~e[p: $i>$o, q: $i>$o, f: $i>$i, a: $i], fn ->
  ~f[(p @ (f @ a)) & (q @ (f @ a))]
end

TF.get_term!(t) |> Kino.Tree.new

alias ShotDs.Stt.TermFactory, as: TF

[left, right] = TF.get_term!(t).args

TF.get_term!(left) |> Kino.Tree.new()

Both conjuncts reference the same node for $f(a)$, which is memoised once:

alias ShotDs.Stt.TermFactory, as: TF

TF.get_term!(left).args == TF.get_term!(right).args

true

Terms are constructed globally, via the ShotDs.Stt.TermFactory module in a single ETS table (:term_pool). Term IDs may be global or local. Global term IDs are stored in the :term_pool while local IDs only persist in a process-local ETS table, the scratchpad. Garbage collection is implemented so that result terms (and transitively, their argument terms) are committed to the :term_pool while the scratchpad with all its entries is deleted. Garbage collection can be enabled by wrapping the code block in with_scratchpad(fn -> ... end). Using Kino lets us inspect the content of the :term_pool interactively. Note that the :term_pool records signature -> term_id and term_id -> term.

Kino.ETS.new :term_pool

Treating terms as global DAGs lets us write efficient canonical higher-order functions such as map_term or fold_term using term IDs as keys for caching:

defmodule Ch2.TermTraversal do
  @spec map_term!(
    term_id :: Ch2.Term.term_id(),
    env :: a,
    update_env :: (Ch2.Term.t(), a -> a),
    transform :: (Ch2.Term.t(), [Ch2.Term.term_id()], a, map() -> {Ch2.Term.term_id(), map()}),
    short_circuit :: (Ch2.Term.t(), a -> boolean()),
    cache :: map()
  ) :: {Ch2.Term.term_id(), map()}
    when a: var
  def map_term!(
      term_id,
      env,
      update_env,
      transform,
      short_circuit \\ fn _, _ -> false end,
      cache \\ %{}
    ) do
    case Map.fetch(cache, {term_id, env}) do
      {:ok, cached_id} -> {cached_id, cache}
      :error ->
        term = StubTF.get_term!(term_id)
        if short_circuit.(term, env) do
          {term_id, Map.put(cache, {term_id, env}, term_id)}
        else
          new_env = update_env.(term, env)
          arg_map_fn = &map_term!(&1, new_env, update_env, transform, short_circuit, &2)
          {new_args, cache} = Enum.map_reduce(term.args, cache, arg_map_fn)
          {new_id, cache} = transform.(term, new_args, new_env, cache)
          {new_id, Map.put(cache, {term_id, env}, new_id)}
        end
    end
  end
end

defmodule StubTF do
  @type_o %Ch2.Type{goal: :o}
  @dummy_head %Ch2.Declaration{kind: :co, name: "h", type: @type_o}
  def get_term!(term_id), do: %Ch2.Term{id: term_id, head: @dummy_head, type: @type_o}
end

Kino.nothing

Typing

Definition (Context). A context $\Gamma$ is a finite sequence of types $\bar{\tau}$, listed from outermost to innermost binding. Lookup $\Gamma(i)$ is defined by

$$ (\Gamma, \tau)(1) = \tau \qquad\qquad (\Gamma, \tau)(i+1) = \Gamma(i) $$

Definition (Typing). The typing judgement $\Gamma \vdash_\Sigma t : \tau$ is defined by the following rules; we drop the subscript $\Sigma$ when it is fixed.

$$ \frac{c : [\bar{\alpha}_n]., \tau \in \Sigma \qquad \bar{\rho}_n \in \mathcal{T}}{\Gamma \vdash c\langle \bar{\rho}_n \rangle : \tau[\bar{\alpha}n \mapsto \bar{\rho}n]} \qquad \frac{X \in \mathcal{V}\tau}{\Gamma \vdash X : \tau} \qquad \frac{p \in \mathcal{P}\tau}{\Gamma \vdash p : \tau} \qquad \frac{\Gamma(i) = \tau}{\Gamma \vdash i : \tau} $$

$$ \frac{\Gamma, \bar{\tau} \vdash t : \bar{\upsilon} {\to} \varsigma}{\Gamma \vdash \lambda \bar{\tau}., t : (\bar{\tau}, \bar{\upsilon}) {\to} \varsigma} \qquad\qquad \frac{\Gamma \vdash s : \bar{\tau}_n {\to} \varsigma \qquad \Gamma \vdash \bar{t}_n : \bar{\tau}_n}{\Gamma \vdash s(\bar{t}_n) : \varsigma} $$

A term $t$ is well-typed in $\Gamma$ if $\Gamma \vdash t : \tau$ holds for some $\tau$. From here on, we only consider well-typed terms. We write $t : \tau$ for the term $t$ for which $\Gamma \vdash t : \tau$ for some global context $\Gamma$.

Proposition (Unique Typing). If $\Gamma \vdash t : \tau$ and $\Gamma \vdash t : \tau'$, then $\tau = \tau'$.

Proof. Induction on $t$. Each typing rule is determined by the shape of $t$, so at most one applies to a given term. For a head the conclusion is read off data fixed independently of the derivation: the signature entry together with the type arguments for $c\langle \bar{\rho}_n \rangle$, the type index of $\mathcal{V}$ or $\mathcal{P}$ for $X$ and $p$, and the context lookup for $i$. For $\lambda \bar{\tau}., t$ and $s(\bar{t}_n)$ the conclusion is a function of the premise types, unique by the induction hypothesis, and of the split of the premise type into arguments and goal, unique by Canonical Decomposition. $\square$

Shifting and Substitution

Definition (Shifting). For $d \geq 0$ and cutoff $k \geq 0$, the shift $t \uparrow^{d}_{k}$ is defined by

$$ i !\uparrow^{d}{k}; = \begin{cases} i + d & i > k \ i & i \leq k \end{cases} \qquad (\lambda \bar{\tau}., t) !\uparrow^{d}{k}; = \lambda \bar{\tau}., t !\uparrow^{d}{k+n}; \qquad (s(\bar{t})) !\uparrow^{d}{k}; = (s !\uparrow^{d}{k})(\bar{t} !\uparrow^{d}{k}) $$

together with $c\langle \bar{\rho} \rangle !\uparrow^{d}{k}; = c\langle \bar{\rho} \rangle$, $X !\uparrow^{d}{k}; = X$ and $p !\uparrow^{d}{k}; = p$. We write $t !\uparrow^{d}$ for $t !\uparrow^{d}{0}$.

Definition (Substitution). The simultaneous substitution of a block $\bar{u}_n$ for the innermost $n$ indices, $t[\bar{u}_n]$, is $t[\bar{u}_n]_0$ where

$$ i[\bar{u}_n]k = \begin{cases} u{n+1-(i-k)} !\uparrow^{k} & k < i \leq k+n \ i - n & i > k+n \ i & i \leq k \end{cases} \qquad\qquad (\lambda \bar{\tau}_m., t)[\bar{u}_n]_k = \lambda \bar{\tau}_m., t[\bar{u}n]{k+m} $$

together with $(s(\bar{t}_m))[\bar{u}_n]_k = (s[\bar{u}_n]_k)(\bar{t}_m[\bar{u}_n]_k)$, and with constants, free variables and parameters left unchanged.

Definition (Free-Variable Substitution). A free-variable substitution $\theta$ is a map from a finite subset of $\mathcal{V}$ to $\Lambda(\Sigma)$ such that $\theta(X)$ has type $\tau$ for every $X \in \mathcal{V}_\tau \cap \operatorname{dom}(\theta)$. Its application $t\theta$ is $t\theta_0$ where

$$ X\theta_k = \begin{cases} \theta(X) \uparrow^{k} & X \in \operatorname{dom}(\theta) \ X & \text{otherwise} \end{cases} \qquad\qquad (\lambda \bar{\tau}_n., t)\theta_k = \lambda \bar{\tau}n., t\theta{k+n} $$

together with $(s(\bar{t}))\theta_k = (s\theta_k)(\bar{t}\theta_k)$, and with constants, parameters and indices left unchanged.

Shifting and substitution are efficiently implemented on top of the map_term combinator. Both make use of the env field to store the current index depth and use a term's max_num and fvars fields to skip unnecessary recursive calls (as short_circuit).

Reduction and Normal Forms

Definition ($\beta$-Reduction). $(\lambda \bar{\tau}_n., t)(\bar{u}_n, \bar{v}m) ;\longrightarrow\beta; t\bar{u}_n$

Definition (Head). A head ($h$) is a term of the form $c\langle \bar{\rho}_n \rangle$, $X$, $p$ or $i$.

Definition (Long Normal Form). A well-typed term $t$ with $\Gamma \vdash t : \tau$ is in $\eta$-long $\beta$-normal form if $t = \lambda \bar{\upsilon}_n., h(\bar{u}_m)$ where $n = \operatorname{ar}(\tau)$ and each $u_j$ is in $\eta$-long $\beta$-normal form. In the following, we only consider terms that are in $\eta$-long $\beta$-normal form and assume that they are always $\beta$-reduced and $\eta$-expanded after each transformation.

The internals of the TermFactory and Semantics API ensure terms to always be well-typed and in $\eta$-long $\beta$-normal form.

Parameter Terms

Definition (Parameter Term). Let $\bar{X} \in \mathcal{V}$ be pairwise distinct with $\bar{X} \in \mathcal{V}{\bar{\tau}}$, and let $p \in \mathcal{P}{(\bar{\tau}, \bar{\upsilon}_n) \to \varsigma}$. The parameter term of $p$ over $\bar{X}$ is

$$ p{\bar{X}} = \lambda \bar{\upsilon}_n., p(\bar{X}, \overleftarrow{n}) $$

We call $\bar{X}$ the dependencies of $p{\bar{X}}$, and $p$ fresh for a set of terms $T$ if $p \notin \operatorname{par}(T)$.

Proposition (Parameter Term). $\Gamma \vdash p{\bar{X}} : \bar{\upsilon} {\to} \varsigma$, and $p{\bar{X}}$ is in $\eta$-long $\beta$-normal form.

Proof. Under the context $\Gamma, \bar{\upsilon}_n$ the parameter rule gives $p : (\bar{\tau}, \bar{\upsilon}_n) {\to} \varsigma$, the variable rule gives $X_i : \tau_i$, and lookup gives the reversed indices $\overleftarrow{n}$ the types $\bar{\upsilon}_n$, the context being listed outermost to innermost. The application rule yields $\Gamma, \bar{\upsilon}_n \vdash p(\bar{X}, \overleftarrow{n}) : \varsigma$ and the abstraction rule $\Gamma \vdash \lambda \bar{\upsilon}_n., p(\bar{X}, \overleftarrow{n}) : \bar{\upsilon}_n {\to} \varsigma$. The term is in $\eta$-long $\beta$-normal form because its head is the parameter $p$, its arguments are in that form by the standing convention on terms, and the number of binders is $n = \operatorname{ar}(\bar{\upsilon}_n {\to} \varsigma)$. $\square$

A parameter is created by make_fresh_const_term/1, which builds a Declaration carrying a unique reference as its name at type $(\bar{\tau}_n, \bar{\upsilon}_m){\to}\varsigma$. Since make_term/1 $\eta$-expands any declaration of arrow type on construction, the abstraction $\lambda\bar{\upsilon}_m$ is produced by the term factory rather than written by the caller; applying the result to the dependencies $\bar{X}_n$ then $\beta$-reduces the outer $n$ binders away. No shift on $\bar{X}_n$ is needed, as shifting acts as the identity on free variables. For $m = 0$ the parameter term collapses to $p(\bar{X}_n)$, and for $n = 0$ to the $\eta$-long form of $p$ itself.

Syntactic Equality and Unification

Definition (Syntactic Equality). Two terms $s$ and $t$ are syntactically equal if they are the same element of $\Lambda(\Sigma)$.

Because terms are hash-consed into a single global pool, syntactic equality is decided by comparing term IDs. Together with de Bruijn indices and the $\eta$-long $\beta$-normal invariant, this makes $\alpha$-, $\beta$- and $\eta$-equivalence all coincide with identity of IDs.

Definition (Flex, Rigid). A term is flex if its head is a free variable and rigid otherwise. A unification problem is a finite set of equations ${\bar{s}_n \overset{?}{=} \bar{t}_n}$; an equation is flex-flex if both of its sides are flex. A unifier of a unification problem is a free-variable substitution $\theta$ such that $s_i\theta$ and $t_i\theta$ are syntactically equal for every $i$.

Definition (Pre-Unification Problem). A pre-unifier [Hue75] of a unification problem $E$ is a pair $\Theta = (\theta, C)$, where $\theta$ is a free-variable substitution and $C$ is a finite set of flex-flex equations, such that $\theta\theta'$ is a unifier of $E$ for every unifier $\theta'$ of $C$. The pre-unification problem for $E$ is the task of enumerating pre-unifiers of $E$.

A pre-unifier is represented as %ShotUn.UnifSolution{substitutions: theta, flex_pairs: C} and pre-unifiers are enumerated lazily as a stream. Flex-flex equations are always solvable, so a pre-unifier witnesses solvability of $E$ without committing to a solution for $C$.

Connectives, Quantifiers and Equality

Classical higher-order logic (HOL) is defined as an extension of STT and is the language we will be working with. Textbook treatments are given by Andrews [And02], and the model classes lying between Henkin and standard semantics are laid out by Benzmüller, Brown and Kohlhase [BBK04]. The signature, the semantics and the notion of entailment the prover decides are fixed in this section and the four that follow it.

Definition (Signature of HOL). $\Sigma^{\textrm{HOL}}$ contains the following symbols:

$$ \top, \bot : o \qquad\qquad \neg : o !\to! o \qquad\qquad \lor, \land, \supset, \equiv ;: (o, o) {\to} o $$ $$ \forall,\exists : [\alpha]., (\alpha {\to} o) {\to} o \qquad\qquad =; : [\alpha]., (\alpha, \alpha) {\to} o $$

We write $\varphi * \psi$ instead of $(\varphi, \psi)$ for $ \in {\land, \lor, \supset, \equiv, =}$ and $\mathrm{Q}\bar{\tau}_n., \varphi$ instead of $\mathrm{Q}(\lambda \tau_1., \dots \mathrm{Q}(\lambda \tau_n.,\varphi))$ for $\mathrm{Q} \in {\forall, \exists}$. We call terms from $\Lambda(\Sigma^{\mathrm{HOL}})$ HOL terms, those of type $o$ formulae ($\varphi, \psi, \chi$), and those of type $\tau {\to} o$ for $\tau \in \mathcal{T}$ properties ($\Phi, \Psi$).

ShotDs.Hol.Definitions.signature

["⊤", "⊥", "¬", "∨", "∧", "⊃", "≡", "=", "∀", "∃"]

Definition (Complement). The complement ${\sim}\varphi$ of a formula $\varphi$ is $\chi$ if $\varphi = \neg\chi$, and $\neg\varphi$ otherwise.

Frames and Interpretations

Classical HOL is typically discussed for curried terms, i.e. $f(x, y)$ represented as $fxy$. To discuss the semantics of HOL in the notation introduced in this chapter, we borrow the notion of sections from set theory. This allows us to describe partial application.

Definition (Frame). A frame $\mathcal{D} = (\mathcal{D}\tau){\tau \in \mathcal{T}}$ is a collection of nonempty sets $\mathcal{D}\tau$ such that $\mathcal{D}o = {\mathrm{T}, \mathrm{F}}$, each $\mathcal{D}{\bar{\tau}n {\to} \varsigma}$ is a set of functions mapping $\overline{\mathcal{D{\tau_i}}}n$ to $\mathcal{D}\varsigma$, and the collection is closed under sections: for $f \in \mathcal{D}{(\bar{\tau}_n, \bar{\upsilon}) {\to} \varsigma}$ and $\bar{a}n \in \overline{\mathcal{D{\tau_i}}}n$, the section $f{\bar{a}n}$ given by $f{\bar{a}n}(\bar{b}) = f(\bar{a}n, \bar{b})$ lies in $\mathcal{D}{\bar{\upsilon} {\to} \varsigma}$. The frame is standard if every $\mathcal{D}{\bar{\tau}_n {\to} \varsigma}$ is the full space of such functions.

Sections are what make partial application meaningful here. Types are uncurried with a base goal, so an element of $\mathcal{D}_{(\tau, \bar{\upsilon}) {\to} \varsigma}$ is a function of $1 + |\bar{\upsilon}|$ arguments and supplying one of them yields nothing in the frame unless the frame is asked to contain the result. Where no confusion arises we allow $s(a)$ as a synonym for $s_a$, and correspondingly read a term $s(t)$ whose head is under-applied as the $\eta$-long form $\lambda\bar{\upsilon}., s(t, \bar{\upsilon})$.

Definition (Interpretation). An interpretation $\mathcal{I}$ over a frame $\mathcal{D}$ and a signature $\Sigma \supseteq \Sigma^{\mathrm{HOL}}$ maps every type instance $c\langle\bar{\rho}\rangle : \upsilon$ of a constant $c \in \Sigma$, and every parameter $p \in \mathcal{P}\upsilon$, to an element of $\mathcal{D}\upsilon$, subject to the conditions below on the logical constants. Each condition constrains $\mathcal{I}$ and at the same time demands of $\mathcal{D}$ that the required element be present in it.

• $\mathcal{I}(\top) = \mathrm{T}$ and $\mathcal{I}(\bot) = \mathrm{F}$; $\mathcal{I}(\neg)$ maps $\mathrm{T}$ to $\mathrm{F}$ and $\mathrm{F}$ to $\mathrm{T}$; and $\mathcal{I}(\land)$, $\mathcal{I}(\lor)$, $\mathcal{I}(\supset)$, $\mathcal{I}(\equiv)$ are the corresponding Boolean functions on ${\mathrm{T}, \mathrm{F}}$.
• Equality. For every $\tau \in \mathcal{T}$ and $a, b \in \mathcal{D}\tau$, $\mathcal{I}(=!\langle\tau\rangle)(a, b) = \mathrm{T}$ if and only if $a$ and $b$ are the same element of $\mathcal{D}\tau$.
• Quantifiers. For every $\tau \in \mathcal{T}$ and every $f \in \mathcal{D}{\tau {\to} o}$, $\mathcal{I}(\forall\langle\tau\rangle)(f) = \mathrm{T}$ if and only if $f(a) = \mathrm{T}$ for every $a \in \mathcal{D}\tau$, and $\mathcal{I}(\exists\langle\tau\rangle)(f) = \mathrm{T}$ if and only if $f(a) = \mathrm{T}$ for some $a \in \mathcal{D}_\tau$.

Equality is fixed to identity at every type, which is the property that makes an interpretation logical in the sense of Benzmüller, Brown and Kohlhase [BBK04]. The two extensionality principles a higher-order calculus needs are then consequences rather than stipulations, and are stated as such below; the one principle that is not a consequence, Leibniz equality, is separated out with the condition it actually requires.

Denotation and Models

Definition (Variable Assignment). A variable assignment $g$ maps every free variable $X \in \mathcal{V}\tau$ to an element $g(X) \in \mathcal{D}\tau$.

Definition (Denotation). Let $\mathcal{D}$ be a frame, $\mathcal{I}$ an interpretation over it, $\mathcal{M}$ the pair $(\mathcal{D}, \mathcal{I})$, $g$ a variable assignment and $\bar{\xi}_k$ a sequence of elements of $\mathcal{D}$ valuing the outermost $k$ de Bruijn indices. The denotation of a term $t : \tau$, written $[![t]!](\mathcal{M}, g, \bar{\xi}k)$, is the partially defined element of $\mathcal{D}\tau$ given by

• $[![c\langle\bar{\rho}\rangle]!](\mathcal{M}, g, \bar{\xi}_k) = \mathcal{I}(c\langle\bar{\rho}\rangle)$ for constant symbols $c \in \Sigma$
• $[![p]!](\mathcal{M}, g, \bar{\xi}_k) = \mathcal{I}(p)$ for parameters $p \in \mathcal{P}$
• $[![X]!](\mathcal{M}, g, \bar{\xi}_k) = g(X)$ for free variables $X \in \mathcal{V}$
• $[![i]!](\mathcal{M}, g, \bar{\xi}_k) = \xi_i$ for de Bruijn indices $1 \leq i \leq k$
• $[![s(\bar{t}_n)]!](\mathcal{M}, g, \bar{\xi}_k) = \left([![s]!](\mathcal{M}, g, \bar{\xi}_k)\right) \left(\overline{[![t_i]!](\mathcal{M}, g, \bar{\xi}_k)}_n \right)$
• $[![\lambda\bar{\tau}_n., t]!](\mathcal{M}, g, \bar{\xi}k)$, for $t : \bar{\upsilon} {\to} \varsigma$, is the unique $f \in \mathcal{D}{(\bar{\tau}n, \bar{\upsilon}) {\to} \varsigma}$ whose sections satisfy $f{\bar{d}_n} = [![t]!](\mathcal{M}, g, (\overleftarrow{d}_n, \bar{\xi}_k))$ for all $\bar{d}n \in \overline{\mathcal{D{\tau_i}}}_n$, and is undefined when $\mathcal{D}$ contains no such $f$

Definition (Henkin Model, Standard Model). A Henkin model [Hen50, And02] is a pair $\mathcal{M} = (\mathcal{D}, \mathcal{I})$ of a frame and an interpretation over it whose denotation is total, meaning that $[![t]!](\mathcal{M}, g, \bar{\xi}_k)$ is defined for every well-typed term $t$, every variable assignment $g$ and every $\bar{\xi}_k$ valuing $t$'s context. $\mathcal{M}$ is a standard model if $\mathcal{D}$ is standard.

Totality is the substantive condition in this definition. A frame may omit functions, so the demand is that it omit none whose absence would leave a term without a value; every standard model is a Henkin model, and the converse fails.

Extensionality and Leibniz Equality

Proposition (Boolean Extensionality). $\mathcal{I}(=!\langle o \rangle) = \mathcal{I}(\equiv)$.

Proof. $\mathcal{D}_o = {\mathrm{T}, \mathrm{F}}$, so two elements are the same element exactly when both are $\mathrm{T}$ or both are $\mathrm{F}$, which is the graph of $\mathcal{I}(\equiv)$. $\square$

Proposition (Functional Extensionality). Let $s, t \in \mathcal{D}{(\tau, \bar{\upsilon}) {\to} \varsigma}$. Then $\mathcal{I}(=!\langle(\tau, \bar{\upsilon}) {\to} \varsigma\rangle)(s, t) = \mathrm{T}$ if and only if $\mathcal{I}(=!\langle\bar{\upsilon} {\to} \varsigma\rangle)(s_a, t_a) = \mathrm{T}$ for every $a \in \mathcal{D}\tau$.

Proof. Elements of a frame at arrow type are functions, and two functions are the same function exactly when all their sections agree. Both sides therefore say that $s$ and $t$ are the same element. $\square$

Definition (Separation). A frame separates at $\tau$ if for all distinct $a, b \in \mathcal{D}\tau$ there is a $P \in \mathcal{D}{\tau {\to} o}$ with $P(a) \neq P(b)$. It separates if it separates at every type.

Proposition (Leibniz Equality). Let $a, b \in \mathcal{D}\tau$. If $\mathcal{I}(=!\langle\tau\rangle)(a, b) = \mathrm{T}$ then $P(a) = P(b)$ for every $P \in \mathcal{D}{\tau {\to} o}$. The converse holds for all $a, b \in \mathcal{D}_\tau$ if and only if $\mathcal{D}$ separates at $\tau$. Every standard frame separates.

Proof. The first claim is substitution of identicals. The second is the definition of separation, contraposed. For the third, the characteristic function of ${a}$ is a member of a standard $\mathcal{D}_{\tau {\to} o}$ and separates $a$ from every other element. $\square$

The three propositions are what Chapter 3's three equality-expansion rules appeal to, one each, and they do not all cost the same. Expansion at $o$ and expansion at an arrow type are sound in every Henkin model, because they restate identity in a frame whose arrow components are functions. Leibniz expansion at a base type is sound in the direction that reads an equation as agreement of all properties, and its converse direction, the one a refutation needs when it expands $\neg(s =!\langle\varsigma\rangle; t)$, holds only where the frame separates at $\varsigma$. Separation is therefore a condition on the model class rather than a consequence of the semantics, and the negative rule of that section is what makes it operational: it Skolemises the separating property into a fresh parameter rather than requiring the frame to supply it.

Satisfiability and Entailment

Definition (Satisfiability). A formula $\varphi$ is satisfiable iff there exists a Henkin model $\mathcal{M}$ and a variable assignment $g$, such that $[![\varphi]!](\mathcal{M}, g, ()) = \mathrm{T}$. A set of formulae is satisfiable if all its elements are jointly satisfiable under the same Henkin model and variable assignment. Conversely, a formula (or a set of formulae) is unsatisfiable if no such model and variable assignment exists.

Definition (Entailment and Validity). A formula $\psi$ is entailed by a set of formulae $\Phi$, written $\Phi \models \psi$, if $[![\psi]!](\mathcal{M}, g, ()) = \mathrm{T}$ for every Henkin model $\mathcal{M}$ and variable assignment $g$ under which every element of $\Phi$ denotes $\mathrm{T}$. A formula $\varphi$ is valid, written $\models \varphi$, iff $\varnothing \models \varphi$.

Proposition (Refutational Reformulation). $\Phi \models \psi$ if and only if $\Phi \cup {\neg\psi}$ is unsatisfiable.

Proof. $\mathcal{I}(\neg)$ is Boolean complement and $\mathcal{D}_o$ has two elements, so under a fixed $\mathcal{M}$ and $g$ exactly one of $\psi$ and $\neg\psi$ denotes $\mathrm{T}$. $\square$

The reformulation is the form the prover decides. A conjecture is refuted rather than proved: the negated conclusion joins the assumptions and the tableau of Chapter 3 attempts to show the resulting set unsatisfiable. The turnstile $\vdash$ is reserved for the typing judgement of this chapter and is not used for entailment.

Chapter References

• [And02] Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, second edition. Applied Logic Series 27. Kluwer Academic Publishers, 2002.
• [BBK04] Christoph Benzmüller, Chad E. Brown, and Michael Kohlhase. Higher-order semantics and extensionality. The Journal of Symbolic Logic, 69(4):1027–1088, 2004.
• [Chu40] Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56–68, 1940.
• [dB72] Nicolaas G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 75(5):381–392, 1972.
• [FC06] Jean-Christophe Filliâtre and Sylvain Conchon. Type-safe modular hash-consing. In Proceedings of the 2006 Workshop on ML, pages 12–19. ACM, 2006.
• [Hen50] Leon Henkin. Completeness in the theory of types. The Journal of Symbolic Logic, 15(2):81–91, 1950.
• [Hue75] Gérard P. Huet. A unification algorithm for typed $\lambda$-calculus. Theoretical Computer Science, 1(1):27–57, 1975.
• [KSR16] Cezary Kaliszyk, Geoff Sutcliffe, and Florian Rabe. TH1: The TPTP typed higher-order form with rank-1 polymorphism. In Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), CEUR Workshop Proceedings 1635, pages 41–55, 2016.
• [SB10] Geoff Sutcliffe and Christoph Benzmüller. Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning, 3(1):1–27, 2010.
• [Sut17] Geoff Sutcliffe. The TPTP problem library and associated infrastructure: From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017.

---

Previous: Chapter 1: Introduction  $\cdot$  Contents  $\cdot$  Next: Chapter 3: Higher-Order Tableaux