miniKanren -

Relational (Logic) programming

Yiyi Wang

What is miniKanren?

http://minikanren.org/

miniKanren is an embeded Domain Specific Language for logic programming.

It was originally written in Scheme, and has been ported to dozens of other host languages over the past decade..

The core miniKanren language is very simple, with only three logical operators (eq, and, or) and one interface operator run.

logic.js

  is a JavaScript implementation of a modified version of miniKanren.

Brief introduction to

ECMAScript 6 (ES6)

Why JavaScript - Pros

• easy syntax

• higher order function

• independent from any big company

• the only native web browser language

• big community

• lots of tools, libraries, and framworks

Variables

var x  // x = undefined
var y = "Hello JS"

Function

function add(x, y) {
  return x + y
}
 
// or
 
var add = function(x, y) {
  return x + y
}

Data types

• primitive

  • String

  • Number

  • Boolean

  • Undefined

  • Null

• non-primitive

  • Array

  • Object

  • RegExp

String

var x = "a"
var y = 'a'
x === y // true

Array

var x = [1, 2]
console.log(x.length) // 2
x.push(3) // x = [1, 2, 3]

Object

var x = {a: 1}
console.log(x.a)     // 1  
console.log(x['a'])  // 1
x.b = 2              // {a: 1, b: 2}
x.a = 3              // {a: 3, b: 2}

Why use ES6

(the newest version of JavaScript)

var foo = 'OUT'
 
if (true) {
  var foo = 'IN'
}
 
console.log(foo) // IN

let - A new Hope Scope

let foo = 'OUT'
 
if (true) {
  let foo = 'IN'
}
 
console.log(foo) // OUT

const

const x = 1
x = 2 // cause error.

Arrow function

function(x, y) {
  return x + y
}
 
(x, y) => {
  return x + y
}
 
(x, y) => x + y

Default Parameters

function add(x=1, y=2) {
  return x + y
}
 
var add = (x=1, y=2)=> x + y
 
add()  // 3
add(3) // 5
add(undefined, 3) // 4

Rest Parameters

function add(first, second, ...rest) {
  console.log('first: ', first)
  console.log('second: ', second)
  console.log('rest: ', rest)
}
add(1, 2, 3, 4, 5)
// first: 1
// second: 2
// rest: [3, 4, 5]

Generator

function* genThree() {
  yield 1
  yield 2
  console.log('Hello World')
  yield 3
}
let three = genThree()
three.next()  
// Object { value: 1, done: false }
three.next()  
// Object { value: 2, done: false }
three.next()  
// Hello World
// Object { value: 3, done: false }
three.next()
// Object { value: undefined, done: true }

function* anotherGenerator(i) {
  yield i + 1;
  yield i + 2;
  yield i + 3;
}
 
function* generator(i) {
  yield i;
  yield* anotherGenerator(i);
  yield i + 10;
}
 
var gen = generator(10);
 
console.log(gen.next().value); // 10
console.log(gen.next().value); // 11
console.log(gen.next().value); // 12
console.log(gen.next().value); // 13
console.log(gen.next().value); // 20

$\longrightarrow$ miniKanren in JavaScript.

miniKanren in JavaScript

The logic.js library

Logic variables

Either x is the beginning of the list ["banana", "orange", "apple"],
or x is the number 1.

Either x is the beginning of the list ["banana", "orange", "apple"],
or x is the number 1.

(The two values of x that make this expression true are 1 and banana)

Define logic variables

const q = lvar('q') // {id: "q"}
const x = lvar()    // {id: "~.0"}
const y = lvar()    // {id: "~.1"}

Substitution & Walking

ImmutableMap

const x = new ImmutableMap() // x => {}
const y = x.set('a', 12)     // x => {}, y => {a: 12}
console.log( x === y )       // false
x.get('a')                   // undefined
y.get('a')                   // 12

Given the expression:

Either x is the beginning of the list ["banana", "orange", "apple"],
or x is the number 1.

