ShotUn

ShotUn adapts the higher-order unification algorithm developed in the library HOL to the data structures and semantics of ShotDs.

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

Higher-order Unification

Higher-order unification is the task of determining the common instances of two given higher-order terms, i.e., a complete set of unifiers (substitutions) that represent solutions to the given unification problem. However, Goldfarb (1981) has shown that unification is already undecidable for second-order logic.

Unification Problems

Generally, there are three configurations of unification problems for two given higher-order terms:

• rigid-rigid: The head symbols of both terms are constant.
• flex-rigid: One head symbol is variable, the other constant.
• flex-flex: The head symbols of both terms are variable.

Pre-unification

Higher-order pre-unification (Huet, 1975) describes a semi-decision procedure for this problem by not unifying flex-flex pairs and instead returning them as constraints (there are infinitely many common instances). The semi-decidability stems from flex-rigid pairs. Certain terms might require a very complex composition of imitation and projection bindings, while for others we might only be certain no solution exists after exhausting this infinite search space. Without a depth bound, there is hence no termination guarantee.

Imitation and Projection Bindings

When the algorithm encounters a flex-rigid equation, it takes the form:

$$F(s_1, \dots, s_n) \overset{?}{=} h(t_1, \dots, t_m)$$

where $F$ is a free variable with arity $n$ (the flexible head) and $h$ is a constant or bound variable of arity $m$ (the rigid head).

To solve this, the algorithm must generate a partial substitution for $F$ of the form $\lambda X_1 \dots X_n. e / F$, where $e$ is an expression that constructs the required output. We branch the search space into two specific strategies:

In imitation, we guess that the flexible variable $F$ directly produces the rigid head $h$. We substitute $F$ with a $\lambda$-abstraction that explicitly calls $h$, passing fesh variables $H_1 \dots H_m$ to represent the unknown arguments that $h$ will need. Note that imitation is only valid if $h$ is a constant, not a bound variable. Otherwise, we could have a variable capture error.

In projection, we guess that the flexible variable $F$ doesn't construct $h$ itself, but rather relies on one of its own arguments $s_i$ to eventually produce the required structure. We substitute $F$ with a $\lambda$-abstraction that returns its $i$-th argument. If $s_i$ is itself a function taking $k$ arguments, we must supply it with fresh variables. The algorithm will branch and attempt projection for every argument $s_i$ whose return type matches the goal type.

Decidable Fragments

Two well-known fragments of higher-order unification are decidable and are implemented as separate entry points:

• Miller pattern unification(Miller, 1991): the subclass in which every free variable appears only in applications to pairwise distinct bound variables. Unification is unitary — every solvable problem has a most-general unifier (MGU). Exposed via ShotUn.pattern_unify/1, which returns {:ok, %UnifSolution{}} (with no remaining flex-flex pairs) or :error. The implementation follows the four standard rules (decomposition, flex-rigid inversion with pruning of nested flex applications, flex-flex with shared head, flex-flex with distinct heads).
• Second-order matching(Huet & Lang, 1978): the special case where the right-hand side is ground and every type in the problem has order at most 2. The complete set of matchers is enumerated lazily without a depth bound; termination follows from a strict structural recursion on the right-hand sides. Exposed via ShotUn.match/1.

ShotUn.unify/3 accepts a :strategy option to dispatch among the three algorithms. The default is :pre_unification; :auto inspects the problem and routes it to the most specific fragment it falls into:

ShotUn.unify(pairs)                                  # depth-bounded pre-unification
ShotUn.unify(pairs, 10, strategy: :auto)             # auto-dispatch
ShotUn.unify(pairs, 10, strategy: :pattern)          # force Miller patterns
ShotUn.unify(pairs, 10, strategy: :matching)         # force second-order matching

ShotUn.pattern_unify(pairs)                          # direct pattern API
ShotUn.match({pattern, target})                      # direct matching API (one pair or a list)

Installation

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

def deps do
  [
    {:shot_un, "~> 0.1"}
  ]
end