Unification in Ruby

bindings.rb

require 'set'

class Bindings

  ################
  #              #
  # Declarations #
  #              #
  ################
  
  attr_reader :bindings

  ###############
  #             #
  # Constructor #
  #             #
  ###############
  
  def initialize
    @bindings = Hash.new { |hash, variable| hash[variable] = Set.new([variable]) }
  end

  ####################
  #                  #
  # Instance Methods #
  #                  #
  ####################
  
  def []=(variable, item)
    return if variable == item

    value = @bindings[variable]

    if item.kind_of? Symbol
      merge value, @bindings[item]
    else
      assign value, item
    end
  end

  def build
    yield self
    @bindings
  end

  private

  def assign(variable_set, item)
    variable_set.each do |variable|
      throw :unification_failed if occurs?(variable, item)

      @bindings[variable] = item
    end

    simplify_bindings
  end

  def merge(value_1, value_2)
    if value_1 == value_2
      return
    elsif value_1.kind_of?(Set) && value_2.kind_of?(Set)
      new_set = value_1 | value_2
      assign(new_set, new_set)
    elsif value_1.kind_of?(Set)
      assign(value_1, value_2)
    elsif value_2.kind_of?(Set)
      assign(value_2, value_1)
    else
      throw :unification_failed
    end
  end

  def simplify_bindings
    @bindings.each do |variable, value|
      @bindings[variable] = substitute(value)
    end
  end

  def substitute(item)
    case item
    when Array  then substitute_array(item)
    when Symbol then substitute_variable(item)
                else item
    end
  end

  def substitute_array(array)
    array.map { |item| substitute(item) }
  end

  def substitute_variable(variable)
    if ! @bindings.has_key?(variable)
      variable
    elsif @bindings[variable].kind_of?(Set)
      variable
    else
      substitute(@bindings[variable])
    end
  end

  def occurs?(variable, item)
    return true if item == variable
    return false unless item.kind_of? Array
    
    item.any? { |inside| occurs? variable, inside }
  end

end

unification.shard.rb

require_relative 'bindings'

class Unification

  attr_reader :statements, :unification

  ###############
  #             #
  # Constructor #
  #             #
  ###############
  
  def initialize(statements)
    @statements = statements
  end

  #################
  #               #
  # Class Methods #
  #               #
  #################
  
  def self.[](*statements)
    new(statements).unify
  end

  ####################
  #                  #
  # Instance Methods #
  #                  #
  ####################
  
  def unify
    catch(:unification_failed) do
      Bindings.new.build do |bindings|
        @bindings = bindings

        (statements.length - 1).times do |idx|
          unify_items statements[idx], statements[idx+1]
        end
      end
    end
  end

  private

  # Arrays

  def unify_array(array, other)
    case other
    when Symbol then @bindings[other] = array
    when Array  then unify_array_with_array(other, array)
                else throw :unification_failed
    end
  end

  def unify_array_with_array(array_1, array_2)
    throw :unification_failed unless array_1.length == array_2.length

    array_1.zip(array_2).each do |item_1, item_2|
      unify_items(item_1, item_2)
    end
  end

  # Items

  def unify_items(item_1, item_2)
    case item_1
    when Symbol then @bindings[item_1] = item_2
    when Array  then unify_array(item_1, item_2)
                else unify_term(item_1, item_2)
    end
  end

  # Terms

  def unify_term(term, other)
    if other.kind_of? Symbol
      @bindings[other] = term
    elsif term != other
      throw :unification_failed
    end
  end

end

unification_spec.rb

gem 'minitest'
require 'minitest/autorun'

require_relative 'unification.shard'

describe "Unification" do

  it "unifies similar atoms" do
    Unification['abc', 'abc'].must_equal Hash.new
  end
  
  it "doesn't unify different atoms" do
    Unification['abc', 'xyz'].must_equal nil
  end

  it "should unify like symbols" do
    Unification[:x, :x].must_equal Hash.new
  end
  
  it "unifies a variable with an atom" do
    Unification[ :x, 'abc' ].must_equal(x: 'abc')
  end

  it "unifies two variables" do
    Unification[ :x, :y ].must_equal(x: Set[:x, :y], y: Set[:x, :y])
  end

  it "unifies a variable in a function" do
    Unification[ ['f', :x, :y], ['f', :x, 'a'] ].must_equal(y: 'a')
  end

  it "doesn't unify different functions" do
    Unification[ ['f', :x], ['g', :y] ].must_equal nil
  end
  
  it "doesn't unify functions of different arity" do
    Unification[ ['f', :x], ['f', :x, :y] ].must_equal nil
  end

  it "unifies a variable with a function" do
    Unification[ ['f', :x], ['f', ['g', :y]] ].must_equal x: ['g', :y]
  end

  it "unifies..." do
    Unification[ ['f', ['g', :x], :x], ['f', :y, 'a'] ].must_equal x: 'a', y: ['g', 'a']
  end

  it "should unify across statements" do
    Unification[:x, :y, :y, 'abc'].must_equal x: 'abc', y: 'abc'
  end
  
  it "should unify function arguments" do
    Unification[ ['f', :x], ['f', :y] ].must_equal x: Set[:x, :y], y: Set[:x, :y]
  end
  
  it "should not unify a variable with a function that contains that variable" do
    Unification[ :x, ['f', :x] ].must_equal nil
  end
  
end