Quels algorithmes pour l'unification des termes de tableaux (multidimensionnels) ?

Question

Je recherche des références sur la mise en œuvre de l'unification sur des termes de tableaux multidimensionnels.

Existe-t-il des algorithmes d'unification spécialisés pour ces cas ?Je n'ai pas pu trouver de littérature satisfaisante sur le sujet et j'essaie d'écrire une bibliothèque de programmation logique pour le langage J.

Answer 1

En guise de contexte, je suppose que l'objectif est de réaliser l'unification en logique classique du premier ordre dans un langage fixe. $\mathscr{L}$.(Le formatage et autres corrections sont les bienvenus.)

En bref, vous pouvez traiter les tableaux comme des termes et les tableaux multidimensionnels comme des tableaux de tableaux.Vous allez également introduire un nouveau symbole de terme qui n'apparaît pas dans $\mathscr{L}$.

Ainsi, par exemple, si vous disposez d'un tableau multidimensionnel comme celui-ci,

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

vous allez d'abord le convertir en un tableau de tableaux,

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

puis convertissez-le en termes.En supposant le terme symbole a n'est pas dans votre langue, vous pouvez maintenant représenter votre tableau multidimensionnel comme suit :

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