今年四月左右，我心血来潮地为自己立了一个学习Prolog的目标——对，就是那门以逻辑编程和人工智能为卖点的语言。不仅要学会它的基本用法，还妄想用它像朋友圈广告里的Python那样，用来处理Excel文件中的大数据！

尽管处理大数据是开个玩笑，但学习Prolog的目标是真的。既然要学习一门编程语言，就必须找一本靠谱的教材。在无中生友之后，我选择了由谭浩强老先生主编的《Learn Prolog Now》作为入门读物。

尽管《Learn Prolog Now》的内容一点也不real world，却循序渐进、非常地适合初学者，每一章的结尾还准备了“上机题”。出人意料的是，仅仅在第三章就遇到了不会做的题目。在焦急地苦战一番未果后，我拖着疲惫的身躯搁置了它，继续学习后面的章节。

时隔五个月，我再次尝试解答这道题目。却惊喜地发现，只需要冷静地分析再仔细运用前三章学过的知识，解决这道题目也就是水到渠成的事情了。

所以到底是个什么题？

讲了这么多，是时候揭晓这它的真面目了。由于第三题以第二题为基础，因此一并搬运了过来

感兴趣的朋友也可以直接移步源网页查看。

看完上面的题目，只学过主流编程语言的朋友大概会是一头雾水，毕竟无论是代码还是术语，都与平日里使用的大相径庭。我来试着解释一下。像byCar(auckland, hamilton)和byTrain(metz, frankfurt)这样的代码，用Prolog的术语来讲叫做“事实”。就像数学中的公理一样，它们总是成立的。如果向Prolog提问，它会给出肯定的回答

byCar和byTrain被称为“谓词”，auckland和hamilton则是“原子”。

第二题要求定义travel/2，第三题要求定义travel/3。travel是谓词的名字，2和3则是它所接受的参数的个数。定义一个谓词就是给出描述它何时成立的“规则”，举个例子，可以定义一个名为len的谓词，只有当第二个参数等于第一个参数的长度时才成立

以大写字母开头的标识符（如题目中的X，上图中的T、L）是变量，在归一化（unification）时Prolog能够为它们赋值使得查询成立。

鉴于本文不是Prolog的入门教程，各位读者如果想进一步了解Prolog，还请移步《Learn Prolog Now》的相关章节。

先解决第二题吧

讲了这么多，该进入正题了。第二题其实不难，细心的读者应该已经发现，这题可以用递归来解决（就像上文的len一样）。

设谓词travel的两个参数分别叫做S和E，各代表起点和终点。显然，travel(S, E)成立，当且仅当：

1. 可以从S搭乘汽车（byCar）、火车（byTrain），或飞机（byPlane）抵达E，或者；
2. 存在另一个城市M，可以从S搭乘汽车、火车，或飞机抵达M，并且travel(M, E)也成立。

上述算法可以轻松地写成Prolog代码

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

byCar(auckland,hamilton).
byCar(hamilton,raglan).
byCar(valmont,saarbruecken).
byCar(valmont,metz).

byTrain(metz,frankfurt).
byTrain(saarbruecken,frankfurt).
byTrain(metz,paris).
byTrain(saarbruecken,paris).

byPlane(frankfurt,bangkok).
byPlane(frankfurt,singapore).
byPlane(paris,losAngeles).
byPlane(bangkok,auckland).
byPlane(singapore,auckland).
byPlane(losAngeles,auckland).

travel(S, E) :- just_go(S, E).
travel(S, E) :- just_go(S, M), travel(M, E).

just_go(S, E) :- byCar(S, E).
just_go(S, E) :- byTrain(S, E).
just_go(S, E) :- byPlane(S, E).

让Prolog告诉咱们这个travel/2写得对不对

精彩！

你话我猜？

Prolog不仅知道一个查询是否成立，还知道这个查询在什么参数下成立。例如，可以让Prolog告诉咱们，从valmont可以抵达哪一些城市，以及哪一些城市可以抵达auckland

这正是在接下来的题目中需要发扬光大的能力。

终于来到第三题

第三题所要求的travel是一个接受三个参数的谓词，第三个参数由从起点到终点的途径城市构成。设这个新的变量为R，那么travel(S, E, R)成立当且仅当：

