乍听之下,不无道理;仔细揣摩,胡说八道

0%

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

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

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

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

所以到底是个什么题?

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

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

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

byCarbyTrain被称为“谓词”,aucklandhamilton则是“原子”。

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

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

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

先解决第二题吧

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

设谓词travel的两个参数分别叫做SE,各代表起点和终点。显然,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,并且Rgo(S, E),或者;
  2. 存在另一个城市M,以及另一条路径R2。可以从S抵达M,并且travel(M, E, R2)成立,并且Rgo(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键。

Vim列模式的效果

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

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

Emacs的string-insert-rectangle的效果

除了各家编辑器内置的功能,命令行工具也适合完成这种处理,比如可以用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-stringtext切割为一行行的字符串,给每一行添加前后缀,再用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用户也来使用使用;-)

序言

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

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

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

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

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

先证明一条引理

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

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

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

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

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

反证法证明原命题

假设存在正整数abb大于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'

关于crel,以及更多可以传给tput命令的参数,可以参见terminfoman文档。

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

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

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所示。

全文完。