{x: "banana"} is a substitution map that makes this expression true

Either x is the beginning of the list [y, "orange", "apple"],
or y is the number 1.

One substitution map which makes this expression true is:
{x: y, y: 1}

Looking up values

function walk(key, sMap) {
  if (isLVar(key)) {
    const val = sMap.get(key)
    if (val === undefined) return key // not found
    return walk(val, sMap) // continue
  } else {
    return key
  }
}
 
walk(x, {})           // => x
walk(x, {x: y, y: 3}) // => 3

Unification

// unify(u, v, sMap)
unify(x, "banana", {}) // ==> {x: "banana"}
unify("banana", x, {}) // ==> {x: "banana"}

unify(x, "banana", {x: "banana"}) // {x: "banana"}
 
unify(x, "banana", {x: "mango"})  // null
// failed to unify two terms

function unify(x, y, sMap) {
  x = walk(x, sMap)
  y = walk(y, sMap)
  if (x === y) {
    return sMap
  } else if (isLVar(x)) {
    return sMap.set(x, y)
  } else if (isLVar(y)) {
    return sMap.set(y, x)
  } else { // failed to unify
    return null
  }
}
 
unify(x, 12, {})    // => {x: 12}
unify(x, y, {})     // => {x: y}
unify(x, 1, {x: 2}) // => null
unify(x, m, {x: 3, m: n}) // => {x: 3, m: n, n: 3}

Core miniKanren

eq

eq(x, 1)
 
eq(x, y)

eq

function eq(x, y) {
  return function*(sMap) {
    yield unify(x, y, sMap) // unify x and y
  }
}

fresh (scheme version)

fresh, which syntactically looks like lambda, introduces lexically-scoped Scheme variables that are bound to new logic variables; fresh also performs conjunction of the relations within its body. Thus

(fresh (x y z) (== x z) (== 3 y)) 

fresh in JavaScript?

in Scheme

(fresh (x y z) (== x z) (== 3 y)) 

in JavaScript ES6

(x=lvar(), y=lvar(), z=lvar())=> and(
  eq(x, z),
  eq(3, y))

and, or

const x = lvar('x'),
      y = lvar('y')
 
or(eq(x, 1), eq(x, 2))
 
and(eq(x, y), eq(y, 1))
 
or(
  eq(x, 1),
  (x=lvar())=> eq(x, 2))

function or(...clauses) {
  return function*(sMap) {
    const helper = function(offset, sMap) {
      const gen = clause(sMap) // clause is a goal(generator)
      while (true) {
        const res = gen.next(),
              sMap = res.value
        if (res.done) break
        if (sMap) yield sMap
      }
      yield* helper(offset + 1, sMap)
    }
    yield* helper(0, sMap)
  }
}

function and(...clauses) {
  return function*(sMap) {
    const helper = function(offset, sMap) {
      const clause = clauses[offset] // clause is a goal(generator)
      const gen = clause(sMap)
      while (true) {
        const res = gen.next()
        if (res.done) break
        const sMap = res.value
        if (sMap) {
          if (offset === clauses.length - 1)
            yield sMap
          else
            yield* helper(offset+1, sMap)
        } else { // failed to unify
          yield null
        }
      }
    }
    yield* helper(0, sMap)
  }
}

Define facts and rules

In prolog

parent(amy,bob).      % amy is the parent of bob. 
parent(bob,marco).
parent(bob,mike).
grandparent(X,Z) :- parent(X,Y) , parent(Y,Z).

in prolog

parent(amy,bob).      % amy is the parent of bob. 
parent(bob,marco).
parent(bob,mike).
grandparent(X,Z) :- parent(X,Y) , parent(Y,Z).

in logic.js (miniKanren)

function parent(x, y) {
  return or(
    and(eq(x, 'amy'), eq(y, 'bob')),
    and(eq(x, 'bob'), eq(y, 'marco')),
    and(eq(x, 'bob'), eq(y, 'mike'))
  )
}
function grandparent(x, z) {
  const y = lvar()
  return and(parent(x, y), parent(y, z))
}

