Unification d'ordre supérieur

Question

Je travaille sur un vérificateur de théorèmes d'ordre supérieur, dont l'unification semble être le sous-problème le plus difficile.

Si l'algorithme de Huet est toujours considéré comme l'état de l'art, quelqu'un a-t-il des liens vers des explications de cet algorithme écrites pour être comprises par un programmeur plutôt que par un mathématicien ?

Ou même des exemples où il fonctionne et où l'algorithme habituel du premier ordre ne fonctionne pas ?

Answer 1

État de l'art - oui, pour autant que je sache, tous les algorithmes ont plus ou moins la même forme que celui de Huet (je suis la théorie de la programmation logique, bien que mon expertise soit tangentielle). fourni par vous avez besoin d'une correspondance d'ordre supérieur complète : les sous-problèmes tels que la correspondance d'ordre supérieur (unification où un terme est fermé), et le calcul des motifs de Dale Miller, sont décidables.

Notez que l'algorithme de Huet est le meilleur dans le sens suivant : c'est comme un algorithme de semi-décision, en ce sens qu'il trouvera les unificateurs s'ils existent, mais il n'est pas garanti qu'il se termine s'ils n'existent pas. Puisque nous savons que l'unification d'ordre supérieur (en fait, l'unification de second ordre) est indécidable, vous ne pouvez pas faire mieux que cela.

Explications : Les quatre premiers chapitres de la thèse de doctorat de Conal Elliott, Extensions et applications de l'unification d'ordre supérieur devrait faire l'affaire. Cette partie pèse près de 80 pages, avec une théorie de type dense, mais elle est bien motivée, et c'est le compte rendu le plus lisible que j'ai vu.

Exemples : L'algorithme de Huet trouvera la marchandise pour cet exemple : [X(o), Y(succ(0))] ; ce qui rendra nécessairement perplexe un algorithme d'unification du premier ordre.

Answer 2

Voici un exemple d'unification d'ordre supérieur (en réalité une correspondance de second ordre) : f 3 == 3 + 3 , donde == est modulo alpha, beta, et eta-conversion (mais sans attribuer de signification à "+"). Il existe quatre solutions :

\ x -> x + x
\ x -> x + 3
\ x -> 3 + x
\ x -> 3 + 3

En revanche, l'unification/la correspondance de premier ordre ne donnerait aucune solution.

HOU est très pratique lorsqu'il est utilisé avec HOAS (higher-order abstract syntax), pour encoder des langages avec liaison de variables tout en évitant la complexité de la capture de variables, etc.

Ma première exposition au sujet a été l'article "Proving and Applying Program Transformations Expressed with Second Order Patterns" de Gerard Huet et Bernard Lang. Si je me souviens bien, cet article était "écrit pour être compris par un programmeur". Et une fois que vous avez compris la correspondance du second ordre, HOU n'a plus grand chose à faire. Un résultat clé de Huet est que le cas flexible/flexible (variables en tête d'un terme, et le seul cas n'apparaissant pas dans l'appariement) est toujours soluble.

Answer 3

J'ajouterais à la liste de lecture un chapitre du volume 2 de le Handbook of Automated Reasoning. Ce chapitre est probablement plus accessible au débutant et se termine par -calcul où commence l'article de l'article de Conal Elliott commence.

Un préprint est disponible ici :

Unification et correspondance d'ordre supérieur
Gilles Dowek, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps

L'article de Conal Elliott est plus formel et se concentre sur une variante, et introduit aussi un -calcul à la fin, qui a aussi des types de somme en plus des types de produits.

Au revoir

Answer 4

Il y a aussi l'article de Tobias Nipkow de 1993. Unification fonctionnelle des modèles d'ordre supérieur (seulement 11 pages, dont 4 sont une bibliographie et une annexe de codes). Le résumé :

Le développement complet d'un algorithme d'unification pour ce que l'on appelle les modèles d'ordre supérieur , une sous-classe de \lambda $-termes, est présenté. Le point de départ est une formulation d'unification par transformation, le résultat étant un programme fonctionnel directement exécutable. Dans une dernière étape de développement, le résultat est adapté aux $-termes. \lambda Termes en $ dans la notation de de Bruijn. Les algorithmes fonctionnent à la fois pour les termes simplement typés et non typés.