Print4D

逻辑式语言实践

06 May 2015

了解 Prolog 之后，被逻辑式编程的思想深深惊愕到了。为了更深入地理解逻辑式编程，我用 Lua 写了一个逻辑式语言的最小核心：miniKanren.lua（miniKanren 是用 scheme 写成的一个逻辑引擎）



1. 合一（Unification）

逻辑式语言的核心，就是合一。合一是将两个项（值或变量）关联起来，看起来和赋值操作很像，但合一可以重复、递归地进行。

-- 两个值进行合一
unify(1, 1)
unify("hello", "hello")

-- 两个变量进行合一
unify(x, y)
print(x)                         -- y, x 和 y 关联起来了
print(y)                         -- y

-- x, y 继续合一
unify(x, 1)
print(x)                         -- 1
print(y)                         -- 1，由于 x 和 y 已经关联起来，所以 y 也是 1

-- 递归地模式匹配
unify({1, 2, 3}, {a, b, c})
print(a)                         -- 1
print(b)                         -- 2
print(c)                         -- 3

-- 合一也有可能失败
unify(1, 2)                      -- false
unify(true, false)               -- false
unify({1, 2, 3}, {n, m, 1})      -- false


2. miniKanren.lua


2.1. 操作符

miniKanren.lua 提供 4 个操作符：

eq() 接受两个参数，将两个项进行合一操作，合一失败时返回 false：

eq(a, 1)    -- succeed
eq(b, 2)    -- succeed
eq(a, b)    -- false

not_eq() 意思相反，当合一成功时返回 false：

eq(a, 1)        -- succeed
eq(b, 2)        -- succeed
not_eq(a, b)    -- succeed
not_eq(1, 1)    -- false

all() 和 cond() 接受任意个参数：all() 类似 and，仅当每一项都成功时，all() 成功，否则合一失败；而 cond() 则类似 or。

all(
    eq(a, 1),
    eq(b, 2)
    )           -- succeed

all(
    eq(a, 1),
    eq(b, 2),
    eq(a, b)
    )           -- false

cond(
    eq(a, 1),
    eq(b, 2),
    eq(a, b)
    )           -- succeed

cond(
    eq(1, 2),
    eq(true, false)
    )           -- false


2.2. 运行 miniKanren.lua

miniKanren.lua 对外接口为 run() 函数。

x = fresh_vars(1)
run(1, x, cond(
       eq(x, "a"),
       eq(x, "b")))
-- {"a"}

因为 Lua 不能像 scheme 那样使用 Macro 改变求值规则，所以需要用 fresh_var() 初始化变量。

run() 第 1 个参数为返回值的数量；第 2 个参数指定返回哪个变量；第 3 个参数定义逻辑表达式。上面这段代码中 x 有两个取值：”a” 和 “b”，因为只返回一个值，所以结果为 {“a”}。

run(2, x, cond(
       eq(x, "a"),
       eq(x, "b")))
-- {"a", "b"}
-- 返回 "a" 和 "b" 2 个值

run_all() 返回所有可能的值。

x, y = fresh_vars(2)
run_all({x, y}, cond(
    all(eq(x, y), eq(y, 1)),
    all(eq(x, y), eq(y, 2))))
-- { { 1, 1 }, { 2, 2 } }

如果变量没有与特定的值绑定，则返回字符串 “_.0”，表示可以为任意值。当然，这应该在逻辑表达式合一成功的前提下。

x, y = fresh_vars(2)
run_all(x, eq(1, y))
-- { "_.0" }

如果逻辑表达式合一失败，返回空表，表示没有取值。

x = fresh_vars(1)
run(false, x, all(
       eq(x, 1),
       eq(x, 2)))
-- {}


3. 数独解法

以上大致就是 miniKanren.lua 的全部功能，好像不容易看出亮点何在。下面是用 miniKanren.lua 写成的一个 4x4 数独解法，可以展示逻辑式编程与其他编程语言的不同之处。

