igorw/reasoned

A miniKanren in PHP.

reasoned-php

A miniKanren in PHP., _(*1)

Prologue

What the hell is this? It's a tiny logic programming engine!, _(*2)

What is logic programming, you ask? Logic programming is a largely underrated paradigm that radically changes the way you write, think about, and run, programs., _(*3)

Imagine your program as a bunch of relations. You can relate things to each other. Every time you would use an uni-directional assignment =, that assignment now becomes a bi-directional relation ==. It goes both ways. The program forms a chain of relations from one or more inputs to one or more outputs., _(*4)

You can introduce logic variables that are unbound values (using fresh). These variables obey the constraints imposed on them through relations. This allows you to provide a fresh logic variable and see what it gets bound to. That's what you generally do to get an output from a logic program., _(*5)

Through the use of conjunction ("and") and disjunction ("or"), you can form logical relations. This allows you to encode different possible flows of execution. The higher-level method for this is conde, which is a disjunction of conjunctions., _(*6)

All of these logical relations form a tree. The execution of a program corresponds to a breadth-first search through the tree that unifies the provided arguments in accordance to the relations. This means that a program can discover more than one solution, or no solution at all., _(*7)

This radical way of thinking about and writing programs allows for something very amazing: You can run your programs backwards., _(*8)

What this means is that you can either give a program inputs and search for a corresponding output, but you can also provide outputs and ask for corresponding inputs., _(*9)

Examples

eq

var_dump(run_star(function ($q) {
    return eq($q, 'corn');
}));

// => ['corn']

conde

var_dump(run_star(function ($q) {
    return conde([
        [eq($q, 'tea')],
        [eq($q, 'cup')],
    ]);
}));

// => ['tea', 'cup']

firsto

var_dump(run_star(function ($q) {
    return firsto(['a', 'c', 'o', 'r', 'n'], $q);
}));

// => ['a']

resto

var_dump(run_star(function ($q) {
    return resto(['a', 'c', 'o', 'r', 'n'], $q);
}));

// => [['c', 'o', 'r', 'n']]

all

var_dump(run_star(function ($q) {
    return all([
        firsto(['a', 'l'], $q),
        firsto(['a', 'x'], $q),
        firsto(['a', 'z'], $q),
    ]);
}));

// => ['a']

fresh

var_dump(run_star(function ($q) {
    return fresh(function ($x) use ($q) {
        return all([
            eq(['d', 'a', $x, 'c'], $q),
            conso($x, ['a', $x, 'c'], $q),
        ]);
    });
}));

// => ['d', 'a', 'd', 'c']

membero

function membero($x, $l) {
    return conde([
        [fresh(function ($d) use ($x, $l) {
            return conso($x, $d, $l);
         })],
        [fresh(function ($a, $d) use ($x, $l) {
            return all([
                conso($a, $d, $l),
                membero($x, $d),
            ]);
         })],
    ]);
}

var_dump(run_star(function ($q) {
    return all([
        membero($q, [1, 2, 3]),
        membero($q, [2, 3, 4]),
    ]);
}));

// => [2, 3]

run

var_dump(run(3, function ($q) {
    return membero('tofu', $q);
}));

// => [['tofu', '.', '_.0']
//     ['_.0', 'tofu', '.', '_.1']
//     ['_.0', '_.1', 'tofu', '.', '_.2']]

appendo

var_dump(run_star(function ($q) {
    return appendo([1, 2, 3], [4, 5, 6], $q);
}));

// => [[1, 2, 3, 4, 5, 6]]

neq (disequality)

var_dump(run_star(function ($q) {
    return all([
        membero($q, [1, 2, 3]),
        neq($q, 2),
    ]);
}));

// => [1, 3]

rembero

function rembero($x, $l, $out) {
    return conde([
        [eq([], $l), eq([], $out)],
        [fresh(function ($a, $d) use ($x, $l, $out) {
            return all([
                eq(pair($a, $d), $l),
                eq($a, $x),
                eq($d, $out),
            ]);
         })],
        [fresh(function ($a, $d, $res) use ($x, $l, $out) {
            return all([
                eq(pair($a, $d), $l),
                neq($a, $x),
                eq(pair($a, $res), $out),
                rembero($x, $d, $res),
            ]);
         })],
    ]);
}

var_dump(run_star(function ($q) {
    return rembero('b', ['a', 'b', 'c', 'b', 'd'], $q);
}));

// => [['a', 'c', 'b', 'd']]

See also

• The Reasoned Schemer
• miniKanren
• miniKanren (Byrd's Dissertation)
• microKanren
• rKanren
• Clause and Effect by William F. Clocksin