# Unification

**URL:** <https://swi-prolog.discourse.group/t/unification/691>\
**Category:** Wiki\
**Created:** [May 21, 2019, 5:13pm UTC](https://swi-prolog.discourse.group/t/unification/691 "2019-05-21T17:13:33Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Wiki](https://avatars.discourse-cdn.com/v4/letter/w/e8c25b/32.png) [@Wiki](https://swi-prolog.discourse.group/u/Wiki)\
**Post date:** [May 21, 2019, 5:13pm UTC](https://swi-prolog.discourse.group/t/unification/691/1 "2019-05-21T17:13:34Z")

</div>

How to: [Unification](http://www.swi-prolog.org/pldoc/man?predicate=%3D/2)

> 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](https://swi-prolog.discourse.group/t/wiki-discussion-how-to-unification/692)

> 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](https://swi-prolog.discourse.group/t/wiki-discussion-how-to-unification/692)

> Note: This is a wiki and if you have [Trust level](https://blog.discourse.org/2018/06/understanding-discourse-trust-levels/): [Basic](https://swi-prolog.discourse.group/badges/1/basic) you can edit this by clicking on the pencil icon in the lower right. ![Capture](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/bfd4c3b77dc7f3f98ece3d5ae3202fcccb0fb8b3.png)  
> These topics also have history so they can be rolled-back if needed.

* * *

While there are ways of unifying, e.g. [e-unification](https://en.wikipedia.org/wiki/Unification_(computer_science)#E-unification), this is only going to talk about [syntactic unification](https://en.wikipedia.org/wiki/Unification_(computer_science)#Examples_of_syntactic_unification_of_first-order_terms) 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](http://www.swi-prolog.org/pldoc/man?predicate=write_canonical/1)

#### Unification Examples

Based on [Wikipedia](https://en.wikipedia.org/wiki/Unification_(computer_science)#Examples_of_syntactic_unification_of_first-order_terms)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/47d1ddb5fd4237ac2532cc95b29f06e5d25398de.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/332271277b716e1b949a4864b770dd9750348521.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/c2e46e9142f99a4a6726967e781db581dab34b5e.png)

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

![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/36edff92361f911a6868fdca3a66d58f4588d311.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/5b6a25c769cf0af3867f058d39459835667e0760.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/17356018d18f98688f1380cb47808f7ccbd5af3c.png)

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

![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/c833d1194c25da423306224adb0cd6083cb14495.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/e0185580ab8d202564d0415306583c1708b6ba32.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/e5ed11dc470737564c4eb67ca85ef423a6e02d5b.png)

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

![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/2658dc4f808427ff2016d99b209220aaa5ae4ddd.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/cdcfb75d3a4921ff87487e35da7ea1cef8814c49.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/3d4b06d27f7454f7ed6f7d2d587bb25b58a0efe3.png)

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

![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/353f22eb4de1836dab74e45cdccea138795d5fd4.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/3d32538389e480463e6cd152b876fc67463eaf56.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/4d661f136a6fcf7c1910af6820f7ce331b720353.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/3a7476743d6c132e9236cf3dcebb1c3de39af587.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/6777a6942db5b0a689ed67d60f69d350cb2b8a2f.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/188b9de8f3301f43e1076b0c671db1976f26c120.png)

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

![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/5731c98d6f2014049851bdabb77b432ec582aa05.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/b51426191bb099d0c02b56f1b9695aaa65cb9792.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/b0587da8066af7894eeaa27bb234ce947e1347cd.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/1167e8fe02312ce60ca0fc26ed10dd81f1a4f9b2.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/d7ee2d4adef2e71eb630acf5490046156c14bc4c.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/7031de50ae7550bfb0b9dfacff78a5a856470ab4.png)

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

![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/53d4ab848219a58d43ae6cb2d536445c39760c68.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/67e2b2b5d7d6ba33324e8bfa2f24e21aee2aa10f.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/667778551e8d68fbb2ca31985e34e32bdbf85ce3.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/910d0bf46b35cd7e9f3650454c2df461bd20c1b0.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/acc69382519e0a29e6e1ba45e38c07855968ee5e.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/a04942d959d67e9f430486999407ce95a781943a.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/7e61323c9c4c84577a2a1dd5016949969fa64004.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/932bd92672fcbd83f553afdd4c1859281d9f4ce2.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/aeb26d232ef06fc9173e6f5c808840a3624a1d48.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/281efbf16d0c3d17ec22d3c42eb99e45bed57358.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/4d7692a11d90585104858e2b6da7162986743b88.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/f46481df47eaa7d0567cddcc76f7cd49a36af780.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/3dd4d2daaa9b83f9f5f924c7f8976333c29c61b4.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/f3e6ffddca863065b2af7301fbe4eed3b0ec146a.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/5e8af2fb12386317fd345d7e44351f22930a36b7.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/d51371e8b714b77dbd3294f74c8511126d2a2a86.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/dd5a1cbb4573a71fd0e0862021a5fc42a2f02c03.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/2fa47aea27f1e77ff7872513b3728a634cf56548.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/47a88ddb227f03ef96bcb3e71d1abd8022baaffa.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/8fa0025ea528d6cd0d107fb5809ee319b0c30146.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/97806c47c522c1e6cd888004e420a024ac813704.png)

| 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](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/202b91daff5acbf52749da45efc4bb9eb82688f2.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/bd24bbbfe762aba8addb16c69b134e7cf798e627.png)  
 ![image](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/1X/c7b80e287ae24e683181dff833b308e85aecdcdf.png)

* * *

For a visual representation that shows the unification/substitutions durning the executation of simple Prolog programs see: [Prolog Visualizer](https://swi-prolog.discourse.group/t/prolog-visualizer/2841)