local function v() return fresh_vars(1) end
local function sudoku_4x4(puzzle)

   -- 将 table 变为 list 形式
   puzzle = list(unpack(puzzle))

   -- 初始化所有 run() 函数中会用到的变量
   local s11 , s12, s13, s14,
         s21 , s22, s23, s24,
         s31 , s32, s33, s34,
         s41 , s42, s43, s44,
         row1, row2, row3, row4,
         col1, col2, col3, col4,
         square1, square2, square3, square4 = fresh_vars(28)

   local r = run(1, puzzle,
      all(
          -- 将数独序列的值绑定到相应的变量
          eq(puzzle, list(s11, s12, s13, s14,
                          s21, s22, s23, s24,
                          s31, s32, s33, s34,
                          s41, s42, s43, s44)),
          eq(row1, list(s11, s12, s13, s14)),
          eq(row2, list(s21, s22, s23, s24)),
          eq(row3, list(s31, s32, s33, s34)),
          eq(row4, list(s41, s42, s43, s44)),
          eq(col1, list(s11, s21, s31, s41)),
          eq(col2, list(s12, s22, s32, s42)),
          eq(col3, list(s13, s23, s33, s43)),
          eq(col4, list(s14, s24, s34, s44)),
          eq(square1, list(s11, s12, s21, s22)),
          eq(square2, list(s13, s14, s23, s24)),
          eq(square3, list(s31, s32, s41, s42)),
          eq(square4, list(s33, s34, s43, s44)),

          -- 声明每一行、每一列和每一角中的所有数字都不相同                       1
          all_different(list(row1, row2, row3, row4,
                             col1, col2, col3, col4,
                             square1, square2, square3, square4)),
          -- 声明 puzzle 中的每一个值都必须在 1 - 4 之间                       2
          fd_domain_4(puzzle)
       ))

   -- 如果 r 有值，则将 list 转换成 table 返回
   return #r == 0 and r or list2table(r[1], {})
end

local l = {
   v(), v(), 2  , 3  ,
   v(), 2  , v(), v(),
   2  , v(), v(), v(),
   v(), v(), 1  , 2  ,
}

sudoku_4x4(l)
-- { 1, 4, 2, 3,
--   3, 2, 4, 1,
--   2, 1, 3, 4,
--   4, 3, 1, 2 }

代码中的 list() 用于将 Lua 的 table 转换为 list 形式，关于转换的目的，以及 all_different() 和 fd_domain_4() 的实现，后文会提到。

程序不算短小，但大都是一些变量绑定的操作，有营养的代码只有两句：1，声明元素各不相同；2，声明元素只能在 1 - 4 之间。这两点也正是数独游戏的规则。

这就是逻辑式语言与众不同的地方，只用告诉它做什么，而不用管怎么做。因为这个原因，逻辑式语言也叫声明式语言。


4. 反向运行

逻辑式语言之所以有这个特点，原因在于它反向运行（run backward）的特性。普通的函数，我们给定一个输入，它返回相应的输出。反向运行，给定一个输出，它能返回满足这个输出的所有输入。

比如转换字母为相应数字的函数：

local function alphabet(letter)
   if     letter == "a" or letter == "A" then return 1
   elseif letter == "b" or letter == "B" then return 2
   elseif letter == "c" or letter == "C" then return 3
   elseif letter == "d" or letter == "D" then return 4
   end
end
alphabet("a") -- 1

调用 alphabet(“a”) 得到结果 1。

如果在 miniKanren.lua 中实现这函数，我们就能给它一个输出 4，问它哪些字母可转换为 4，程序就会返回『”d”、”D”』。

回到数独解法的例子，如果使用传统的过程式语言，无论如何也会陷入具体的计算细节。假设我们写的不是如何解数独，而是一个对已经解开的数独序列的验证程序，就会简单许多。只需要套用数独的所有规则，对输入序列检查一下就行。

数独的规则就是：1，每行、每列、每个块中的元素各不相同；2，每个元素只能在 1 - 4 之中。看着很熟悉吧，就是上面使用 miniKanren.lua 完成的数独解法。

实际上，使用 miniKanren.lua 完成的数独程序确实是一个数独的验证程序，但它具有反向运行的特点，即给它一个输出 true（数独验证程序的输出是什么？就是验证成功或者验证失败），它会返回满足输出 true （即验证成功）的所有输入。


4.1. 仅仅是合一

要理解反向运行，应该从合一说起。之所以说逻辑语言的核心是合一，是因为逻辑语言中的函数，例如数独程序中的 all_different()、fd_domain_4()，其内部实现都是若干个合一操作的组合。合一操作符的返回值只有两种，成功或者失败。

alphabet() 在 miniKanren.lua 中的实现是这样的：

local function alphabet(letter, number)
   return cond(
      all(cond(eq(letter, "a"), eq(letter, "A")),
         eq(number, 1)),
      all(cond(eq(letter, "b"), eq(letter, "B")),
         eq(number, 2)),
      all(cond(eq(letter, "c"), eq(letter, "C")),
         eq(number, 3)),
      all(cond(eq(letter, "d"), eq(letter, "D")),
         eq(number, 4)))
end

letter, number = fresh_vars(2)
run_all(number, alphabet("a", number))   -- {1}
run_all(letter, alphabet(letter, 4))     -- {"d", "D"}

