Quelles sont les principales différences techniques entre Prolog et miniKanren, en ce qui concerne la programmation logique?

Quand je veux lire sur la programmation logique, je me heurte toujours à deux manières “principales” de le faire aujourd’hui:

  • miniKanren , un minilanguage présenté dans The Reasoned Schemer et populaire en ce moment en raison de core.logic .
  • Prolog , le premier “grand” langage de programmation logique.

Ce qui m’intéresse maintenant: quelles sont les principales différences techniques entre les deux? Leur approche et leur mise en œuvre sont-elles très similaires, ou adoptent-elles des approches complètement différentes en matière de programmation logique? D’où viennent les mathématiques et quels sont les fondements théoriques?

Tout d’abord, permettez-moi de vous complimenter sur votre icône pw0n1e.

C’est une question délicate à répondre, en grande partie parce qu’il y a tellement de variantes de miniKanren et de Prolog. miniKanren et Prolog sont vraiment des familles de langages, ce qui rend difficile la comparaison de leurs fonctionnalités, voire de leur utilisation dans la pratique. Pour cette raison, veuillez prendre tout ce que je vais dire avec prudence: si je dis que Prolog utilise la recherche en profondeur, sachez que de nombreuses implémentations Prolog prennent en charge d’autres stratégies de recherche et que des stratégies de recherche alternatives peuvent également être codées. -interpreter niveau. Néanmoins, miniKanren et Prolog ont des philosophies de conception différentes et font des compromis différents.

Prolog est l’un des deux langages classiques pour la programmation de l’intelligence artificielle symbolique (l’autre langage classique étant Lisp). Prolog excelle dans la mise en œuvre de systèmes basés sur des règles symboliques dans lesquels les connaissances déclaratives sont codées dans une logique de premier ordre. Le langage est optimisé pour l’expressivité et l’efficacité pour ces types d’applications, parfois au désortingment de la pureté logique. Par exemple, par défaut, Prolog n’utilise pas la “vérification des occurrences” dans l’unification. Du sharepoint vue mathématique / logique, cette version d’unification est incorrecte. Toutefois, la vérification de l’occurrence est coûteuse et, dans la plupart des cas, l’absence de vérification de la présence n’est pas un problème. Il s’agit d’une décision de conception très pragmatique, tout comme l’utilisation par Prolog de la recherche en profondeur et de l’utilisation de cut ( ! ) Pour contrôler le retour en arrière. Je suis sûr que ces décisions étaient absolument nécessaires lors de l’exécution sur le matériel des années 1970, et aujourd’hui, elles sont très utiles lorsque vous travaillez sur de gros problèmes et lorsque vous traitez d’énormes espaces de recherche (souvent infinis!).

Prolog supporte de nombreuses fonctionnalités “extra-logiques” ou “non logiques”, y compris la coupe, l’ assert et le retract , la projection de variables pour l’arithmétique à l’aide de, et ainsi de suite. Beaucoup de ces fonctionnalités facilitent l’expression de stream de contrôle complexes et la manipulation de la firebase database globale de Prolog. Une caractéristique très intéressante de Prolog est que le code Prolog est lui-même stocké dans la firebase database globale des faits et peut être interrogé lors de l’exécution. Cela rend sortingvial d’écrire des méta-interpréteurs qui modifient le comportement du code Prolog sous interprétation. Par exemple, il est possible d’encoder la première recherche dans Prolog à l’aide d’un méta-interpréteur qui modifie l’ordre de recherche. C’est une technique extrêmement puissante qui n’est pas bien connue en dehors du monde Prolog. “The Art of Prolog” décrit cette technique en détail.

Des efforts considérables ont été déployés pour améliorer les implémentations de Prolog, dont la plupart sont basées sur la machine abstraite Warren (WAM). Le WAM utilise un modèle à effet secondaire dans lequel les valeurs sont affectées de manière destructive aux variables logiques, ces effets secondaires étant annulés lors du retour en arrière. De nombreuses fonctionnalités peuvent être ajoutées à Prolog en étendant les instructions du WAM. Un inconvénient de cette approche est que les documents d’implémentation Prolog peuvent être difficiles à lire sans une compréhension solide du WAM. D’autre part, les implémenteurs de Prolog ont un modèle commun pour discuter des problèmes d’implémentation. De nombreuses recherches ont été menées en parallèle sur Prolog, qui a culminé dans Andorra Prolog dans les années 1990. Au moins certaines de ces idées vivent dans Ciao Prolog. (Ciao Prolog regorge d’idées intéressantes, dont beaucoup vont bien au-delà du standard Prolog.)