1. 可以从S抵达E，并且R为go(S, E)，或者；
2. 存在另一个城市M，以及另一条路径R2。可以从S抵达M，并且travel(M, E, R2)成立，并且R为go(S, M, R2)。

那么如何在规则中描述R的结构呢？莫非是像上面的谓词len那样，在:-的右侧写上形如R is go(S, M, R2)这样的代码？

并不是。

借助Prolog强大的模式匹配能力，只需要在:-的左边声明R的结构即可

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

byCar(auckland,hamilton).
byCar(hamilton,raglan).
byCar(valmont,saarbruecken).
byCar(valmont,metz).

byTrain(metz,frankfurt).
byTrain(saarbruecken,frankfurt).
byTrain(metz,paris).
byTrain(saarbruecken,paris).

byPlane(frankfurt,bangkok).
byPlane(frankfurt,singapore).
byPlane(paris,losAngeles).
byPlane(bangkok,auckland).
byPlane(singapore,auckland).
byPlane(losAngeles,auckland).

travel(S, E, go(S, E)) :- just_go(S, E).
travel(S, E, go(S, M, R)) :- just_go(S, M), travel(M, E, R).

just_go(S, E) :- byCar(S, E).
just_go(S, E) :- byTrain(S, E).
just_go(S, E) :- byPlane(S, E).

加载这段代码后，就能让Prolog告诉我们，如何从valmont去往losAngeles了

Prolog不仅找出了题目中所给出的答案（见上图的第二行X =），还找出了另外一条可行的路径。

后记

确实不难，难怪可以作为第三章的习题。

序言

7月初的时候挑战了一下LeetCode的第29题（中等难度，似乎没什么值得夸耀的），题目要求在不使用除、乘，以及模运算的情况下，实现整数相除的函数。

既然被除数和除数都是整数，那么用减法就可以实现除除法了（多么naive的想法）。一个trivial的、用JavaScript编写的函数可以是下面这样的（为了简单起见，只考虑两个参数皆为正整数的情况）

1
2
3
4
5
6
7
8

function divide(n, m) {
  let acc = 0;
  while (n >= m) {
    n -= m;
    acc += 1;
  }
  return acc;
}

如此朴素的divide函数提交给LeetCode是不会被接受的的——它会在像2147483648除以2这样的测试用例上超时。可以在本地运行一下感受下究竟有多慢

1
2
3

➜  nodejs time node divide.js
2147483648/2=1073741824
node divide.js  1.14s user 0.01s system 99% cpu 1.161 total

那么有没有更快的计算两个整数的商的算法呢？答案当然是肯定的。

尝试优化

一眼就可以看出，运行次数最多的是其中的while循环。以2147483648除以2为例，while循环中的语句要被执行1073741824次。为了提升运行速度，必须减少循环的次数。

既然每次从n中减去m需要执行n/m次，那么如果改为每次从中减去2m，不就只需要执行(n/m)/2次了么？循环的次数一下子就减少了一半，想想都觉得兴奋啊。每次减2m，并且自增2的算法的代码及其运行效果如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

➜  nodejs cat divide2.js
function divide(n, m) {
  let acc = 0;
  let m2 = m << 1; // 因为题目要求不能用乘法，所以用左移来代替乘以2。
  while (n >= m2) {
    n -= m2;
    acc += 2;
  }
  while (n >= m) {
    n -= m;
    acc += 1;
  }
  return acc;
}

console.log(`2147483648/2=${divide(2147483648, 2)}`);
➜  nodejs time node divide2.js
2147483648/2=1073741824
node divide2.js  2.65s user 0.01s system 99% cpu 2.674 total

尽管耗时不降反升，令场面一度十分尴尬，但根据理论分析可知，第一个循环的运行次数仅为原来的一半，而第二个循环的运行次数最多为1次，可以知道这个优化的方向是没问题的。

如果计算m2的时候左移的次数为2，那么acc的自增步长需要相应地调整为4，第一个循环的次数将大幅下降至268435456，第二个循环的次数不会超过4；如果左移次数为3，那么acc的步长增至8，第一个循环的次数降至134217728，第二个循环的次数不会超过8。

显然，左移不能无限地进行下去，因为m2的值早晚会超过n。很容易算出左移次数的一个上限为

对数符号意味着即便对于很大的n和很小的m，上述公式的结果也不会很大，因此可以显著地提升整数除法的计算效率。

