miniKanren es un DSL (Domain Specific Language) para la programación logica.
miniKanren es muy simple, con sólo tres operadores lógicos y un operador de interfaz.
La primera implementación fue en scheme, pero ahora existen implementaciones en diferentes lenguajes y tecnologías como Racket, Clojure, Haskell, Python, JavaScript, Scala, Ruby, OCaml, PHP y algunos más.
De igual manera que prolog, esta centrado en reglas y constraits.
En este post vamos a utilizar la implementación de Clojure, MiniKanren se encuentra en core.logic, para poder usarlo debemos tener una jdk y Leiningen.
Para crear un proyecto debemos utilizar Leiningen de la siguiente manera:
lein new logical
Con esta instrucción podemos crear un proyecto.
Ahora debemos agregar las dependencias:
(defproject logical "0.1.0-SNAPSHOT"
:dependencies [[org.clojure/clojure "1.5.1"]
[org.clojure/core.logic "0.8.5"]])
core.logic es donde se encuentra MiniKanren.
Ahora cuando lancemos el relp se levantará miniKanren:
$ lein repl
nREPL server started on port 48235 on host 127.0.0.1
REPL-y 0.3.0
Clojure 1.5.1
Docs: (doc function-name-here)
(find-doc "part-of-name-here")
Source: (source function-name-here)
Javadoc: (javadoc java-object-or-class-here)
Exit: Control+D or (exit) or (quit)
Results: Stored in vars *1, *2, *3, an exception in *e
user=> (use 'clojure.core.logic)
WARNING: == already refers to: #'clojure.core/== in namespace: user, being
replaced by: #'clojure.core.logic/==
nil
user=>
Ahora podemos empezar con el relp de MiniKanren, veamos un ejemplo :
user=> (run* [q] (== q 1))
(1)
En el ejemplo corremos el programa con run* que permite correr programas logicos y retorna un conjunto de soluciones. q es una variable logica. Y el programa contiene la siguiente expresión :
(== q 1)
Dicha expresión es unification, que se puede ver como pattern matching. Este programa devuelve 1 dado que q va valer 1 para que esto sea verdadero.
Le está pidiendo al lenguaje que intente hacer que los lados izquierdo y derecho sean iguales, suponiendo que eso sea posible. Los lados izquierdo y derecho se comparan como en las pruebas de igualdad normales, y cualquier variable lógica no vinculada está vinculada a valores que harían coincidir los dos lados. En este ejemplo, q está vinculado a 1, que es una solución porque no hay otras reglas.
Las expresiones en un programa lógico son objetivos. No devuelven verdadero o falso, pero tienen éxito o fracasan. Es posible que el éxito se logre varias veces de diferentes maneras o en absoluto. Esto nos lleva al último bit de nuestro ejemplo: el resultado.
Nuestro ejemplo devuelto (1). run * devuelve los valores de q que resultan en éxito.
En nuestro ejemplo, unificar q con 1 une q al número 1 y tiene éxito. Nuestro resultado es la lista que contiene el enlace único para q.
Veamos un objetivo fallido:
user=> (run* [q] (== q 1) (== q 2))
()
Este programa tiene dos expresiones, cada una un objetivo. Un programa con múltiples objetivos tendrá éxito solo si todos los objetivos tienen éxito, de manera similar a && u operadores en otros lenguajes. Aquí, la primera unificación unirá q al número 1 como antes y tendrá éxito. La segunda unificación fallará, ya que q está unido a 1 y 1 no se unifica con 2. Debido a que ningún enlace de q puede hacer que ambos objetivos tengan éxito, la lista resultante está vacía. Es decir, no hay solución.
En proximos post seguiremos con este particular lenguaje, por ahora dejo link: http://minikanren.org/
