Quais algoritmos para unificação de termos de array (multidimensionais)?

Question

Estou procurando referências sobre a implementação da unificação em termos de matrizes multidimensionais.

Existem algoritmos de unificação especializados para esses casos?Não consegui encontrar literatura satisfatória sobre o assunto e estou tentando escrever uma biblioteca de programação lógica para a linguagem J.

Answer 1

A título de contexto, assumirei que o objetivo é fazer a unificação na lógica clássica de primeira ordem em uma linguagem fixa $\mathscr{L}$.(Formatação e outras correções são bem-vindas.)

Resumidamente, você pode tratar matrizes como termos e matrizes multidimensionais como matrizes de matrizes.Você também apresentará um novo termo símbolo que não ocorre em $\mathscr{L}$.

Por exemplo, se você tiver um array multidimensional como o seguinte,

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

você primeiro irá convertê-lo em uma matriz de matrizes,

$$ exto{((1 2 3) (x y z))}$$

e depois converta-o em termos.Assumindo o termo símbolo a não estiver no seu idioma, agora você pode representar seu array multidimensional da seguinte maneira:

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