README

PHP中的miniKanren。

序言

这到底是什么？这是一个小巧的逻辑编程引擎！

逻辑编程是什么？逻辑编程是一种在很大程度上被低估的范式，它彻底改变了你编写、思考和运行程序的方式。

想象一下，你的程序是一系列关系。你可以将事物联系起来。每次你使用单向赋值 = 时，这个赋值现在变成了双向关系 ==。它可以双向进行。程序从输入到输出形成了一串关系链。

你可以引入逻辑变量，这些变量是未绑定的值（使用 fresh）。这些变量遵守通过关系施加在其上的约束。这使得你可以提供一个新的逻辑变量，并查看它被绑定到什么上。这就是你通常从逻辑程序中获取输出的方式。

通过使用合取（"and"）和析取（"or"），你可以形成逻辑关系。这允许你编码不同的执行流程。这一高级方法是 conde，它是一系列的合取。

所有这些逻辑关系形成了一棵树。程序的执行对应于通过树进行广度优先搜索，以根据关系统一提供的参数。这意味着程序可以找到多个解决方案，或者根本没有解决方案。

这种对程序思考和编写的革命性方式允许做一件非常神奇的事情：你可以逆向运行你的程序。

这意味着你可以要么给程序输入并寻找相应的输出，也可以提供输出并请求相应的输入。

示例

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（不等）

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']]

另请参阅

《Reasoned Schemer》
miniKanren
miniKanren（Byrd的论文）
microKanren
rKanren
《Clause and Effect》 by William F. Clocksin

igorw / reasoned

维护者

详细信息