Regular Typed Unification

TL;DR

This work tackles unification of terms interpreted over semantic domains defined by deterministic regular types, enabling runtime type-error detection in logic programming. It introduces a constraint-based unification algorithm built on semantic typing, where terms and equations are analyzed with respect to domain-specific typings, and proves termination, soundness, and completeness with respect to the semantic model. The approach combines constraint generation and solving, yielding either a most general unifier with a principal type or outcomes indicating type-domain incompatibility or unsatisfiable constraints, and discusses its applicability to dynamically typed Prolog variants. By partitioning the universe into domains and enforcing type-aware unification, the method provides a principled framework for catching domain-crossing errors during unification and offers a path toward safer, more robust logic programming systems.

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.

Figures (2)

• Figure 1: Type System
• Figure 2: Constraint Typing Judgment