在开始写代码前，让我先来简单地证明一下这个方法算出来的商与直接计算n/m是相等的。

一个简单的证明

记被减数为n，减数为m。显然，存在一个正整数N，使得

令

，再令

，那么n除以m等价于

证明完毕。

从上面的公式还可以知道，新算法将原本规模为n的问题转换为了一个规模为r的相同问题，这意味着可以用递归的方式来优雅地编写最终的代码。

完整的代码

最终的divide函数的代码如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

function divide(n, m) {
  if (n < m) {
    return 0;
  }

  let n2 = n;
  let N = 0;
  // 用右移代替左移，避免溢出。
  while ((n2 >> 1) > m) {
    N += 1;
    n2 = n2 >> 1;
  }

  // `power`表示公式中2的N次幂
  // `product`代表`power`与被除数`m`的乘积
  let power = 1;
  let product = m;
  for (let i = 0; i < N; i++) {
    power = power << 1;
    product = product << 1;
  }
  return power + divide(n - product, m);
}

这个可比最开始的divide要快得多了，有图有真相

1
2
3

➜  nodejs time node divide3.js
2147483648/2=1073741824
node divide3.js  0.03s user 0.01s system 95% cpu 0.044 total

后记

如果以T(n, m)表示被除数为n，除数为m时的算法时间复杂度，那么它的递推公式可以写成下列的形式

但这玩意儿看起来并不能用主定理直接求出解析式，所以很遗憾，我也不知道这个算法的时间复杂度究竟如何——尽管我猜测就是N的计算公式。

如果有哪位好心的读者朋友知道的话，还望不吝赐教。

序言

理论上，开发人员是不允许操作生产环境的，更别说是像商品、订单这样的重要业务数据。不过对小公司来说，后台系统往往不是很完善，总有一些需求让运营或客服部门的同事操作起来捉襟见肘，不得不寻求开发人员的帮助。

通常这些部门的同事会给过来一批需要处理的商品或订单的ID，我会将它们粘贴到一个脚本中，并将脚本放到生产环境的机器上运行，以实现他们的ad hoc需求。ID一般用Excel文件，或在线文档的方式提供过来，将它们粘贴到脚本的源码中之后，还要为它们添加必要的引号和逗号，以满足所用语言的语法要求。比如下图就是直接粘贴后，VSCode提示错误的样子

那么，怎样才能不失逼格地给这批ID加上前后的引号及行末的逗号呢？

八仙过海，各显神通

有很多方法可以完成这个任务，比如借助VSCodemulti-cursor功能，手动添加前后缀

当要添加光标的位置处于同一列时，更适合用VSCode的另一个功能在下面添加光标（快捷键是command+option+↓）来实现，免去了一遍遍点击鼠标的烦恼。multi-cursor所敲入的每个光标还可以在各自的行上沿同方向移动不同的距离，适合处理每行长度不一致的情况。

也可以用Vim中的列编辑模式，操作体验差不多，还可以比VSCode按更少的键——起码不需要一直压着option键。

但列编辑模式不方便在行末追加内容——必须先在第一行的末尾敲入一个空格，往右移动依次光标，然后才能继续用列编辑模式批量添加后缀。

Emacs也有类似列编辑模式的功能，它的string-insert-rectangle命令比Vim的更便于添加后缀。但它没有默认的快捷键，需要先按下M-x，再输入命令名并回车，略为繁琐（尽管命令名可以自动补全）。

除了各家编辑器内置的功能，命令行工具也适合完成这种处理，比如可以用sed

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

➜  /tmp cat b
5FEB1AE4-239A-4276-8E37-BE913CE6D117
5FEB1AE4-239A-4276-8E37-BE913CE6D117
5FEB1AE4-239A-4276-8E37-BE913CE6D117
5FEB1AE4-239A-4276-8E37-BE913CE6D117
5FEB1AE4-239A-4276-8E37-BE913CE6D117
5FEB1AE4-239A-4276-8E37-BE913CE6D117
5FEB1AE4-239A-4276-8E37-BE913CE6D117
➜  /tmp sed -e "s/^/'/" -i '' b
➜  /tmp sed -e "s/$/',/" -i '' b
➜  /tmp cat b
'5FEB1AE4-239A-4276-8E37-BE913CE6D117',
'5FEB1AE4-239A-4276-8E37-BE913CE6D117',
'5FEB1AE4-239A-4276-8E37-BE913CE6D117',
'5FEB1AE4-239A-4276-8E37-BE913CE6D117',
'5FEB1AE4-239A-4276-8E37-BE913CE6D117',
'5FEB1AE4-239A-4276-8E37-BE913CE6D117',
'5FEB1AE4-239A-4276-8E37-BE913CE6D117',

