統一のためのどのアルゴリズム（多次元）アレイ用語は？

Question

多次元配列用語に対する統一の実装に関する参照を探しています。

これらのケースに特殊な統一アルゴリズムはありますか？私はトピックで満足のいく文献を見つけることができませんでした、そして私はJ言語のための論理プログラミングライブラリを書いています。

Answer 1

コンテキストとして、目標は、固定言語 $ \ mathscr {l} $ で、古典的な一次ロジックで統一をすることです。（フォーマットやその他の修正歓迎）

簡単に言うと、配列の配列として用語と多次元配列として配列を扱うことができます。 $ \ mathscr {l} $ には発生しない新しい用語記号も紹介します。

たとえば、次のような多次元配列がある場合は、

\ begin {pmatrix} 1＆2＆3 \\ X＆y＆Z \ end {PMatrix}

最初にそれを配列の配列に変換します、

$$ \ text {（（1 2 3）（x y z））} $$

でそれを用語に変換します。シンボルaという用語が言語ではないと仮定すると、次のように多次元配列を表すことができます。

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

.