Unification

First-order Unification

Below an implementation of the unification procedure for first-order functional expressions.

The internal AST representation of functional terms employed in our unification procedure consists in:

• Term variables: They are the “atomic” expressions. As the name indicates, they are variables that can be substituted for terms (by applying a substitution). Their internal representation is as pairs of the form: {:tvar, <variable_name>} where <variable_name> is an Elixir atom.
• Function applications: It is the “constructor” for complex expressions. They are triples of the form {:app, <function_symbol>, <argument_list>}, where the <function_symbol> represents an n-ary function (which is not a variable!) and <argument_list> is an n-sized list of expressions. For instance, the expression “f(g(x), y)” is input in Elixir as f(g(:x), :y), which ends up becoming represented in our own AST as {:app, :f, [{:app, :g, [{:tvar, :x}]}, {:tvar, :y}]}.

Our AST for functional expressions has been conveniently chosen as a slightly modified version of Elixir’s. This way we can employ Elixir’s syntax for functional expressions as input syntax for our procedure, while reusing Elixir’s parser to seamlessly transform Elixir ASTs into our own ASTs (see quote/unquote).

defmodule Unification do
  # Basic wrapper
  def unify(eqs) when is_list(eqs), do: unify(eqs, Map.new())
  def unify({_, _} = eq), do: unify([eq], Map.new())
  def unify(a, b) when is_tuple(a) and is_tuple(b), do: unify({a, b})

  # Finish 
  def unify([], subst), do: {:ok, make_idempotent(subst)}

  # Same term: trivially unifiable, drop silently
  def unify([{t, t} | rest], subst), do: unify(rest, subst)

  # Variable on the lhs: occurrence and collision checks, updates substitution and applies to rest
  def unify([{{:tvar, x}, term} | rest], subst) do
    if occurs?(term, x) do
      {:error, "occurs-check failed for '#{inspect(x)}'"}
    else
      previous_value = Map.get(subst, x)

      if previous_value != nil && previous_value != term do
        {:error, "not unifiable: colliding variable assignments for '#{inspect(x)}'"}
      else
        new_subst = Map.put(subst, x, term)
        term_subst = as_term_subst(new_subst)
        new_rest = Enum.map(rest, fn {l, r} -> {term_subst.(l), term_subst.(r)} end)
        unify(new_rest, new_subst)
      end
    end
  end

  # Variable on the rhs: reverse equation
  def unify([{term, {:tvar, x}} | rest], subst), do: unify([{{:tvar, x}, term} | rest], subst)

  # Function application: decompose recursively
  def unify([{{:app, f, args1}, {:app, f, args2}} | rest], subst)
      when length(args1) == length(args2) do
    unify(Enum.zip(args1, args2) ++ rest, subst)
  end

  # No match: error
  def unify(x, _subst), do: {:error, "not unifiable: expression '#{inspect(x)}' didn't match"}

  # Whether a variable occurs in a term
  def occurs?({:tvar, v}, x), do: v == x
  def occurs?({:app, _f, args}, x), do: Enum.any?(args, &occurs?(&1, x))

  # Applies a substitution to a term
  def substitute({:tvar, x} = v, subst), do: subst[x] || v
  def substitute({:app, f, args}, subst), do: {:app, f, Enum.map(args, &substitute(&1, subst))}

  # Converts into an idempotent substitution (via fixed-point construction)
  def make_idempotent(subst) do
    term_subst = as_term_subst(subst)
    term_subst2 = compose_fun(term_subst, term_subst)
    subst2 = as_var_subst(term_subst2, Map.keys(subst))
    if subst == subst2, do: subst, else: make_idempotent(subst2)
  end

  # Composes two functions f1 and f2 as: f1 ; f2 (or f2 o f1). Read "f2 after f1"
  def compose_fun(f1, f2), do: fn x -> f2.(f1.(x)) end

  # Converts a term-substitution function into a variable-substitution map (wrt. variable-keys)
  def as_var_subst(term_subst, vars),
    do: Map.new(Enum.zip(vars, Enum.map(vars, compose_fun(fn v -> {:tvar, v} end, term_subst))))

  # Converts a variable-substitution map into a term-substitution function
  def as_term_subst(subst), do: fn t -> substitute(t, subst) end

  # Parses Elixir AST as a term (or term pair)
  def parse({:=, _, [l, r]}), do: {parse(l), parse(r)}
  def parse(name) when is_atom(name), do: {:tvar, name}
  def parse({c, _, Elixir}), do: {:app, c, []}
  def parse({f, _, args}) when is_list(args), do: {:app, f, Enum.map(args, &parse/1)}

  # Pretty-prints function application
  def print_term({:app, f, args}) do
    if length(args) == 0 do
      to_string(f)
    else
      "#{to_string(f)}(#{args |> Enum.map(&print_term/1) |> Enum.join(",")})"
    end
  end

  # Pretty-prints variables
  def print_term({:tvar, name}), do: to_string(name)
  def print_term(term), do: to_string(term)

  # Pretty-prints substitution
  def print_substitution(subst) do
    subst |> Map.to_list() |> Enum.map(fn {v, t} -> "#{print_term(v)} ↦ #{print_term(t)}" end)
  end
end

Note that in our input syntax only variables are represented as Elixir atoms (function symbols are written “as is”):

Unification.parse(quote do: f(g(:x), :y))

{:ok, subst} = Unification.unify (Unification.parse quote do: :x = :f)
Unification.print_substitution(subst)

eq1 = Unification.parse quote do: g(:x2) = :x1
eq2 = Unification.parse quote do: f(:x1, h(:x1), :x2) = f(g(:x3), :x4, :x3)
{:ok, subst} = Unification.unify([eq1,eq2])
Unification.print_substitution(subst)

Below some tests from Wikipedia: https://en.wikipedia.org/wiki/Unification_(computer_science)#Examples_of_syntactic_unification_of_first-order_terms

import Unification

{:ok, subst} = unify(parse quote do: a = a)
print_substitution(subst)

{:error, _} = unify(parse quote do: a = b)

{:ok, subst} = unify(parse quote do: :x = :x)
print_substitution(subst)

{:ok, subst} = unify(parse quote do: a = :x)
print_substitution(subst)

{:ok, subst} = unify(parse quote do: :x = :y)
print_substitution(subst)

{:ok, subst} = unify(parse quote do: f(a,:x) = f(a,b))
print_substitution(subst)

{:error, _} = unify(parse quote do: f(a) = g(a))

{:ok, subst} = unify(parse quote do: f(:x) = f(:y))
print_substitution(subst)

{:error, _} = unify(parse quote do: f(:x) = f(:y,:z))

{:ok, subst} = unify(parse quote do: f(g(:x)) = f(:y))
print_substitution(subst)

{:ok, subst} = unify(parse quote do: f(g(:x),:x) = f(:y,a))
print_substitution(subst)

{:error, _} = unify(parse quote do: :x = f(:x))

eq1 = parse quote do: :x = :y
eq2 = parse quote do: :a = :y
{:ok, subst} = unify([eq1,eq2])
print_substitution(subst)

eq1 = parse quote do: :x = a
eq2 = parse quote do: b = :x
{:error, _} = unify([eq1,eq2])

eq1 = parse quote do: :x = a
eq2 = parse quote do: :x = :y
{:ok, subst} = unify([eq1,eq2])
print_substitution(subst)