有些从在线文档上复制下来的ID会有一行空行存在于两两之间，如果是在命令行的话，只需要先用grep筛选一遍即可，可组合性比编辑器更强。

美中不足的是，用sed处理后需要手动将文件b的内容粘贴到脚本中——如果是用Emacs的话，也可以用C-x i让编辑器在光标处直接插入该文件的内容。

如果可以寸步不离Emacs，通过简单的命令或快捷键来完成这个操作，岂不美哉？

自己动手，丰衣足食

用上自定义的Elisp函数后的效果如下

其实实现思路很简单：

1. 首先用户会选中一片要添加前后缀的区域；
2. 使用buffer-substring-no-properties函数复制这个region中的字符串，绑定为text；
3. 用read-from-minibuffer提示并读取用户输入待添加的前后缀字符串；
4. 用split-string将text切割为一行行的字符串，给每一行添加前后缀，再用mapconcat拼回一个字符串；
5. 用delete-region删除被选中的内容，然后用insert插入新的字符串。

最终的Elisp函数的定义如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14

(defun lt--insert-at-start-end ()
  "为TEXT中的每一行添加PREFIX前缀和SUFFIX后缀。"
  (interactive)
  (let* ((text (buffer-substring-no-properties (mark) (point)))
         (prefix (read-from-minibuffer "插入的前缀："))
         (suffix (read-from-minibuffer "插入的后缀："))
         (lines (split-string text))
         (decorated-lines
          (mapcar (lambda (line)
                    (concat prefix line suffix))
                  lines))
         (new-text (mapconcat 'identity decorated-lines "\n")))
    (delete-region (mark) (point))
    (insert new-text)))

欢迎读者朋友中的Emacs用户也来使用使用;-)

序言

《编码》这本书曾经在我的豆瓣“想读”列表中躺了很久，大概在今年年初才开始看。但读着读着发现书中的电路图越来越多，而我的阅读热情也随之被慢慢浇灭。五月初的时候，终究还是把它合上，并在豆瓣上羞愧难当地将其标注为“读过”。

抛开晦涩的电路图不谈，书中有一句话吸引了我的注意力

第一次读到这里时，我想作者应当会在下一段给出具体的证明过程——结果居然没有。难道作者觉得两侧的空白太小了，不足以写下他所发现的美妙证法？

受好奇心的驱使，我便试着证明书中的这个结论。

不过正式开始前，还得明确一下命题：对于任意的正整数a和b（a不等于b），10的a次幂和2的b次幂不相等。

先证明一条引理

为了证明上面的命题，需要先证明一条引理：对于任意的正整数a，5的a次幂是一个奇数。可以用数学归纳法来证明。

首先验证a为1时命题成立。由于5的1次幂为5，并且5是一个奇数，所以命题成立；

接着，假设a为k时命题成立，将5的k次幂写成2n+1的形式，当a为k+1时，

因此，5的k次幂也是一个奇数。因此，该命题对于任意的正整数a都是成立的。

同理可证：对于任意的正整数a，2的a次幂是偶数。

反证法证明原命题

假设存在正整数a和b（b大于a），使得10的a次幂与2的b次幂相等

将10分解为2和5的积，再两边同时除以2的a次幂

等式的左边和右边分别是5的正整数次幂与2的正整数次幂。由前一节的引理可知，左边是奇数，右边是偶数，两者不可能相等，与上述等式产生矛盾。因此，原假设不成立，命题得证。

后记

我最开始的想法很复杂。虽然也是采用反证法，但我将等式做了如下变换

然后试图证明以2为底的10的对数不是有理数，和等式右边不相等。不过这个方法于我而言太难了，便没有继续尝试下去。

序言

相信各位读者对秒表都不陌生，智能手机上通常都有这样一款软件

有一天心血来潮，便想要“复刻”一个命令行版本的秒表程序——主要是想尝试一下新学会的、“原地更新”的技能，而不是一行接一行地输出。程序的运行效果如下

那么这是怎么做的呢？

实现思路及代码

如何获取流逝的时间长度？

要实现一个秒表，首先要知道从开始计时至今过了多久。在*nix系统中，表示时刻的事实标准是Epoch Time，在shell脚本中要获取Epoch Time可以用date命令。再用首尾时刻相减便得到了期间流逝的秒数了，示例代码如下

1
2
3
4

begin_at=$(date '+%s')
# 睡个觉
end_at=$(date '+%s')
((interval=${end_at} - ${begin_at}))

双圆括号是一种在shell脚本中执行算术运算的语法，其它语法可以参见Math in Shell Scripts。

如何换算为时分秒？

有了interval中存储的总秒数后，换算成时分秒便是轻而易举的事情，示例代码如下

1
2
3

((hours=${interval} / 3600))
((minutes=(${interval} % 3600) / 60))
((seconds=(${interval} % 3600) % 60))

如何输出形如hh:mm:ss的格式？

hh:mm:ss的意思是分别用两个十进制数字显示时分秒，并以冒号分隔它们。如果有任何一个单位的数值小于10，便用字符0填充左侧的空白。按这个格式，凌晨1点2分3秒便会显示为01:02:03。

要在命令行中打印字符串，最容易想到的便是echo命令，只可惜它不能方便地实现填充字符0的需求。

强人所难也不是不行，示例代码如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

hours=1
minutes=2
seconds=3

if [ "${hours}" -lt '10' ];
then
   echo -n "0${hours}"
else
   echo -n "${hours}"
fi
echo -n ':'
if [ "${minutes}" -lt '10' ];
then
   echo -n "0${minutes}"
else
   echo -n "${minutes}"
fi
echo -n ':'
if [ "${seconds}" -lt '10' ];
then
   echo -n "0${seconds}"
else
   echo -n "${seconds}"
fi

更优雅的方法是用printf命令来自动填充左侧的字符0

1

printf "%02d:%02d:%02d" ${hours} ${minutes} ${seconds}

printf命令类似于C语言中的printf函数——它也支持打印转义的字符，下文会提到。

如何覆盖已经打印的内容？

今年以来我在断断续续地看Build Your Own Text Editor，学习如何开发文本编辑器。在这本小册子的第三章中，作者讲述了如何使用终端的转义序列（escape sequence）来控制屏幕上显示的东西——这正是秒表程序所需要的。

例如，在终端输出转义序列\x1b[2J可以清空屏幕，效果如下

为了覆盖已经打印出来的时分秒，需要：

1. 先将光标移动到行首；
2. 再清除从光标开始到行末的内容。

查阅《VT100 User Guide》第三章可以知道

1. 要把光标移动到行首可以用转义序列\x1b[8D。之所以是8，是因为按照hh:mm:ss输出时分秒后光标距离行首8个身位；
2. 要清除光标到行末内容可以用转义序列\x1b[0K（实际上，将光标移到行首只需要使用回车（carriage return）即可，但它被解释为开启新的一行了）。

更优雅的方法甚至连转义序列也不需要，只要用tput命令即可，示例代码如下

1
2
3
4

echo -n '11:22:33'
tput cr
tput el
echo '44:55:66'

关于cr和el，以及更多可以传给tput命令的参数，可以参见terminfo的man文档。

如何每隔一秒钟输出一次？

这大概是整个程序中最简单的需求了

1
2
3
4
5

while [ 1 -eq 1 ]
do
    # 此处可以为所欲为
    sleep 0.5
done

完整的秒表实现

至此，完整的秒表程序就可以实现出来了

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

#!/bin/bash
# 秒表，以hh:mm:ss的格式展示数据

begin_at=$(date '+%s')

while [ 1 -eq 1 ]
do
    end_at=$(date '+%s')
    # 算术运算：http://faculty.salina.k-state.edu/tim/unix_sg/bash/math.html
    ((interval=${end_at} - ${begin_at}))
    ((hours=${interval} / 3600))
    ((minutes=(${interval} % 3600) / 60))
    ((seconds=(${interval} % 3600) % 60))
    tput cr
    tput el
    printf "%02d:%02d:%02d" ${hours} ${minutes} ${seconds}
    sleep 0.5
done

运行后的效果正如本文开头的GIF所示。

全文完。