原本是输出的 number 被当成了新函数的输入。确实，所谓反向运行是相对其他语言来说的，这里的『输出』是指其他语言中的输出。在逻辑语言中，输出只有合一成功或者失败。假如世上只有逻辑式语言，那也不会有什么反向运行的说法，有的仅仅是合一。


5. 从合一开始

逻辑式语言中的所有函数都是由合一组合而成的。


5.1. fd_domain_4()

从 fd_domain_4() 开始，这个函数接受一个数字序列，并确保这个序列中的每一个数字都在 1 - 4 之间。如果有一个数字没有在其中，则合一失败。很自然的想法，先写一个验证单个数字的函数 single_domain_4()，然后对序列的每一个数字调用 single_domain_4()，直到序列为空。

local function single_domain_4(n)
   return cond(
      eq(n, 1),
      eq(n, 2),
      eq(n, 3),
      eq(n, 4))
end

single_domain_4() 很简单，难的是如何取出序列的第 1 个和剩余元素。假设这个序列是存在 table（Lua 也没其他复合结构了）中的，如果按照 table 的思路来实现 head() 是这样的：

local function head(t, head)
    return eq(t[1], head)
end

这样实现 head() 函数是有问题的。在 miniKanren.lua 中，要处理每一个参数都可能不是数字、字符串、table 等固定的类型，它可能是一个等待绑定的变量。如果希望知道什么 table 的第 1 个元素是 “a”，调用 head(t, "a")，这个时候会对一个变量 t 进行 t[1] 操作，从而产生异常。

避免这个问题的要点是，要分解一个元素，应该通过新的元素来合成这个元素。改进 head() 的实现：

local function head(t, head)
   local tail = fresh_vars(1)
   return eq({head, tail}, t)
end

这样新问题又来了，head() 把 table 看成只有两个元素，如果试图对包含两个以上元素的 table 调用 head()，会导致合一失败，得到一个空值。

这就是为什么使用 list() 函数将 table 转换成 list 的原因，list 是 lisp 中一种由序对构成的链表。也就是将形如 {1, 2, 3, 4} 的 table 转换成 {1, {2, {3, {4}}}} 这种链式结构。虽然，这样看起来很不直观，但好处是保证了 list 中只有两个元素（{4} 与 {4, {}} 等价），从而很方便的取到表头和表尾。

tail() 和 head() 类似：

local function tail(t, tail)
   local head = fresh_vars(1)
   return eq({head, tail}, t)
end

head() 和 tail() 还可以合并成一个函数：

local function tableo(head, tail, t)
    return eq({head, tail}, t)
end

fd_domain_4() 需要的部件都齐备了：

local function fd_domain_4(l)
   local head, tail = fresh_vars(2)
   return cond(
      eq(l, {}),
      all(
         tableo(head, tail, l),
         cond(
            eq(head, 1),
            eq(head, 2),
            eq(head, 3),
            eq(head, 4)),

            -- 这里本来应该是 fd_domain_4(tail) 的
            -- 放到匿名函数中是为了防止提早求值，进入无限循环
            function(s) return fd_domain_4(tail)(s) end))
end


5.2. all_different()

all_different() 的实现比 fd_domain_4() 要复杂一些，方式还是一致的，不同的是 all_different() 中使用的是 not_eq()。 这是其中一个子函数 different_others() 的实现：

local function different_others(x, t)
   local head, tail = fresh_vars(2)
   return cond(
      eq(t, {}),
      all(
         tableo(head, tail, t),
         not_eq(x, head),
         function(s) return different_others(x, tail)(s) end
      ))
end

这个函数确保某一个值（x）不同于 table（t）中的每一个元素。这里 包含了完整的 all_different() 实现。


6. One More Thing

all_different() 是 prolog 中的内置函数，prolog 中也有一个类似 fd_domain_4() 的内置函数，叫 fd_domain()，接受三个参数，第 1 个是 list，第 2 和第 3 个参数指明限制的下界和上界。这里没有这样设计是为了简单，如果允许指定界限之后就不得不对数字进行比较。数字的比较和计算，在 miniKanren.lua 中是不能想当然的直接进行的。原因前面提过到过，操作一个元素，应该先将它分解成子元素，再重新组合得到新的结果。但是数字再分解又是什么呢？

local function add(a, b, sum) return eq(a + b, sum) end
add(a, b, 10) -- error

数字是可以分解的，答案就是表示成二进制。在处理数字之前先将数字比如 10 转换成二进制的序列 {0, {1, {0, {1}}}} （倒置的序列），之后数字的处理都是对二进制序列的位操作。这里 是 miniKanren.lua 中所有四则运算和比较的函数。

（完）

参考链接：