# What algorithms for unification over (multidimensional) array terms?

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.

• Could you give an example of what you mean by a multidimensional array term? Is it just a multidimensional array? Mar 5 '20 at 4:24
• @ShyPerson yes, just a multidimensional array. I would have thought that there would be special tweaks or extensions to traditional algorithms for those. Mar 7 '20 at 9:54

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