# 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

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 ...

Top 50 recent answers are included