Syntactic Unification in Java

Unify.java

/* Copyright (C) Freddy A Cubas "superstar64"
Boost Software License - Version 1.0 - August 17th, 2003

Permission is hereby granted, free of charge, to any person or organization
obtaining a copy of the software and accompanying documentation covered by
this license (the "Software") to use, reproduce, display, distribute,
execute, and transmit the Software, and to prepare derivative works of the
Software, and to permit third-parties to whom the Software is furnished to
do so, all subject to the following:

The copyright notices in the Software and this entire statement, including
the above license grant, this restriction and the following disclaimer,
must be included in all copies of the Software, in whole or in part, and
all derivative works of the Software, unless such copies or derivative
works are solely in the form of machine-executable object code generated by
a source language processor.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT
SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE
FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE,
ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
DEALINGS IN THE SOFTWARE.
*/
import java.io.*;
import java.util.*;

abstract class Term {
	abstract void match(Term right, Unify unifier);
	abstract void matchRight(Variable left, Unify unifier);
	abstract void matchRight(Function left, Unify unifier);
	abstract void occurs(String name);
	abstract Term substitute(String name, Term target);
}

class Variable extends Term {
	String name;
	Variable(String name) {
		this.name = name;
	}

	public String toString() {
		return name;
	}

	void match(Term right, Unify unifier) {
		right.matchRight(this, unifier);
	}

	void matchRight(Variable left, Unify unifier) {
		unifier.match(left, this);
	}

	void matchRight(Function left, Unify unifier) {
		unifier.match(left, this);
	}

	void occurs(String name) {
		if(this.name.equals(name)) {
			throw new RuntimeException("Occurance check: " + name);
		}
	}

	Term substitute(String name, Term target) {
		if(this.name.equals(name)) {
			return target;
		} else {
			return this;
		}
	}
}

class Function extends Term {
	String name;
	List<Term> arguments;
	Function(String name, List<Term> arguments) {
		this.name = name;
		this.arguments = arguments;
	}

	public String toString() {
		String result = name;
		result += "(";

		for(int i = 0; i < arguments.size(); i++) {
			result += arguments.get(i).toString();

			if(i != arguments.size() - 1) {
				result += ",";
			}
		}

		result += ")";
		return result;
	}

	void match(Term right, Unify unifier) {
		right.matchRight(this, unifier);
	}

	void matchRight(Variable left, Unify unifier) {
		unifier.match(left, this);
	}

	void matchRight(Function left, Unify unifier) {
		unifier.match(left, this);
	}

	void occurs(String name) {
		for(Term argument : arguments) {
			argument.occurs(name);
		}
	}

	Term substitute(String name, Term target) {
		List<Term> fresh = new ArrayList<>(arguments);

		for(int i = 0; i < fresh.size(); i++) {
			fresh.set(i, fresh.get(i).substitute(name, target));
		}

		return new Function(this.name, fresh);
	}
}

class Equation {
	Term left;
	Term right;
	Equation(Term left, Term right) {
		this.left = left;
		this.right = right;
	}

	public String toString() {
		return left.toString() + "=" + right.toString();
	}

	Equation substitute(String name, Term target) {
		return new Equation(left.substitute(name, target), right.substitute(name, target));
	}
}

class Parser {
	int head;
	InputStream tail;

	Parser(InputStream stream) throws IOException {
		head = stream.read();
		tail = stream;
	}

	void next() throws IOException {
		head = tail.read();
	}

	void space() throws IOException {
		while(head == ' ' || head == '\n' || head == '\r') {
			next();
		}
	}

	String string() throws IOException {
		if(Character.isAlphabetic(head)) {
			String result = "";

			while(Character.isAlphabetic(head)) {
				result += (char)head;
				next();
			}

			space();
			return result;
		}

		return null;
	}

	boolean match(char c) throws IOException {
		if(head == c) {
			next();
			space();
			return true;
		}

		return false;
	}

	Term term() throws IOException {
		String name = string();

		if(name == null) {
			return null;
		}

		if(match('(')) {
			ArrayList<Term> arguments = new ArrayList<>();

			while(!match(')')) {
				Term argument = term();

				if(argument == null) {
					throw new IOException("Expected Term");
				}

				arguments.add(argument);
				match(',');
			}

			return new Function(name, arguments);
		} else {
			return new Variable(name);
		}
	}

	Equation equation() throws IOException {
		Term left = term();

		if(left == null) {
			return null;
		}

		if(!match('=')) {
			throw new IOException("Expected =");
		}

		Term right = term();

		if(right == null) {
			throw new IOException("Expected term");
		}

		return new Equation(left, right);
	}

	List<Equation> equations() throws IOException {
		List<Equation> result = new ArrayList<>();
		Equation equation;

		while((equation = equation()) != null) {
			result.add(equation);
		}

		return result;
	}
}

public class Unify {
	List<Equation> problems;
	Map<String, Term> solution;

	// https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm

	// abuse overloading
	void match(Variable e1, Variable e2) {
		if(!e1.name.equals(e2.name)) {
			matchVariable(e1, e2);
		}
	}
	void match(Variable e1, Function e2) {
		matchVariable(e1, e2);
	}
	void match(Function e1, Variable e2) {
		matchVariable(e2, e1);
	}
	void match(Function e1, Function e2) {
		if(!(e1.name.equals(e2.name) && e1.arguments.size() == e2.arguments.size())) {
			throw new RuntimeException("Function mismatch " + e1.name + " != " + e2.name);
		}

		for(int i = 0; i < e1.arguments.size(); i++) {
			problems.add(new Equation(e1.arguments.get(i), e2.arguments.get(i)) );
		}
	}
	void matchVariable(Variable e1, Term e2) {
		e2.occurs(e1.name);

		for(int i = 0; i < problems.size(); i++) {
			problems.set(i, problems.get(i).substitute(e1.name, e2));
		}

		for(Map.Entry<String, Term> answer : solution.entrySet()) {
			answer.setValue(answer.getValue().substitute(e1.name, e2));
		}

		solution.put(e1.name, e2);
	}

	void solve() {
		while(!problems.isEmpty()) {
			Equation head = problems.remove(problems.size() - 1);
			System.out.println("Solving " + head);
			head.left.match(head.right, this);
		}
	}

	public static void main(String[] $) throws IOException {
		Parser parser = new Parser(System.in);
		Unify unifier = new Unify();
		unifier.problems = parser.equations();
		unifier.solution = new HashMap<>();
		unifier.solve();
		System.out.println(unifier.solution);
	}
}

Here's an example usage (use CTRL+D to stop input).

$ java Unify
f(x,a()) = f(y(), b)


Solving f(x,a())=f(y(),b)
Solving a()=b
Solving x=y()
{b=a(), x=y()}