Welche Algorithmen zur Vereinheitlichung über (mehrdimensionale) Array-Terme?

Question

Ich suche nach Referenzen zur Implementierung der Vereinheitlichung über mehrdimensionale Array-Begriffe.

Gibt es spezielle Vereinheitlichungsalgorithmen für diese Fälle?Ich konnte keine zufriedenstellende Literatur zu diesem Thema finden und versuche, eine Logikprogrammierbibliothek für die Sprache J zu schreiben.

Answer 1

Im Kontext gehe ich davon aus, dass das Ziel darin besteht, die Vereinheitlichung in der klassischen Logik erster Ordnung in einer festen Sprache durchzuführen $\mathscr{L}$.(Formatierung und andere Korrekturen sind willkommen.)

Kurz gesagt, Sie können Arrays als Begriffe und mehrdimensionale Arrays als Arrays von Arrays behandeln.Sie werden auch ein neues Begriffssymbol einführen, das in nicht vorkommt $\mathscr{L}$.

Wenn Sie beispielsweise ein mehrdimensionales Array wie das folgende haben,

\begin{pmatrix} 1 & 2 & 3\\ x & y & z \end{pmatrix}

Sie konvertieren es zuerst in ein Array von Arrays,

$$ ext{((1 2 3) (x und z))}$$

und wandle es dann in Begriffe um.Unter der Annahme des Begriffs Symbol a ist nicht in Ihrer Sprache, können Sie Ihr mehrdimensionales Array jetzt wie folgt darstellen:

    a(a(1,2,3),a(x,y,z))