Prolog possède une belle syntaxe de type “pattern-matching” basée sur l’unification qui se traduit par des programmes très succincts. Les prologistes aiment leur syntaxe, tout comme les Lispers aiment leurs expressions s. Prolog possède également une grande bibliothèque de prédicats standard. Grâce à toute l’ingénierie qui a permis de rendre le WAM rapide, il existe des implémentations Prolog très performantes. En conséquence, de nombreux systèmes basés sur les connaissances ont été entièrement écrits dans Prolog.

miniKanren a été conçu comme un langage de programmation logique minimaliste, avec une petite implémentation facile à comprendre et facilement piratable. miniKanren était à l’origine intégré à Scheme et a été porté sur des dizaines d’autres langues hôtes au cours de la dernière décennie. L’implémentation miniKanren la plus populaire est ‘core.logic’ dans Clojure, qui a maintenant de nombreuses extensions de type Prolog et un certain nombre d’optimisations. Récemment, le kernel de l’implémentation de miniKanren a été encore simplifié, ce qui a abouti à un minuscule “micro-kernel” appelé “microKanren”. miniKanren peut alors être implémenté sur ce microKanren. Le port de microKanren ou miniKanren dans un nouveau langage hôte est devenu un exercice standard pour les programmeurs qui apprennent miniKanren. Par conséquent, la plupart des langages de haut niveau les plus populaires ont au moins une implémentation miniKanren ou microKanren.

Les implémentations standard de miniKanren et microKanren ne contiennent aucune mutation ou autre effet secondaire, à une seule exception près: certaines versions de miniKanren utilisent l’égalité des pointeurs pour comparer les variables logiques. Je considère cela comme un “effet bénin”, bien que de nombreuses implémentations évitent même cet effet en passant un compteur à travers l’implémentation. Il n’y a pas non plus de firebase database globale. La philosophie d’implémentation de miniKanren s’inspire de la functional programming: la mutation et les effets doivent être évités et toutes les constructions de langage doivent respecter la scope lexicale. Si vous examinez attentivement la mise en œuvre, vous pourriez même repérer quelques monades. L’implémentation de la recherche est basée sur la combinaison et la manipulation de stream paresseux, une fois de plus sans utiliser de mutation. Ces choix d’implémentation conduisent à des compromis très différents que dans Prolog. Dans Prolog, la recherche de variable est un temps constant, mais le retour en arrière nécessite de réduire les effets secondaires. Dans miniKanren, la recherche de variables est plus coûteuse, mais le retour en arrière est “gratuit”. En fait, il n’y a pas de retour en arrière dans miniKanren, en raison de la manière dont les stream sont gérés.

Un aspect intéressant de la mise en œuvre de miniKanren est que le code est insortingnsèquement sûr pour les threads et, au moins en théorie, sortingvialement parallélisable. Bien sûr, la parallélisation du code sans le ralentir n’est pas une mince affaire, étant donné que chaque thread ou processus doit avoir suffisamment de travail pour compenser la surcharge de la parallélisation. Cependant, il s’agit d’un domaine de la mise en œuvre de miniKanren qui, je l’espère, recevra plus d’attention et d’expérimentation.

miniKanren utilise la vérification des occurrences pour l’unification et utilise une recherche d’entrelacement complète au lieu d’une recherche en profondeur. La recherche par entrelacement utilise plus de mémoire que la recherche par la profondeur en premier, mais peut trouver des réponses dans certains cas où la recherche en profondeur doit diverger / boucler pour toujours. miniKanren supporte quelques opérateurs extra-logiques, par exemple conda , conda et project . conda et conda peuvent être utilisés pour simuler la coupe de Prolog, et le project peut être utilisé pour obtenir la valeur associée à une variable logique.

La présence de conda , conda et project — et la possibilité de modifier facilement la stratégie de recherche — permet aux programmeurs d’utiliser miniKanren comme un langage intégré de type Prolog. Cela est particulièrement vrai pour les utilisateurs de «core.logic» de Clojure, qui inclut de nombreuses extensions de type Prolog. Cette utilisation “pragmatique” de miniKanren semble représenter la majorité de l’utilisation de miniKanren dans l’indussortinge. Les programmeurs qui souhaitent append un système de raisonnement basé sur la connaissance à une application existante écrite en Clojure ou Python ou JavaScript ne sont généralement pas intéressés par la réécriture de toute leur application dans Prolog. Intégrer un petit langage de programmation logique dans Clojure ou Python est beaucoup plus attrayant. Une implémentation Prolog intégrée fonctionnerait tout aussi bien à cette fin, sans doute. Je soupçonne que miniKanren est devenu populaire en tant que langage logique intégré en raison de l’implémentation minimale et pure du kernel, ainsi que des conférences, des articles de blog, des didacticiels et d’autres matériels éducatifs publiés depuis la publication de The Reasoned Schemer.

