C#: first-order unification

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.

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)));
  }
}

Read the full lesson