Solve a Goal (Expression)

run(1, [x], eq(x, 1))
// [{x: 1}]
 
run([x], grandparent(x, 'mike'))
// [{x: 'amy'}]
run([x, y], grandparent(x, y))
// [{x: 'amy', y: 'marco'}, {x: 'amy', y: 'mike'}]
 
run(1, [x], and(
  eq(x, y),
  or(eq(x, 1), eq(x, 2), eq(x, 3)),
  eq(y, 2)))
// [{x: 2}]

run(1, [x], and(
  eq(x, y),
  or(eq(x, 1), eq(x, 2), eq(x, 3)),
  eq(y, 2)))

run(1, [x], ...)

Recall eq function

function eq(x, y) {
  return function*(sMap) {
    yield unify(x, y, sMap) // unify x and y
  }
}

Recall eq function

function eq(x, y) {
  return function*(sMap) {
    yield unify(x, y, sMap) // unify x and y
  }
}

run(1, [x], and(
  eq(x, y),
  or(eq(x, 1), eq(x, 2), eq(x, 3)),
  eq(y, 2)))

Results: [{x: 2}]

I extend the Core miniKanren to support more operators.

succeed

function succeed() {
  return function*(sMap) {
    yield sMap
  }
}
 
run(1, [x], succeed()) // [{x: x}]
run([x], or(eq(x, 1), succeed())) // [{x: 1}, {x: x}]

fail

function fail() {
  return function*(sMap) {
    yield null // failed to unify
  }
}
 
run(1, [x], fail()) // []
run(1, [x], and(eq(x, 1), fail())) // []

numbero, stringo, arrayo

run(1, [x], and(eq(x, 'haha'), stringo(x))) // [{x: 'haha'}]
run(1, [x], and(stringo(x), eq(x, 'haha'))) // []

conso, firsto, resto, emptyo, membero

cons(1, [2, 3]) // [1, 2, 3]
first([1, 2, 3]) // 1
rest([1, 2, 3])  // [2, 3]
 
run(1, [x, y], conso(x, y, [1, 2, 3])) // [ { x: 1, y: [ 2, 3 ] } ]
run(1, [x], firsto(x, [1, 2])) // [{x: 1}]
run(1, [x], resto(x, [1, 2]))  // [{x: [2]}]
run(1, [x], emptyo(x))         // [{x: []}]
 
run(1, [x], and(eq(x, 1), membero(x, [3, 2, 1]))) // [{x: 1}]

appendo

In prolog

append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :-
    append(Xs,Ys,Zs).

In logic.js (miniKanren)

function appendo(Xs, Ys, Zs) {
  return or(
    and(empty(Xs), eq(Ys, Zs)),
    (X=lvar(), Xs_=lvar(), Zs_=lvar())=> and(
      conso(X, Xs_, Xs),
      conso(X, Zs_, Zs),
      appendo(Xs_, Ys, Zs_)
    )
  )
}

appendo example

run([x, y], appendo(x, y, [1, 2, 3, 4, 5]))
/*
[ { x: [], y: [ 1, 2, 3, 4, 5 ] },
  { x: [ 1 ], y: [ 2, 3, 4, 5 ] },
  { x: [ 1, 2 ], y: [ 3, 4, 5 ] },
  { x: [ 1, 2, 3 ], y: [ 4, 5 ] },
  { x: [ 1, 2, 3, 4 ], y: [ 5 ] },
  { x: [ 1, 2, 3, 4, 5 ], y: [] } ]
 */

add, sub, mul, div

takes three arguments, and only works when at least two of the arguments are numbers

// x and y are logic variables
//
run([x], add(x, 3, 5)) // [{x: 2}]
run([x], add(x, y, 5)) // []
run([x], and(eq(y, 3), add(x, y, 5))) // [{x: 2}]
run([x], and(add(x, y, 5), eq(y, 3))) // [{x: 2}]