C#: first-order unification

Before you start

C# classes, recursion, and dictionaries.

Find a substitution that makes two logical terms identical, including the occurs check.
Predict the sample output and explain the state changes.
Complete the practice task and check the boundary cases.

The concept

Unification is the matching step at the heart of Prolog and of automated theorem provers. Two terms unify if there is a substitution of variables that makes them identical. By convention variables start with an uppercase letter and constants with a lowercase one, so f(X, b) and f(a, Y) unify with X = a and Y = b.

The algorithm compares the terms recursively. A variable is bound to the other term, unless it is already bound, in which case the binding is followed. Two compound terms must have the same name and arity and their arguments must unify pairwise. The occurs check rejects a binding such as X = g(X), which would build an infinite term.

Code example

using System;
using System.Collections.Generic;
using System.Linq;

class Term {
  public string Name;
  public Term[] Args;

  public Term(string name, params Term[] args) {
    Name = name;
    Args = args;
  }

  public bool IsVariable { get { return Args.Length == 0 && char.IsUpper(Name[0]); } }

  public override string ToString() {
    return Args.Length == 0 ? Name : Name + "(" + string.Join(",", Args.Select(a => a.ToString())) + ")";
  }
}

class Program {
  static Term Walk(Term t, Dictionary<string, Term> s) {
    while (t.IsVariable && s.ContainsKey(t.Name)) {
      t = s[t.Name];
    }
    return t;
  }

  static bool Occurs(string variable, Term t, Dictionary<string, Term> s) {
    t = Walk(t, s);
    if (t.IsVariable) return t.Name == variable;
    return t.Args.Any(a => Occurs(variable, a, s));
  }

  static bool Unify(Term x, Term y, Dictionary<string, Term> s) {
    x = Walk(x, s);
    y = Walk(y, s);
    if (x.IsVariable && y.IsVariable && x.Name == y.Name) return true;
    if (x.IsVariable) {
      if (Occurs(x.Name, y, s)) return false;
      s[x.Name] = y;
      return true;
    }
    if (y.IsVariable) return Unify(y, x, s);
    if (x.Name != y.Name || x.Args.Length != y.Args.Length) return false;
    for (int i = 0; i < x.Args.Length; i++) {
      if (!Unify(x.Args[i], y.Args[i], s)) return false;
    }
    return true;
  }

  static void Try(Term a, Term b) {
    var s = new Dictionary<string, Term>();
    if (Unify(a, b, s)) {
      string bindings = string.Join(", ", s.OrderBy(p => p.Key).Select(p => p.Key + "=" + p.Value));
      Console.WriteLine(a + " ~ " + b + ": " + bindings);
    } else {
      Console.WriteLine(a + " ~ " + b + ": fail");
    }
  }

  static void Main() {
    Term X = new Term("X"), Y = new Term("Y"), a = new Term("a"), b = new Term("b"), mary = new Term("mary"), john = new Term("john");
    Try(new Term("f", X, b), new Term("f", a, Y));
    Try(new Term("loves", X, mary), new Term("loves", john, X));
    Try(new Term("f", X), new Term("f", new Term("g", X)));
  }
}

Output

f(X,b) ~ f(a,Y): X=a, Y=b
loves(X,mary) ~ loves(john,X): fail
f(X) ~ f(g(X)): fail

Example details

Follow the code

Open the walkthrough to inspect the example one step at a time.

Show guided walkthrough

Guided walkthroughReady

1using System;

2using System.Collections.Generic;

3using System.Linq;

5class Term {

6 public string Name;

7 public Term[] Args;

9 public Term(string name, params Term[] args) {

10 Name = name;

11 Args = args;

12 }

14 public bool IsVariable { get { return Args.Length == 0 && char.IsUpper(Name[0]); } }

16 public override string ToString() {

17 return Args.Length == 0 ? Name : Name + "(" + string.Join(",", Args.Select(a => a.ToString())) + ")";

18 }

19}

21class Program {

22 static Term Walk(Term t, Dictionary<string, Term> s) {

23 while (t.IsVariable && s.ContainsKey(t.Name)) {

24 t = s[t.Name];

25 }

26 return t;

27 }

29 static bool Occurs(string variable, Term t, Dictionary<string, Term> s) {

30 t = Walk(t, s);

31 if (t.IsVariable) return t.Name == variable;

32 return t.Args.Any(a => Occurs(variable, a, s));

33 }

35 static bool Unify(Term x, Term y, Dictionary<string, Term> s) {

36 x = Walk(x, s);

37 y = Walk(y, s);

38 if (x.IsVariable && y.IsVariable && x.Name == y.Name) return true;

39 if (x.IsVariable) {

40 if (Occurs(x.Name, y, s)) return false;

41 s[x.Name] = y;

42 return true;

43 }

44 if (y.IsVariable) return Unify(y, x, s);

45 if (x.Name != y.Name || x.Args.Length != y.Args.Length) return false;

46 for (int i = 0; i < x.Args.Length; i++) {

47 if (!Unify(x.Args[i], y.Args[i], s)) return false;

48 }

49 return true;

50 }

52 static void Try(Term a, Term b) {

53 var s = new Dictionary<string, Term>();

54 if (Unify(a, b, s)) {

55 string bindings = string.Join(", ", s.OrderBy(p => p.Key).Select(p => p.Key + "=" + p.Value));

56 Console.WriteLine(a + " ~ " + b + ": " + bindings);

57 } else {

58 Console.WriteLine(a + " ~ " + b + ": fail");

59 }

60 }

62 static void Main() {

    Term X = new Term("X"), Y = new Term("Y"), a = new Term("a"), b = new Term("b"), mary = new Term("mary"), john = new Term("john");

64 Try(new Term("f", X, b), new Term("f", a, Y));

65 Try(new Term("loves", X, mary), new Term("loves", john, X));

66 Try(new Term("f", X), new Term("f", new Term("g", X)));

67 }

68}

Follow the example

Start to inspect the source, values, and output. These prepared steps explain the published sample; grouped loop steps describe multiple iterations.

View the complete dry-run table

Prepared trace of the published program. Some rows group repeated iterations.
What happens	State after step	Output so far
A term with no arguments and an uppercase name is a variable.	`—`	—
The occurs check refuses to bind a variable to a term that contains it.	`—`	—
X is bound to a, then b is matched with Y.	`X = a, Y = b`	f(X,b) ~ f(a,Y): X=a, Y=b
X is bound to john, then X (now john) must equal mary, which fails.	`X = john, then john ≠ mary`	f(X,b) ~ f(a,Y): X=a, Y=b loves(X,mary) ~ loves(john,X): fail
X would have to equal g(X), an infinite term; the occurs check rejects it.	`X = john, then john ≠ mary`	f(X,b) ~ f(a,Y): X=a, Y=b loves(X,mary) ~ loves(john,X): fail f(X) ~ f(g(X)): fail

Behind the scenes

How C# processes this code

C# compiles to code for the .NET runtime, which invokes the program entry point.

Cost and common mistakes

Linear-time algorithms exist. This simple version is worst-case quadratic or exponential in term size because of repeated walks.

Skipping the occurs check is faster, and many Prolog systems do it by default, but it can produce cyclic terms and unsound results.
Follow existing bindings (Walk) before comparing, or an earlier binding can be silently overwritten.

Try it yourself

Do p(X, X) and p(a, b) unify?

Reveal answer and reasoning

No: X is bound to a, and then a must equal b, which fails.