En plus de l’utilisation de miniKanren comme langage de programmation logique intégré pragmatique similaire à Prolog, miniKanren est utilisé pour la recherche en programmation “relationnelle”. C’est-à-dire dans les programmes d’écriture qui se comportent comme des relations mathématiques plutôt que des fonctions mathématiques. Par exemple, dans Scheme, la fonction append peut append deux listes, renvoyant une nouvelle liste: l’appel de la fonction (append '(abc) '(de)) renvoie la liste (abcde) . On peut cependant aussi traiter append comme une relation à trois plutôt que comme une fonction à deux arguments. L’appel (appendo '(abc) '(de) Z) associerait alors la variable logique Z à la liste (abcde) . Bien sûr, les choses deviennent plus intéressantes lorsque nous plaçons des variables logiques dans d’autres positions. L’appel (appendo X '(de) '(abcde)) associe X à (abc) , tandis que l’appel (appendo XY '(abcde)) associe X et Y à des paires de listes qui, ajoutées, sont égales à (abcde) . Par exemple, X = (ab) et Y = (cde) font partie de ces paires de valeurs. Nous pouvons également écrire (appendo XYZ) , ce qui produira une infinité de sortingplets de listes X , Y et Z sorte que l’ajout de X à Y produira Z

Cette version relationnelle de append peut être facilement exprimée dans Prolog, et est en effet affichée dans de nombreux didacticiels Prolog. En pratique, les programmes Prolog plus complexes ont tendance à utiliser au moins quelques fonctions extra-logiques, telles que la coupe, qui empêchent de traiter le programme résultant comme une relation. En revanche, miniKanren est explicitement conçu pour prendre en charge ce style de programmation relationnelle. Les versions plus récentes de miniKanren prennent en charge la résolution de contraintes symboliques ( numbero , absento , absento, contraintes de déséquilibre, programmation logique nominale) pour faciliter l’écriture de programmes non sortingviaux en tant que relations. En pratique, je n’utilise jamais les fonctionnalités extra-logiques de miniKanren et j’écris tous mes programmes miniKanren en tant que relations. Les programmes relationnels les plus intéressants sont les interpréteurs relationnels pour un sous-ensemble de Scheme. Ces interprètes ont de nombreuses capacités intéressantes, telles que la génération d’un million de programmes Scheme qui correspondent à la liste (I love you) , ou la génération sortingviale de quines (programmes qui se évaluent).

miniKanren fait un certain nombre de compromis pour permettre ce style de programmation relationnel, qui est très différent des compromis de Prolog. Au fil du temps, miniKanren a ajouté plus de contraintes symboliques, devenant vraiment un langage de programmation logique par contraintes orienté symboliquement. Dans de nombreux cas, ces contraintes symboliques permettent d’éviter d’utiliser des opérateurs extra-logiques tels que condu et project . Dans d’autres cas, ces contraintes symboliques ne sont pas suffisantes. Un meilleur support pour les contraintes symboliques est un domaine actif de la recherche miniKanren, avec la question plus large de savoir comment écrire des programmes plus grands et plus complexes en tant que relations.

En bref, miniKanren et Prolog ont des fonctionnalités, des implémentations et des utilisations intéressantes, et je pense que cela vaut la peine d’apprendre les idées des deux langages. Il existe également d’autres langages de programmation logiques très intéressants, tels que Mercury, Curry et Gödel, qui ont chacun leur propre programmation logique.

Je terminerai avec quelques ressources miniKanren:

Le principal site web de miniKanren: http://minikanren.org/

Une interview que j’ai donnée sur la programmation relationnelle et miniKanren, y compris une comparaison avec Prolog: http://www.infoq.com/interviews/byrd-relational-programming-minikanren

À votre santé,

–Volonté

Réponse provisoire:

AFAIK, “The Reasoned Schemer” a introduit la programmation logique de base dans une syntaxe Scheme-y et un style de functional programming, en ajoutant notamment les objectives constants “#u” (fail) et “#s” (suceeed) aux valeurs booléennes “#t “et” #f “. Il utilisait la même approche de la programmation logique que Prolog: la recherche d’unification et de retour en arrière. Je verrai si j’ai le temps de récupérer ce livre de mon étagère pendant le week-end. La twig des mathématiques est une logique de premier ordre sous forme restreinte, en l’occurrence des clauses de type Horn, et l’effacement de résolution. Voir: Logique computationnelle: souvenirs du passé et défis pour l’avenir par John Alan Robinson et Les premières années de la programmation logique par Robert Kowalski pour un démarrage à froid.