ShotUnify

ShotUnify adapts the 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 formulae:

• rigid-rigid: The head symbols of both formulae are constant.
• flex-rigid: One head symbol is variable, the other constant.
• flex-flex: The head symbols of both formulae 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 formulae 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.

Installation

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

def deps do
  [
    {:shot_unify, "~> 0.1.0"}
  ]
end