Unification API

Unification is the process of matching two Terms by computing a substitution of their variables that makes them syntactically equal — the most general unifier (MGU). 2P-Kt exposes this as a standalone API in the :unify module, independent of the resolution engine.

Substitution

A Substitution (package it.unibo.tuprolog.core) represents a set of variable bindings. It is a Map<Var, Term> and comes in exactly two flavors, modeled as a sealed interface:

• Substitution.Unifier — a successful substitution, actually binding zero or more Vars to Terms;
• Substitution.Fail — the (singleton) representation of a failed unification attempt; it binds nothing.

sealed interface Substitution :
    Map<Var, Term>,
    Taggable<Substitution>,
    Castable<Substitution> {
    /** Whether this [Substitution] is a successful one (i.e., a [Unifier]) */
    @JsName("isSuccess")
    val isSuccess: Boolean

    /** Whether this [Substitution] is a failed one */
    @JsName("isFailed")
    val isFailed: Boolean

Key members:

• isSuccess / isFailed — discriminate between the two cases without casting;
• asUnifier() / castToUnifier() and asFail() / castToFail() — safe/unsafe downcasts;
• applyTo(term: Term): Term? — applies the bindings to a Term, returning null on Fail;
• plus(other: Substitution): Substitution — composes (unions) two substitutions; the result is Fail if either operand is Fail or if the union is contradictory (same Var bound to two different Terms);
• minus(...) / filter(...) — remove or select entries, preserving the concrete subtype (Unifier stays Unifier, Fail stays Fail);
• getOriginal(variable: Var): Var? — walks a chain of bindings backwards to find the original variable name.

Construction goes through Substitution's companion object: Substitution.empty(), Substitution.failed(), Substitution.of(variable, term), Substitution.of(vararg pairs), Substitution.unifier(...) (same as of but throws SubstitutionException instead of returning Fail on contradiction), and their Map/Iterable/Sequence overloads.

Unificator

The Unificator interface (it.unibo.tuprolog.unify.Unificator) is the entry point for performing unification. It carries a context: Substitution — pre-existing bindings assumed while unifying — and exposes three core operations, each with an occurCheckEnabled toggle (default true):

 *   that same variable (which would otherwise produce an infinite/cyclic term); disabling it trades soundness for
 *   speed, which is safe only when the caller already knows the operands cannot give rise to such a cycle.
 *
 * When the operands have distinct semantic roles, the subject term (such as a goal, query, actual value, or sought
 * item) should be passed first, and the reference term (such as a pattern, rule head, expected value, or stored
 * candidate) second. Calls whose operands have no such roles may retain their natural or mathematical order.
 *
 * Although unifiability is symmetric, the substitutions and unified terms returned by [mgu] and [unify] can retain
 * operand orientation. Reordering their arguments is therefore a behavioral change and requires appropriate tests.
 *
 * ```kotlin
 * val unificator = Unificator.default
 * val x = Var.of("X")
 * val substitution = unificator.mgu(x, Atom.of("a")) // {X -> a}
 * unificator.match(x, Atom.of("a")) // true
 * unificator.unify(x, Atom.of("a")) // a
 * ```
 *
 * To customize how terms are compared, or to observe/alter the equation-solving process, extend [AbstractUnificator]
 * instead of implementing this interface directly.
 */
interface Unificator {
    /**
     * The bindings assumed as already holding before unification starts; every [mgu]/[merge] call is implicitly
     * performed against this context, as if it were merged into the result. If [context] is [Substitution.failed],
     * every operation on this [Unificator] fails as well.
     */
    @JsName("context")
    val context: Substitution

    /**
     * Calculates the Most General Unifier of [term1] and [term2], optionally enabling occurs-check.
     *
     * @return a [Substitution.Unifier] (possibly [Substitution.empty]) binding the variables of [term1] and [term2]
     * so that applying it to both terms yields syntactically equal results, or [Substitution.failed] if no such
     * substitution exists (including when [occurCheckEnabled] is `true` and unification would otherwise produce a
     * cyclic term, or when [context] itself is failed).
     */
    @JsName("mguWithOccurCheck")
    fun mgu(
        term1: Term,
        term2: Term,
        occurCheckEnabled: Boolean = true,
    ): Substitution

    /** Calculates the Most General Unifier of [term1] and [term2], with occurs-check enabled. */
    @JsName("mgu")
    fun mgu(

• mgu(term1, term2) — computes the most general unifier, or Substitution.failed() if the terms don't unify;
• match(term1, term2) — true iff an MGU exists (shorthand for mgu(...) !== Substitution.failed());
• unify(term1, term2) — applies the MGU to term1 and returns the resulting Term, or null on failure.

A related operation, merge(sub1, sub2, occurCheckEnabled), combines two Substitutions the same way mgu combines two Terms (used internally when composing partial unifiers).

Operands are not interchangeable in general: when they have distinct semantic roles (a goal vs. a rule head, e.g.), the subject term should be passed first and the reference term second, since the returned substitution/unified term can retain that orientation even though unifiability itself is symmetric.

Creating unificators

The companion object provides three strategies, each obtainable with or without a starting context: Substitution:

• Unificator.default — strict() wrapped nowhere further; uses Term.equals for identity;
• Unificator.strict(context = Substitution.empty()) — compares terms via ==;
• Unificator.naive(context = Substitution.empty()) — like strict, but compares Integer/Numeric terms by value rather than by type-and-value.

val strict = Unificator.strict()
val strictWithContext = Unificator.strict(someSubstitution)

Caching

Unificator.cached(other: Unificator, capacity: Int = 32) decorates any Unificator with an LRU cache (via CachedUnificator) that memoizes recent mgu/match/unify calls. Unificator.default already uses an internal LRU cache of DEFAULT_CACHE_CAPACITY (32) entries.

Infix operators

For lighter-weight call sites, the companion object also defines infix extension functions on Term and Substitution, all backed by Unificator.default (hence always occur-check-enabled):

val substitution = term1 mguWith term2
val matches = term1 matches term2
val unified = term1 unifyWith term2
val merged = substitution1 mergeWith substitution2

Custom unification strategies

Implementing a custom Unificator amounts to subclassing AbstractUnificator and overriding checkTermsEquality(first: Term, second: Term): Boolean, the primitive used throughout the unification algorithm to decide whether two non-variable terms are equal:

val absoluteValueUnificator =
    object : AbstractUnificator() {
        override fun checkTermsEquality(first: Term, second: Term): Boolean = when {
            first is Integer && second is Integer ->
                first.value.absoluteValue.compareTo(second.value.absoluteValue) == 0
            else -> first == second
        }
    }