Regular Typed Unification

TL;DR

The paper introduces a new unification algorithm for terms in semantic domains using deterministic regular types, ensuring termination, soundness, and completeness, with applications to dynamically typed Prolog.

Contribution

It presents a novel unification algorithm based on constraint solving for deterministic regular types, with proven theoretical properties and practical application to Prolog.

Findings

Algorithm guarantees termination, soundness, and completeness.

Applicable to dynamically typed Prolog implementations.

Provides a formal foundation for type-aware unification in semantic domains.

Abstract

Here we define a new unification algorithm for terms interpreted in semantic domains denoted by a subclass of regular types here called deterministic regular types. This reflects our intention not to handle the semantic universe as a homogeneous collection of values, but instead, to partition it in a way that is similar to data types in programming languages. We first define the new unification algorithm which is based on constraint generation and constraint solving, and then prove its main properties: termination, soundness, and completeness with respect to the semantics. Finally, we discuss how to apply this algorithm to a dynamically typed version of Prolog.