Unification

How to: Unification

Note: This is a work in progress. When it is complete these notes will be removed.

Note: Do not reply to this topic, questions, concerns, comments, etc. are to handled in
Wiki Discussion: How to - Unification

Note: This is just to get the topic started and hopefully others to jump in and make this useful. Even if you are brand new to Prolog, this is such a basic and fundamental concept that you can and should join in to help improve the value of this Wiki. Join the discussion at Wiki Discussion: How to - Unification

Note: This is a wiki and if you have Trust level: Basic you can edit this by clicking on the pencil icon in the lower right. Capture
These topics also have history so they can be rolled-back if needed.


While there are ways of unifying, e.g. e-unification, this is only going to talk about syntactic unification as used in Prolog.

For unification of syntax there is basically only three things to be aware of

  1. Values
  2. Variables
  3. Structures that have a name as a value and are made up of values, variables and structures.

A value is a constant that will not change.
A variable can change but only once, hence the words unbound and bound as opposed to assigned.
A structure will have name called a functor and one or more arguments. While some things may not seem like structures such as list, [a,b,c] they really are in concept. See write_canonical/1

Unification Examples

Based on Wikipedia

Symbols
Variables Constants
In Prolog: Start with upper case letter In Prolog: Start with lower case letter
X Y Z a b f g
Δ Φ Ω π λ ε
⌂ ⌀ ⌘ ☃ ⍟ ∎
Rectangles Ovals

a = a π = π ☃ = ☃
Unify: true
MGU: {}
Unify: true
MGU: {}
Unify: true
MGU: {}
SWI-Prolog:
?- =(a,a).
true.
SWI-Prolog:
?- =(π,π).
true.
SWI-Prolog:
?- =(☃,☃).
true.

image
image
image

a = b π = λ ☃ = ⍟
Unify: false Unify: false Unify: false
SWI-Prolog:
?- =(a,b).
false.
SWI-Prolog:
?- =(π,λ).
false.
SWI-Prolog:
?- =(☃,⍟).
false.

image
image
image

X = X Δ = Δ ⌂ = ⌂
Unify: true
MGU: {}
Unify: true
MGU: {}
Unify: true
MGU: {}
SWI-Prolog:
?- =(X,X).
true.
SWI-Prolog:
?- =(Δ,Δ).
true.
SWI-Prolog:
?- =(⌂,⌂).
true.

image
image
image

a = X π = Δ ☃ = ⌂
Unify: true
MGU: { X ↦ a }
Unify: true
MGU: { Δ ↦ π }
Unify: true
MGU: { ⌂ ↦ ☃ }
SWI-Prolog:
?- =(a,X).
X = a.
SWI-Prolog:
?- =(π,Δ).
Δ = π.
SWI-Prolog:
?- =(☃,⌂).
⌂ = ☃.

image
image
image

X = Y Δ = Φ ⌂ = ⌀
Unify: true
MGU: { X ↦ Y }
Unify: true
MGU: { Δ ↦ Φ }
Unify: true
MGU: { ⌂ ↦ ⌀ }
SWI-Prolog:
?- =(X,Y).
X = Y.
SWI-Prolog:
?- =(Δ,Φ).
Δ = Φ.
SWI-Prolog:
?- =(⌂,⌀).
⌂ = ⌀.

image
image
image

f(a,X) = f(a,b) λ(π,Φ) = λ(π,ε) ⍟(☃,⌀) = ⍟(☃,∎)
Unify: true
MGU: { X ↦ b }
Unify: true
MGU: { Φ ↦ ε }
Unify: true
MGU: { ⌀ ↦ ∎ }
SWI-Prolog:
?- =(f(a,X),f(a,b)).
X = b.
SWI-Prolog:
?- =(λ(π,Φ),λ(π,ε)).
Φ = ε.
SWI-Prolog:
?- =(⍟(☃,⌀),⍟(☃,∎)).
⌀ = ∎.

image
image
image

f(a) = g(a) ε(λ) = π(λ) ∎(⍟) = ☃(⍟)
Unify: false Unify: false Unify: false
SWI-Prolog:
?- =(f(a),g(a)).
false.
SWI-Prolog:
?- =(ε(λ),π(λ)).
false.
SWI-Prolog:
?- =(∎(⍟),☃(⍟)).
false.

image
image
image

f(X) = f(Y) π(Ω) = π(Δ) ☃(⌘) = ☃(⌂)
Unify: true
MGU: { X ↦ Y }
Unify: true
MGU: { Ω ↦ Δ }
Unify: true
MGU: { ⌘ ↦ ⌂ }
SWI-Prolog:
?- =(f(X),f(Y)).
X = Y.
SWI-Prolog:
?- =(π(Ω),π(Δ)).
Ω = Δ.
SWI-Prolog:
?- =(☃(⌘),☃(⌂)).
⌘ = ⌂.

image
image
image

f(X) = g(Y) ε(Ω) = π(Φ) ∎(⌘) = ☃(⌀)
Unify: false Unify: false Unify: false
SWI-Prolog:
?- =(f(X),g(Y)).
false.
SWI-Prolog:
?- =(ε(Ω),π(Φ)).
false.
SWI-Prolog:
?- =(∎(⌘),☃(⌀)).
false.

image
image
image

