Print4D

逻辑式语言实践

06 May 2015

了解到 Prolog 之后,被逻辑式编程的思想深深震撼到了。为了更深入地理解逻辑式编程,我用 Lua 写了一个逻辑式语言的最小核心:miniKanren.luaminiKanren 是用 scheme 写成的一个逻辑引擎)


零,合一(Unification)

逻辑式语言的核心,就是合一(严格讲还有回溯,但是回溯主要涉及实现层面)操作符。合一操作是将两项(值或变量)关联起来,看起来和赋值操作很像。但是合一可以递归、重复地进行。

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

unify(x, y)
print(x)                         -- y
print(y)                         -- y

-- x, y 继续合一
unify(x, 1)
print(x)                         -- 1
print(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


一,miniKanren.lua


操作符

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。


连通 Lua

eq()、not_eq()、all() 和 cond() 返回一个函数。要运行起来得用 run() 函数来连通 Lua。

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

fresh_var() 函数的作用仅仅是为了生成了一个 miniKanren.lua 的变量,因为 Lua 没有宏不能改变求值规则,所以只能这样丑陋了。

run() 第 1 个参数为返回值的数量;第 2 个为返回值;第 3 个就是逻辑表达式了。这个逻辑表达式中 a 有两个取值:”a” 和 “b”。但是只返回 1 个值,即 {“a”}。

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

run_all() 返回所有值:

a, b = fresh_vars(2)
run_all({a, b}, cond(
    all(eq(a, b), eq(b, 1)),
    all(eq(a, b), eq(b, 2))))
-- { { 1, 1 }, { 2, 2 } }

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

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

如果逻辑表达式最终合一失败,返回空表,没有取值:

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


二,数独解法

以上大致就是 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)),

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

程序虽然不算短,但大都是一些变量绑定的操作。有营养的代码其实只有两条:声明元素各不相同;声明元素只能在 1 - 4 之间。这两条也正是数独游戏的规则。这就是逻辑式语言与众不同的地方,我们只用告诉它做什么,而不用在乎怎么做。因为这个原因,逻辑式语言也叫声明式语言。

list() 用于将 Lua 的 table 转换为 list 形式,关于转换的目的,以及 all_different() 和 fd_domain_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。那现在我们给它一个输出 4,问它哪些输入可以得到 4,它就会返回 letter = “d”。当然,这只是其中一个值,满足条件的还有 letter = “D”,考虑 run() 函数第 1 个参数。

回到数独解法的例子,如果使用传统的过程式语言来实现,无论如何也会陷入具体的计算细节。那假设我们写的不是如何解数独,而是一个对已经解开的数独序列的验证程序,那就简单多了。只需要套用数独的所有规则,对输入序列检查一次就行。也就是:每行、每列、每个块中的元素各不相同;每个元素只能在 1 - 4 之中。很熟悉吧,就是上面使用 miniKanren.lua 完成的那个解法。

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


仅仅是合一

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

alphabet() 写成逻辑语言的形式,是这样的:

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 被当成了新函数的输入。确实,所谓反向运行是相对于其他语言而言的,这里的“输出”是指其他语言中的输出。在逻辑语言中,输出仅仅只是合一成功还是失败。合一只是试图绑定每个变量或值使合一成功。所以,如果世上只有逻辑式语言,那也不会有什么反向运行的说法。有的仅仅是合一。


四,从合一开始

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


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 也没其他复合结构了)中的,如果套用 Lua 的思路来实现 head() 是这样的:

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

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

避免这个问题的要点是,要分解一个值,应该通过新的变量来合成这个值

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}}}} 这种链式结构。虽然,这样看起来丑陋了许多,但也不是那么出乎意料。因为 lisp 中的 list 虽然看起来和 Lua 和 table 是一样的:'(1 2 3 4),但在构造 list 时却是这样的:'(1 . (2 . (3 . (4))))。眼熟吧,就是 list() 将 table 转换之后的形式。

这样,事情变得很简单了,list 只有两个元素({4} 与 {4, {}} 等价),第二个元素也是一个 list。

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


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() 实现。


五,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 中所有四则运算和比较的函数。

(完)

参考资料: