It's time to unify!
code-golf logic math
Introduction
Wouldn't it be awesome if they whole world would be united and there would be no conflicts and disputes? Now while you can't unify nations, you certainly can unify expressions to resolve their unknown relation and conflicts.
Your mission is simple: Unify the world (of expressions)!
And of course, because you're lazy you want to do this with the least effort (read: code-length) possible.
Specification
Input
Your input will be a unification problem. You can format it however you want and need, as long as you don't encode additional information to what is given in the standard / example format. Encoding the number of arguments per function into the input is allowed but not mandatory, you can also just derive this from the input.
Example format:
Your first input will be list of function symbols, which is represented as a list of pairs of strings and non-negative integers.
Your second input will be a list of equalities (you may represent each as a string), which represent the unification problem. They will be represented as a list of strings as well. Anything which is not a parenthesis or an equality sign can be considered a variable. If the number of arguments is 0, parenthesis are omitted.
Example input:
[("f",1),("g",2),("h",3),("a",0)], [x=f((g(a,y)),y=h(g(f(a),z),f(z),a)]
Output
The output is either some falsy value or something representing a list of equalities. It is allowed to use the empty list to indicate a falsy value.
What to do?
You need to unify the inputs you got. In the end there must only be variables on the left side of the equality-signs if the you didn't encounter an error. If you did you need to report it (-> false or empty list).
To do the unification, you can - but don't have to - use Martelli and Montanari's algorithm, which goes as follows:
E is always the (complete) set of equalities except the current one
x,y,z are variables, f,g,h are functions, t1,t2, ...,tn,s1,...,sn are arbitrary terms (compositions of functions and variables)
{x=x} E => E, e.g. if you encounter two equivalent variables, discard
{f(t1,...,tn)=f(s1,...,sn)} E => {t1=s1,t2=s2,...,tn=sn} E, e.g. if you encounter the same function on both sides, unify the arguments along with your rest
{f(t1,...,tn}=g(s1,...,sn)} E => Error, if the symbols are different, you can't succeed
{x=f(t1,...,tn)} E => {x=f(t1,...,tn)} E[x -> f(t1,...,tn)], e.g. if you see a variable equals a term, replace the variable with this term in all other expressions
{x=f(t1,...,tn)} E => Error, e.g. if any of the t1,..,tn contain x at some point
{f(t1,...,tn)=x} E => {x=f(t1,...,tn)} E, e.g. if you see a variable "naked" on the right side, swap the sides
Two step-by-step examples are provided below additionally to the test cases.
Corner Cases
You can get an empty list of function symbols, this means you have exclusively variables in the second input.
The input list of equalities will never be empty, your code does not need to handle this case.
Who wins?
This is code-golf so the shortest answer in bytes wins!
Standard rules apply of course.
Test-cases
All these test cases use the functions [("a",0),("b",0),("f",1),("g",1),("h",2)]
[x=b] -> [x=b]
[a=x] -> [x=a]
[a=b] -> []
[y=f(x)] -> [y=f(x)]
[x=f(x)] -> []
[f(x)=f(y)] -> [x=y]
[f(x)=g(y)] -> []
[h(x,y)=h(a,b)] -> [x=a,y=b]
[x=f(z),y=f(a),x=y] -> [x=f(a),y=f(a),z=a]
[h(x,f(y))=z,z=h(f(y),v)] -> [x=f(y),v=f(y),z=h(f(y),f(y))]
Step-By-Step Example
Example 1: Test Case 9
[x=f(z),y=f(a),x=y] => (replace x in third equation with first x)
[x=f(z),y=f(a),f(z)=y] => (replace y in third equation)
[x=f(z),y=f(a),f(z)=f(a)] => (remove f's in third equation)
[x=f(z),y=f(a),z=a] => (replace the z in the first expression)
[x=f(a),y=f(a),z=a]
Example 2:
Let [("f",2),("g",2),("a",0),("b",0)] be your functions
[f(g(a,x),g(y,b)=f(x,g(v,w)),f(x,g(v,w))=f(g(x,a),g(v,b))] => (remove f in second equation)
[f(g(a,x),g(y,b)=f(x,g(v,w)),x=g(x,a),g(v,w)=g(v,b))] => (function symbol missmatch in equation 2)
[]
