Introduction
Unification and pattern matching are the fundamental mechanisms that make logic programming work. They enable the system to:
- Match queries against facts and rule heads
- Bind variables to values
- Determine if two terms can be made identical
- Explore alternative solutions through backtracking
Understanding unification and pattern matching is essential for writing correct and efficient logic programs.
What is Unification?
Unification is the process of making two terms identical by finding appropriate variable bindings. It’s the core mechanism that enables pattern matching in logic programming.
Definition
Two terms unify if there exists a substitution (binding of variables to values) that makes them identical.
Example:
% parent(tom, bob) unifies with parent(X, Y)
% Substitution: X = tom, Y = bob
% parent(tom, bob) unifies with parent(tom, Z)
% Substitution: Z = bob
% parent(tom, bob) does NOT unify with parent(X, X)
% No substitution can make tom = bob
Unification Algorithm
The unification algorithm works as follows:
-
If both terms are identical atoms or numbers: They unify with no substitution needed.
tom unifies with tom → Success 5 unifies with 5 → Success tom unifies with bob → Failure -
If one term is a variable: The variable unifies with the other term (if occurs check passes).
X unifies with tom → X = tom X unifies with f(a, b) → X = f(a, b) -
If both terms are compound terms: They unify if:
- They have the same functor and arity
- Their corresponding arguments unify
parent(tom, bob) unifies with parent(X, Y) → tom unifies with X (X = tom) → bob unifies with Y (Y = bob) → Success -
Otherwise: They don’t unify.
parent(tom, bob) does NOT unify with grandparent(tom, bob) → Different functors (parent vs grandparent)
Occurs Check
The occurs check prevents infinite structures by checking if a variable appears in the term it’s being unified with.
% Without occurs check (standard Prolog)
X = f(X). % Succeeds, creates infinite structure
% With occurs check (safer)
X = f(X). % Fails, X cannot contain itself
Most Prolog systems don’t perform occurs check by default for performance reasons, but it’s important to be aware of this issue.
Pattern Matching
Pattern matching is the process of comparing a query or goal against facts and rule heads to find matches. Unification is the mechanism that enables pattern matching.
Basic Pattern Matching
Matching against facts:
% Facts
parent(tom, bob).
parent(bob, ann).
parent(bob, pat).
% Query: ?- parent(tom, bob).
% Matching process:
% 1. Try to unify parent(tom, bob) with parent(tom, bob) → Success!
% Answer: yes
% Query: ?- parent(tom, X).
% Matching process:
% 1. Try to unify parent(tom, X) with parent(tom, bob)
% → tom unifies with tom (success)
% → X unifies with bob (X = bob)
% Answer: X = bob
Matching against rule heads:
% Rule
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
% Query: ?- grandparent(tom, ann).
% Matching process:
% 1. Try to unify grandparent(tom, ann) with grandparent(X, Z)
% → tom unifies with X (X = tom)
% → ann unifies with Z (Z = ann)
% 2. Now try to prove the body with these bindings:
% parent(tom, Y), parent(Y, ann)
Complex Pattern Matching
Matching compound terms:
% Facts
person(john, age(25), city(new_york)).
person(mary, age(30), city(london)).
% Query: ?- person(john, age(A), city(C)).
% Matching:
% 1. john unifies with john → Success
% 2. age(A) unifies with age(25) → A = 25
% 3. city(C) unifies with city(new_york) → C = new_york
% Answer: A = 25, C = new_york
Matching lists:
% Facts
list_member([1, 2, 3]).
list_member([a, b, c]).
% Query: ?- list_member([H|T]).
% Matching:
% 1. [H|T] unifies with [1, 2, 3]
% → H = 1 (head)
% → T = [2, 3] (tail)
% Answer: H = 1, T = [2, 3]
Unification Examples
Example 1: Simple Unification
% Query: ?- parent(tom, bob) = parent(X, Y).
% Unification:
% 1. parent unifies with parent (same functor)
% 2. tom unifies with X → X = tom
% 3. bob unifies with Y → Y = bob
% Answer: X = tom, Y = bob
Example 2: Recursive Unification
% Query: ?- f(a, g(b, c)) = f(X, g(Y, Z)).
% Unification:
% 1. f unifies with f (same functor)
% 2. a unifies with X → X = a
% 3. g(b, c) unifies with g(Y, Z)
% → g unifies with g (same functor)
% → b unifies with Y → Y = b
% → c unifies with Z → Z = c
% Answer: X = a, Y = b, Z = c
Example 3: Failed Unification
% Query: ?- parent(tom, bob) = parent(tom, tom).
% Unification:
% 1. parent unifies with parent (same functor)
% 2. tom unifies with tom → Success
% 3. bob unifies with tom → FAILURE (bob ≠ tom)
% Answer: no
Example 4: Variable Unification
% Query: ?- X = Y, Y = tom.
% Unification:
% 1. X = Y → X and Y are the same variable
% 2. Y = tom → Y = tom, so X = tom
% Answer: X = tom, Y = tom
Example 5: List Unification
% Query: ?- [H|T] = [1, 2, 3].
% Unification:
% 1. [H|T] unifies with [1, 2, 3]
% → H = 1 (head)
% → T = [2, 3] (tail)
% Answer: H = 1, T = [2, 3]
% Query: ?- [A, B|Rest] = [1, 2, 3, 4].
% Unification:
% 1. A = 1 (first element)
% 2. B = 2 (second element)
% 3. Rest = [3, 4] (remaining elements)
% Answer: A = 1, B = 2, Rest = [3, 4]
Pattern Matching in Action
Example 1: Finding Family Relationships
% Facts
parent(tom, bob).
parent(bob, ann).
parent(bob, pat).
% Query: ?- parent(X, bob).
% Pattern matching:
% 1. Try to match parent(X, bob) with parent(tom, bob)
% → tom unifies with X (X = tom)
% → bob unifies with bob (success)
% Answer: X = tom
% Query: ?- parent(bob, X).
% Pattern matching:
% 1. Try to match parent(bob, X) with parent(tom, bob) → Fails
% 2. Try to match parent(bob, X) with parent(bob, ann)
% → bob unifies with bob (success)
% → X unifies with ann (X = ann)
% Answer: X = ann (first solution)
% 3. Backtrack and try next fact: parent(bob, pat)
% → X = pat (second solution)
Example 2: Matching Structured Data
% Facts
employee(john, department(engineering), salary(80000)).
employee(mary, department(sales), salary(60000)).
employee(bob, department(engineering), salary(75000)).
% Query: ?- employee(john, department(D), salary(S)).
% Pattern matching:
% 1. john unifies with john → Success
% 2. department(D) unifies with department(engineering)
% → D = engineering
% 3. salary(S) unifies with salary(80000)
% → S = 80000
% Answer: D = engineering, S = 80000
% Query: ?- employee(X, department(engineering), salary(S)).
% Pattern matching:
% 1. Try first fact: employee(john, department(engineering), salary(80000))
% → X = john, S = 80000
% Answer: X = john, S = 80000 (first solution)
% 2. Backtrack and try next fact: employee(mary, ...) → Fails
% 3. Try next fact: employee(bob, department(engineering), salary(75000))
% → X = bob, S = 75000
% Answer: X = bob, S = 75000 (second solution)
Example 3: Matching with Rules
% Facts
parent(tom, bob).
parent(bob, ann).
% Rule
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
% Query: ?- grandparent(tom, ann).
% Pattern matching and unification:
% 1. Try to unify grandparent(tom, ann) with grandparent(X, Z)
% → X = tom, Z = ann
% 2. Now try to prove the body: parent(tom, Y), parent(Y, ann)
% 3. Try to unify parent(tom, Y) with parent(tom, bob)
% → Y = bob
% 4. Try to unify parent(bob, ann) with parent(bob, ann)
% → Success!
% Answer: yes
Substitution and Variable Binding
A substitution is a mapping from variables to terms. When unification succeeds, it produces a substitution that binds variables to values.
Substitution Notation
% Substitution: {X = tom, Y = bob}
% This means: replace X with tom, replace Y with bob
% Original term: parent(X, Y)
% After substitution: parent(tom, bob)
Applying Substitutions
% Substitution: {X = tom, Y = bob, Z = ann}
% Apply to parent(X, Y)
% Result: parent(tom, bob)
% Apply to grandparent(X, Z)
% Result: grandparent(tom, ann)
% Apply to ancestor(X, Y)
% Result: ancestor(tom, bob)
Composing Substitutions
% Substitution 1: {X = Y}
% Substitution 2: {Y = tom}
% Composed: {X = tom, Y = tom}
% Original term: parent(X, Y)
% After substitution 1: parent(Y, Y)
% After substitution 2: parent(tom, tom)
Unification Failures
Understanding why unification fails is important for debugging logic programs.
Failure Reasons
Different functors:
% parent(tom, bob) does NOT unify with grandparent(tom, bob)
% Reason: Different functors (parent vs grandparent)
Different arities:
% parent(tom, bob) does NOT unify with parent(tom)
% Reason: Different arities (2 vs 1)
Different constants:
% parent(tom, bob) does NOT unify with parent(tom, ann)
% Reason: bob ≠ ann
Occurs check failure:
% X does NOT unify with f(X) (with occurs check)
% Reason: X appears in f(X)
Unification in Queries
Query Execution with Unification
% Facts
parent(tom, bob).
parent(bob, ann).
% Query: ?- parent(X, Y).
% Execution:
% 1. Unify parent(X, Y) with parent(tom, bob)
% → X = tom, Y = bob
% → Return first solution
% 2. User asks for more (;)
% 3. Backtrack and unify parent(X, Y) with parent(bob, ann)
% → X = bob, Y = ann
% → Return second solution
% 4. No more facts
% → Done
Query Execution with Rules
% Facts
parent(tom, bob).
parent(bob, ann).
% Rule
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
% Query: ?- grandparent(X, Y).
% Execution:
% 1. Unify grandparent(X, Y) with grandparent(X, Z) (rule head)
% → X = X, Y = Z (no new bindings)
% 2. Try to prove body: parent(X, Y), parent(Y, ann)
% Wait, we need to be more careful here...
%
% Actually:
% 1. Unify grandparent(X, Y) with grandparent(X1, Z1) (rule head with fresh variables)
% → X = X1, Y = Z1
% 2. Try to prove body: parent(X1, Y1), parent(Y1, Z1)
% 3. Unify parent(X1, Y1) with parent(tom, bob)
% → X1 = tom, Y1 = bob
% 4. Unify parent(Y1, Z1) with parent(bob, ann)
% → Y1 = bob (already bound), Z1 = ann
% 5. Success! X = tom, Y = ann
Best Practices
1. Understand Variable Scope
Variables in a clause are local to that clause. Each time a rule is used, fresh variables are created.
% Rule
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
% Query 1: ?- grandparent(tom, ann).
% Uses fresh variables: X, Y, Z
% Query 2: ?- grandparent(bob, jim).
% Uses fresh variables: X, Y, Z (different from Query 1)
2. Use Meaningful Variable Names
% Good
grandparent(GrandParent, GrandChild) :-
parent(GrandParent, Parent),
parent(Parent, GrandChild).
% Less clear
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
3. Be Aware of Unification Order
The order of unification can affect performance.
% Less efficient: Unifies with all facts first
?- parent(X, Y), age(X, A), A > 50.
% More efficient: Filters early
?- age(X, A), A > 50, parent(X, Y).
4. Avoid Infinite Unification
Be careful with recursive rules to avoid infinite loops.
% Bad: Can cause infinite recursion
ancestor(X, Y) :- ancestor(X, Z), parent(Z, Y).
% Good: Base case first
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
Glossary
- Unification: Process of making two terms identical through variable binding
- Pattern matching: Comparing a query against facts and rules using unification
- Substitution: Mapping from variables to terms
- Variable binding: Assigning a value to a variable
- Occurs check: Checking if a variable appears in the term it’s being unified with
- Functor: The name of a compound term (e.g., parent in parent(tom, bob))
- Arity: The number of arguments a functor takes
- Ground term: A term containing no variables
- Compound term: A term with a functor and arguments
- Atom: A basic constant (e.g., tom, bob)
- Unification failure: When two terms cannot be made identical
- Fresh variables: New variables created each time a rule is used
Practice Problems
Problem 1: Unification
Which of the following pairs unify? For those that do, show the substitution.
parent(tom, bob)withparent(X, Y)parent(tom, bob)withparent(tom, tom)f(a, g(b))withf(X, g(Y))[1, 2, 3]with[H|T]Xwithf(X)(with occurs check)
Solution:
- ✓ Unifies: X = tom, Y = bob
- ✗ Does not unify (bob ≠ tom)
- ✓ Unifies: X = a, Y = b
- ✓ Unifies: H = 1, T = [2, 3]
- ✗ Does not unify (occurs check fails)
Problem 2: Pattern Matching
Given the facts:
employee(alice, engineering, 80000).
employee(bob, sales, 60000).
employee(charlie, engineering, 75000).
What are the results of these queries?
?- employee(alice, D, S).?- employee(X, engineering, S).?- employee(X, Y, 80000).
Solution:
- D = engineering, S = 80000
- X = alice, S = 80000 ; X = charlie, S = 75000
- X = alice, Y = engineering
Problem 3: Unification with Rules
Given:
parent(tom, bob).
parent(bob, ann).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
Trace the unification process for: ?- grandparent(tom, ann).
Solution:
- Unify grandparent(tom, ann) with grandparent(X, Z) → X = tom, Z = ann
- Try to prove parent(tom, Y), parent(Y, ann)
- Unify parent(tom, Y) with parent(tom, bob) → Y = bob
- Unify parent(bob, ann) with parent(bob, ann) → Success!
- Answer: yes
Problem 4: Complex Unification
Given:
person(john, info(age(25), city(new_york))).
person(mary, info(age(30), city(london))).
What are the results of:
?- person(john, info(age(A), city(C))).?- person(X, info(age(30), city(Y))).
Solution:
- A = 25, C = new_york
- X = mary, Y = london
Related Resources
Online Platforms
- SWI-Prolog Official - Leading Prolog implementation
- Learn Prolog Now! - Interactive tutorial
- Prolog Tutorial - Comprehensive guide
- Unification Visualizer - Trace unification
- Prolog Playground - Web-based IDE
Interactive Tools
- SWISH - Web-based Prolog IDE
- Prolog Online Compiler - Quick testing
- Prolog Debugger - Trace execution
- Unification Tracer - Step through unification
- Pattern Matching Visualizer - Visualize matching
Recommended Books
- “Programming in Prolog” by Clocksin & Mellish - Classic introduction
- “The Art of Prolog” by Sterling & Shapiro - Advanced techniques
- “Logic Programming: The 1st and 2nd Conferences” - Historical perspective
- “Prolog and Natural Language Analysis” by Pereira & Shieber - NLP applications
- “Constraint Logic Programming” by Jaffar & Maher - CLP overview
Academic Journals
- Journal of Logic Programming - Primary research
- Theory and Practice of Logic Programming - Current research
- ACM Transactions on Programming Languages - Language design
- Artificial Intelligence - AI applications
- Computational Linguistics - NLP applications
Software Tools
- SWI-Prolog - Most popular Prolog
- GNU Prolog - Free implementation
- XSB Prolog - Tabling support
- Ciao Prolog - Modern Prolog
- Datalog Educational System - Datalog learning
Conclusion
Unification and pattern matching are the core mechanisms that enable logic programming:
- Unification makes two terms identical through variable binding
- Pattern matching uses unification to compare queries against facts and rules
- Substitutions track variable bindings throughout computation
- Backtracking explores alternative unifications when one fails
Mastering unification and pattern matching is essential for understanding how logic programs work and for writing correct and efficient programs.
In the next level, we’ll explore more advanced topics in formal systems and automated reasoning.
Previous Article: Facts, Rules, and Queries
Comments