MiniKanren

Si hablamos de programación lógica siempre pensamos en Prolog. Pero existen otros lengujes lógicos, como  MiniKanren que es un lenguaje embebido en Clojure.

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/