f(X) = f(Y,Z) λ(Ω) = λ(Φ,Δ) ⍟(⌘) = ⍟(⌀,⌂)
Unify: false Unify: false Unify: false
SWI-Prolog:
?- =(f(X),f(Y,Z)).
false.
SWI-Prolog:
?- =(λ(Ω),λ(Φ,Δ)).
false.
SWI-Prolog:
?- =(⍟(⌘),⍟(⌀,⌂)).
false.

image
image
image

f(g(X)) = f(Y) π(λ(Φ)) = π(Δ) ☃(⍟(⌀)) = ☃(⌂)
Unify: true
MGU: { Y ↦ g(X) }
Unify: true
MGU: { Δ ↦ λ(Φ) }
Unify: true
MGU: { ⌂ ↦ ⍟(⌀) }
SWI-Prolog:
?- =(f(g(X)),f(Y)).
Y = g(X).
SWI-Prolog:
?- =(π(λ(Φ)),π(Δ)).
Δ = λ(Φ).
SWI-Prolog:
?- =(☃(⍟(⌀)),☃(⌂)).
⌂ = ⍟(⌀).

image
image
image

f(g(X),X) = f(Y,a) ε(λ(Φ),Φ) = ε(Δ,π) ∎(⍟(⌀),⌀) = ∎(⌂,☃)
Unify: true
MGU: { X ↦ a, Y ↦ g(a) }
Unify: true
MGU: { Φ ↦ π, Δ ↦ λ(π) }
Unify: true
MGU: { ⌀ ↦ ☃, ⌂ ↦ ⍟(☃) }
SWI-Prolog:
?- =(f(g(X),X),f(Y,a)).
X = a,
Y = g(a).
SWI-Prolog:
?- =(ε(λ(Φ),Φ),ε(Δ,π)).
Φ = π,
Δ = λ(π).
SWI-Prolog:
?- =(∎(⍟(⌀),⌀),∎(⌂,☃)).
⌀ = ☃,
⌂ = ⍟(☃).

image
image
image

X = f(X) Φ = π(Φ) ⌀ = ☃(⌀)
Unify: false
Occurs check: fails
Unify: false
Occurs check: fails
Unify: false
Occurs check: fails
SWI-Prolog:
?- =(X,f(X)).
X = f(X).
SWI-Prolog:
?- =(Φ,π(Φ)).
Φ = π(Φ).
SWI-Prolog:
?- =(⌀,☃(⌀)).
⌀ = ☃(⌀).
SWI-Prolog:
?- unify_with_occurs_check(X,f(Y,X))
false.
SWI-Prolog:
?- unify_with_occurs_check(Φ,π(Φ)).
false.
SWI-Prolog:
?- unify_with_occurs_check(⌀,☃(⌀)).
false.

image
image
image

X = Y,
Y = a
Ω = Δ,
Δ = ε
⌘ = ⌂,
⌂ = ∎
Unify: true
MGU: { Y ↦ a, X ↦ a }
Unify: true
MGU: { Δ ↦ ε, Ω ↦ ε }
Unify: true
MGU: { ⌂ ↦ ∎, ⌘ ↦ ∎ }
SWI-Prolog:
?- X=Y,Y=a.
X = Y, Y = a.
or
?- =(X,Y),=(Y,a).
X = Y, Y = a.
SWI-Prolog:
?- Ω=Δ,Δ=ε.
Ω = Δ, Δ = ε.
or
?- =(Ω,Δ),=(Δ,ε).
Ω = Δ, Δ = ε.
SWI-Prolog:
?- ⌘=⌂,⌂=∎.
⌘ = ⌂, ⌂ = ∎.
or
?- =(⌘,⌂),=(⌂,∎).
⌘ = ⌂, ⌂ = ∎.

image
image
image

a = Y,
X = Y
λ = Φ,
Δ = Φ
⍟ = ⌀,
⌂ = ⌀
Unify: true
MGU: { Y ↦ a, X ↦ a }
Unify: true
MGU: { Φ ↦ λ, Δ ↦ λ }
Unify: true
MGU: { ⌀ ↦ ⍟, ⌂ ↦ ⍟ }
SWI-Prolog:
?- a=Y,X=Y.
Y = X, X = a.
or
?- =(a,Y),=(X,Y).
Y = X, X = a.
SWI-Prolog:
?- λ=Φ,Δ=Φ.
Φ = Δ, Δ = λ.
or
?- =(λ,Φ),=(Δ,Φ).
Φ = Δ, Δ = λ.
SWI-Prolog:
?- ⍟=⌀,⌂=⌀.
⌀ = ⌂, ⌂ = ⍟.
or
?- =(⍟,⌀),=(⌂,⌀).
⌀ = ⌂, ⌂ = ⍟.

image
image
image

X = a,
b = X
Δ = λ,
ε = Δ
⌂ = ⍟,
∎ = ⌂
Unify: false Unify: false Unify: false
SWI-Prolog:
?- X=a,b=X.
false.
or
?- =(X,a),=(b,X).
false.
SWI-Prolog:
?- Δ=λ,ε=Δ.
false.
or
?- =(Δ,λ),=(ε,Δ).
false.
SWI-Prolog:
?- ⌂=⍟,∎=⌂.
false.
or
?- =(⌂,⍟),=(∎,⌂).
false.

image
image
image


For a visual representation that shows the unification/substitutions durning the executation of simple Prolog programs see: Prolog Visualizer

2 Likes