Toying with Core.logic

Core.logic is a Clojure implementation of the miniKanren logic programming language.

In this kata you will practice simple logic programming problems through core.logic. With that said, this kata only features beginner level problems and aims to be a reasonable excuse for Clojure hobbyists to have a taste of logic programming; users with previous experiences with miniKanren or Prolog might find the problems trivial.

Learning Core.logic

Clojure features quite some complete introductions. Core.logic much less so. Here are some well-written resources that would get you started (and googling around would reveal more):

• https://github.com/swannodette/logic-tutorial
• A Core.logic Primer
• https://web.archive.org/web/20170822021646/http://objectcommando.com/blog/2011/11/04/the-magical-island-of-kanren-core-logic-intro-part-1/

Beyond the Most Basic

This kata will use some features of core.logic that is beyond what has been mentioned in some online tutorials. I will try to run a quick recap of basic core.logic and then introduce the features.

Setup

In this section, we assume that we are in a namespace with the setup below:

(ns logic-playground.core
  [:refer-clojure :exclude [==]]
  [:require
    [clojure.core.logic :refer :all]
    [clojure.core.logic.fd :as fd]])

Recap

Recall the unification operator ==, and the run variants:

(run 1 [q]
    (== q 3)) ;; (3)

Recall the conde operator:

(run* [q]
    (conde
        [(== q :banana)]
        [(== q :wire)]
        [fail]
        [succeed])) ;; (:banana :wire _0)

Recall that fresh creates new logic variables:

(run* [q]
    (fresh [p]
        (== p q)
        (== p 3))) ;; (3)

Recall that defn can be used to define new goals

(defn fake-firsto [l x]
    (== (first l) x))

(run* [q]
    (fresh [p]
        (fake-firsto [q 10 100] p))) ;; (_0)

Recall the following goals:

• conso
• resto
• membero
• distincto

core.logic.fd

The information in this section is all based on https://github.com/clojure/core.logic/wiki/Features

Arithmetic functions + - * are not by default defined for logic variables. Thankfully instead of using project or building our own natural number system, core.logic.fd defines the arithmetic operations for us.

(run* [q]
    (fresh [a b]
        (fd/in a b (fd/interval 1 100))
        (fd/* a b 30)
        (fd/<= a b)
        (== q [a b]))) ;; ([1 30] [2 15] [3 10] [5 6])

defne

defne is a macro extending defn, providing pattern-matching for logic goals.

A contrived example is that we are to define addition in the ℤ₂ ring, or equivalently the xor function.

(defne z2+ [a b c]
    ([0 0 0])
    ([0 1 1])
    ([1 1 0])
    ([1 0 1]))

The definition is just listing all the possibilities of a b c: 0 + 0 = 0, 0 + 1 = 1, 1 + 1 = 0, 1 + 0 = 1.

defne's strength becomes more obvious when matching on sequences.

For example, suppose we are to write a relation called (lasto l x) that succeeds when x is the last element of l.

A way to write this "from scratch" is to write it in the traditional functional programming way via pattern-matching:

(defne lasto
        [xs x]
        ([[x . ()] _])
        ([[_ . a] _]
            (lasto a x)))

The pattern [x . ()] matches cons lists in the form x :: nil, a one-element list that has only the element x (the same x in the arguments).

Unfortunately, this does not work as well as firsto in reality: (lasto v 1) can yield infinite many results (as opposed to one result in the case of the built-in firsto). For this kata, however, we wil only extract and test a finite amount of results, so this problem does not matter.

As the last example, here is a naive implementation of the fibonacci sequence:

(defne fib [input output]
    ([0 1])
    ([1 1])
    ([n r]
        (fresh [n1 n2 r1 r2]
            (fd/- n 1 n1)
            (fd/- n 2 n2)
            (fib n1 r1)
            (fib n2 r2)
            (fd/+ r1 r2 r))))

Goals

Implement the following goals

;; ntho, "coll" will only be vectors in the input
(ntho coll i ele) ;; (= ele (nth coll i))

;; reverseo, "a" and "b" will only be vectors in the input
(reverseo a b) ;; (= b (reverse a))

;; sets implemented as vectors, A must be a subset of B to succeed, both inputs only contain distinct elements
(subseto a b)

Note that the core.logic library used in this kata only contains the clojure.core.logic and clojure.core.logic.fd namespace. The others are not included.