# Tag Info

2

Here $f$ is not a mathematical function. Rather, it is a function symbol. Don't think of $f(a,b)$ as the result of evaluating the function at parameters $a,b$. Rather, think of it as a term in a symbolic expression -- it is a syntactic object that is not intended to be interpreted in the way you are interpreting it. If you like, you can think of it as ...

2

Because that's not how substitution is defined. Seriously, there isn't much more to it than that. In some situations (such as applying a single step of a collection of rewriting rules), having the ability to substitute "each variable once, all at once" like this is important for the correctness of the definition. So substitution is defined so that there is ...

1

Say you tried to solve $f(A, g(A)) = f(B, B)$ after applying $A \to B$ you'd then have $f(A, g(A)) = f(A, A)$ and you'd have to unify $A = g(A)$ as a sub problem.

1

By way of context, I'll assume the goal is to do unification in classical first-order logic in a fixed language $\mathscr{L}$. (Formatting and other corrections welcome.) Briefly, you can treat arrays as terms and multidimensional arrays as arrays of arrays. You'll also introduce a new term symbol that doesn't occur in $\mathscr{L}$. So for example, if you ...

1

I'm fairly sure this is possible. This seems to me as a special case of set constraints over tree languages: we can view regular expressions as a restriction of regular tree languages where each node has 0 or 1 children. These can handle union, concatenation, and recursion (star), and you can solve for variables like you describe. They're decidable, even ...

Only top voted, non community-wiki answers of a minimum length are eligible