International Workshop on Unification

One context unification extends first-order unification by introducing a single context variable, possibly with multiple occurrences. One context unification is known to be in NP, but it is not known to be solvable in polynomial time. In this talk, we motivate the context unification problem through its application in inter-procedural program analysis. We then present an NP procedure for the problem, followed by a polynomial time algorithm for certain interesting classes of the one context unification problem. The fascinating thing about one context unification is that it is very close to first-order unification and our algorithm itself is presented as an inference system that extends the usual inference rules for first-order unification. The algorithm is of independent value as it can be used, with slight modifications, to solve other problems, such as the first-order unification problem that tolerates one clash.

Matching is the special case of unification where one of the sides to be unified has no variables and thus remains unchanged under substitutions. In Description Logics (DLs), matching concepts against patterns (concepts with variables) was introduced to help filter out unimportant aspects of complicated concepts appearing in large industrial knowledge bases. Unification of patterns was suggested as a means to detect redundancies in ontologies, by finding different concepts that may potentially stand for the same intuitive notion. Recently, approximate unification was introduced in order to increase the recall of classical unification, i.e., find substitutions that are “almost” unifiers rather than exact unifiers. In the DL FL0, the problem can be reduced to approximately solving formal language equations. Adapting a similar technique, we investigate the language equations obtained from approximate matching in FL0 and provide algorithms to approximately solve said equations.

We consider a syntax for nominal terms extended with non-capturing atom substitution and show that unification over such terms is undecidable. The proof of undecidability is obtained by reducing Hilbert's tenth problem to unification of extended nominal terms, adapting Goldfarb's proof of undecidability of second-order unification.

We consider the generalisation of nominal unification where besides expression variables, also atom variables are considered. It is known that in both cases most general unifiers exist for a solvable input constraint. A most general unifier consists of a substitution and a set of freshness constraints, where the latter is an implicit restriction on the instances of the substitution. In the general case with atom variables, we focus in this paper on an improved computation of the most general unifier, and show that a general unifier can be computed in quadratic time. Applications of this algorithm are in reasoning about program transformations in higher order functional languages.

We describe a matching algorithm to solve the so-called letrec matching problem. The meta-expressions occurring in the matching equations stem from a meta-language that uses higher-order abstract syntax augmented by meta-notation for recursive let, contexts, sets of bindings, and chain variables. Additionally, three kinds of constraints can be added to meta-expressions to express usual constraints on evaluation rules and program transformations. We provide a sound and complete matching algorithm ithat it runs in non-deterministic polynomial time. We show that the letrec matching problem is NP-complete.

Typecheckers for dependently typed languages such as Agda, Idris, or Coq use unification to check definitions by dependent pattern matching. Though dependent type theory is a rich theory with higher-order terms, the unification algorithm used is typically a simple first-order one. There are however some considerations unique to the setting of dependent types:
- To see whether a unification rule can be applied, it is essential to know the type of an equation as well as its left- and right-hand sides.
- The left- and right-hand side of an equation can have different types, that only become equal after the preceding equations have been solved.
- Dependently typed languages have their own internal notion of equality (in the form of the identity type), which has to be respected by the unification algorithm. This is especially important for new type theories such as homotopy type theory (HoTT) that add certain extra structure to the identity type.
In this talk, I will present our framework for unification in a dependently typed setting. This framework treats unification problems and unification rules as internal to the type theory, rather than belonging to some external tool. Firstly, we represent a unification problem as a telescopic equation: a list of (typed) equations where the type of each equation can depend on the solution to previous equations. This allows us to keep track of dependencies between the equations precisely, and introduce new unification rules that exploit the dependencies between the equations. Secondly, a unification algorithm in our framework produces not just a substitution but also evidence that the given equations are satisfied under this substitution. This evidence guarantees that all unification rules respect the type theory's notion of equality. Finally, we give a novel characterization of a most general unifier as a (type theoretic) equivalence between the original telescope of equations and the trivial one. This gives us not only a very elegant way to define most general unifiers, but it also turns out to be useful for the compilation of functions defined by dependent pattern matching.

It is widely known that Miller's higher-order patterns provide a decidable class of higher-order unification. These have been used as the basic term structure for pattern matching in various computational systems, such as higher-order logic programming and higher-order rule based computation. However, the class of higher-order patterns is a bit restrictive in practice. Recently, Libal and Miller present a new decidable class of higher-order unification problems called Functions-as-Constructors unification (FCU). It extends the class of higher-order patterns and retains good properties of pattern unification, namely, it ensures the existence of the most general unifier. In this abstract, we report that FCU unification can be implemented functionally as an extension of Nipkow's functional pattern unification. We have implemented the FCU unification in Haskell, which has been a part of our SOL system for critical pair checking of higher-order rules.

Unification theory has found significant applications in cryptographic protocol analysis, but that is not the only security area in which it can be applied. Here we discuss recent research in the automatic generation and verification of cryptographic algorithms, and show how it can be used to find attacks on modes of encryption. We describe an algorithm we have recently developed based on the Baader-Schulz combination procedure, and we discuss some open research problems.

We compare two kinds of unification problems: Asymmetric Unification and Disunification, which are variants of Equational Unification. Asymmetric Unification is a type of Equational Unification where the right‑hand sides of the equations are in normal form with respect to the given term rewriting system. In Disunification we solve equations and disequations with respect to an equational theory. We contrast the time complexities of both and show that the two problems are incomparable: there are theories where one can be solved in polynomial time while the other is NPhard. This goes both ways. The time complexity also varies based on the termination ordering used in the term rewriting system.

TBD

We investigate the unification problem in equational theories involving convergent forward-closed term rewrite systems. In the class of forward-closed theories, unification is decidable and finitary. Furthermore, forward-closed theories are syntactic theories admitting\ a terminating mutation-based unification procedure. We first demonstrate this result by showing that a mutation-based unification algorithm, originally developed for equational theories saturated by paramodulation, remains sound and complete for forward-closed theories. Building on this result we use the new mutation-based algorithm to develop an algorithm that solves the unification problem in unions of forward-closed theories with non-disjoint theories. The resulting algorithm can be viewed as a terminating instance of a procedure initiated for hierarchical combination.

TBD

In this paper, we investigate a problem dual to the unification problem, namely the Common Term (CT) problem for string rewriting systems. Our main motivation was in computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point problem is reducible to the common term problem. We also prove that the common term problem is undecidable for dwindling string rewriting systems.