miniKanren

miniKanren es una familia de lenguajes de programación para programación lógica. Minikaren está disponible como DSL en muchos lenguajes: Scheme, Haskell, Clojure (llamado core.logic), Python, C#, Elixir, Go, JavaScript, Rust, ... y prácticamente cualquier lenguaje de programación que no soporta el paradigma de la programación lógica.

Historia

MiniKanren surgió originalmente en el libro The Reasoned Schemer, escrito por Daniel P. Friedman, William E. Byrd, Oleg Kiselyov, and Jason Hemann y publicado por MIT Press siendo la última edición la de 2018.

Paradigma lógico Con Minikanren es posible añadir el paradigma lógico a cualquier lenguaje de programación añadiendo únicamente 3 funciones. Este conjunto de 3 funciones se denomina microKanren y normalmente las implementaciones de miniKanren implementan microKanren en el lenguaje de destino y el resto de miniKanren se implementa usando las funciones definidas en microKanren. Así miniKanren es una familia de lenguajes que no comparten sintaxis (la sintaxis depende del lenguaje de destino) aunque generalmente es muy parecida.

Las funciones de microKanren son las siguientes:

==
- Realiza la operación de unificación, que ya comenté en la ihttps://blog.adrianistan.eu/introduccion-a-prolog-tutorial-en-espanolntroducción a Prolog y básica en programación lógica
fresh
- Introduce un nuevo scope, definiendo variables lógicas. A su vez, realiza la conjunción de las relaciones que se definen.
conde
- Introduce la posibilidad de múltiples respuestas, definiendo varios conjuntos independientes donde todas los predicados tienen que ser ciertos a la vez. Esto es una mezcla de AND y OR a la vez. Veremos un ejemplo más abajo.

Como las relaciones son bidireccionales, si a miniKanren se le da una expresión y una salida deseada, miniKanren puede ejecutar la expresión "hacia atrás", encontrando todas las entradas posibles a la expresión que producen la salida deseada. Este comportamiento bidireccional permite al usuario restringir tanto la entrada al programa como el resultado del programa simultáneamente. miniKanren realiza una búsqueda intercalada que eventualmente encontrará cualquier solución que exista, incluso si alguna rama del árbol de búsqueda es infinitamente larga y no contiene soluciones. Si no existe una solución, miniKanren puede buscar para siempre si el árbol de búsqueda es infinito.

Un ejemplo de código miniKanren es evalo, un objetivo relacional que relaciona las expresiones con los valores que evalúan. Cuando se llama evalo en miniKanren así: (evalo qq), generará quines, es decir, expresiones q que al ejecutarse se evaluarán a sí mismas.^[1]

El libro The Reasoned Schemer utiliza miniKanren para demostrar la programación relacional y proporciona una implementación completa en Scheme .^[2] El núcleo del lenguaje cabe en dos páginas impresas. La implementación del Esquema de miniKanren está diseñada para ser fácilmente comprensible, modificada y ampliada.

αleanTAP es un programa escrito en αKanren, una extensión de miniKanren para lógica nominal . Dado un teorema, puede encontrar una prueba, lo que lo convierte en un probador de teoremas . Dada una prueba, puede encontrar el teorema, lo que lo convierte en un comprobador de teoremas. Dada parte de una prueba y parte de un teorema, completará las partes faltantes de la prueba y el teorema, convirtiéndolo en un explorador de teoremas.^[3]

Hay implementaciones de miniKanren en Haskell, Racket, Ruby, Clojure, JavaScript, Scala, Swift, Dart y Python . La implementación canónica es un lenguaje incrustado en Scheme . La biblioteca Clojure core.logic se inspiró en miniKanren.

El nombre kanren proviene de una palabra japonesa (関連) que significa "relación".

Véase también

Referencias

↑ Will Byrd, Eric Holk, and Dan Friedman (2012). «miniKanren, live and untagged: Quine generation via relational interpreters (programming pearl)». Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming (ACM): 8-29.
↑ Dan Friedman; Will Byrd; Oleg Kiselyov (2005). The Reasoned Schemer. MIT Press. ISBN 9780262562140.
↑ (Tesis) https://scholarworks.iu.edu/dspace/bitstream/handle/2022/8777/Byrd_indiana_0093A_10344.pdf. Falta el |título= (ayuda)

Enlaces externos

[1] Will Byrd, Eric Holk, and Dan Friedman (2012). «miniKanren, live and untagged: Quine generation via relational interpreters (programming pearl)». Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming (ACM): 8-29.

[2] Dan Friedman; Will Byrd; Oleg Kiselyov (2005). The Reasoned Schemer. MIT Press. ISBN 9780262562140.

[dis-3] (Tesis) https://scholarworks.iu.edu/dspace/bitstream/handle/2022/8777/Byrd_indiana_0093A_10344.pdf. Falta el |título= (ayuda)

[1]

[2]

[3]