Unification

Unification is the fundamental operation that drives inference, querying, and pattern matching in the Reasoning Layer. Understanding unification is essential to understanding how queries find results and how rules derive conclusions.

What is unification?

Unification answers the question: “Can these two things be made identical, and if so, how?”

Given two terms, unification tries to find a substitution — a mapping from variables to values — that makes the two terms structurally equal. If such a substitution exists, the terms unify; if not, they fail to unify.

A simple analogy

Think of unification like solving a jigsaw puzzle between two shapes. Each shape might have “holes” (variables) that can be filled. If the shapes can be made to match by filling in the holes, they unify.

Term A:  person(name: "Alice",  age: ?)
Term B:  person(name: ?,        age: 30)
                          ↓
Result:  person(name: "Alice",  age: 30)
         with ?₁ = "Alice" and ?₂ = 30

Both terms are “person” structures. Term A has a name but no age; Term B has an age but no name. Unification fills in the blanks from both sides.

How it works

Unification compares two terms feature by feature:

1. Sort check: The sorts must be compatible (one must be a subtype of the other, or they must share a GLB in the lattice)
2. Feature matching: For each shared feature name:
   • If both have concrete values, the values must be equal
   • If one has a variable, the variable is bound to the other’s value
   • If both have variables, the variables are linked (they must take the same value)
3. Constraint propagation: If a variable has constraints (guards), the bound value must satisfy them

Examples

Successful unification:

employee(name: "Alice", salary: ?S)
employee(name: ?N,      salary: 120000)
→ unifies with {?N = "Alice", ?S = 120000}

Failed unification — value conflict:

person(name: "Alice", age: 30)
person(name: "Bob",   age: 30)
→ fails: "Alice" ≠ "Bob"

Failed unification — sort incompatibility:

person(name: "Alice")
vehicle(make: "Toyota")
→ fails: person and vehicle have no common subtype

Unification with sort hierarchy:

person(name: "Alice")        ← sort: person
employee(name: "Alice", salary: 90000)  ← sort: employee (subtype of person)
→ unifies: employee is a person, so the structures are compatible
→ result has sort: employee (the more specific type)

Unification in the Reasoning Layer

In backward chaining (inference)

When you run a backward chaining query, the engine tries to unify your goal with rules and facts:

// Goal: find all high earners
const goal = TermInput.byName('high_earner', {
  name: FeatureInput.variable('?Name'),
});

// Rule head: high_earner(name: ?Name) :- employee(name: ?Name, salary > 100000)
// Fact: employee(name: "Alice", salary: 120000)

// Step 1: Goal unifies with rule head → {?Name linked}
// Step 2: Rule body unifies with fact → {?Name = "Alice"}
// Result: ?Name = "Alice"

The engine chains unifications through rules until it reaches facts (ground terms). Each successful chain is a solution.

In queries

The findUnifiable query method uses unification to find matching terms in the knowledge base:

// Find all persons named "Alice"
const matches = await client.query.findUnifiable({
  query: TermInput.byName('person', {
    name: FeatureInput.string('Alice'),
  }),
});
// Returns all terms that unify with this pattern

In fuzzy unification

Fuzzy unification extends standard unification with a similarity degree (0.0 to 1.0). Instead of a strict pass/fail, fuzzy unification asks “how well do these two terms match?” This is used for approximate matching and similarity search.

const result = await client.fuzzy.fuzzyUnify({
  term1_id: termA,
  term2_id: termB,
  threshold: 0.5,
});
// result.degree: 0.0 to 1.0

Unification vs. equality

Unification is not the same as equality:

Operation	Question	Variables?	Direction
Equality	”Are these two things identical right now?”	No	—
Unification	”Can these two things be made identical by filling in variables?”	Yes	Bidirectional

Unification is bidirectional — variables on either side can be filled in. This is different from “matching” in most programming languages, which is one-directional (the pattern has variables, the data doesn’t).

Unification and the sort lattice

When two terms have different sorts, unification computes the GLB (Greatest Lower Bound) of their sorts. If a GLB exists, the unified term has that sort. If no GLB exists (the sorts are completely unrelated), unification fails.

       entity
      /      \
  person    organization
      \      /
     employee    ← GLB of person and organization

If you unify a person term with an organization term, the result (if it succeeds) has sort employee — the most specific type that is both a person and an organization.

Key takeaways

1. Unification is pattern matching with variables on both sides — it finds the most specific common structure
2. It drives all reasoning — backward chaining, forward chaining, queries, and fuzzy comparison all use unification
3. It respects the sort lattice — sort compatibility is checked, and the result has the GLB sort
4. Variables are placeholders — they get bound to concrete values during unification
5. Constraints are checked — guard constraints on variables are validated against bound values