I am looking for references on implementing unification over multidimensional array terms.
Are there specialized unification algorithms for those cases? I wasn't able to find satisfactory literature on the topic, and I am attempting to write a logic programming library for the J language.
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 have a multidimensional array like the following,
\begin{pmatrix} 1 & 2 & 3\\ x & y & z \end{pmatrix}
you'll first convert it to an array of arrays,
$$\text{((1 2 3) (x y z))}$$
and then convert it to terms. Assuming the term symbol a is not in your language, you can now represent your multidimensional array as follows:
a(a(1,2,3),a(x,y,z))
