Weirane的 RSS 预览

开始读《异见时刻》

2024-09-08 00:00:00

打算开始读《异见时刻：“声名狼藉” 的金斯伯格大法官》。这是一本前美国最高法院大法官 Ruth Bader Ginsburg (RBG) 的传记。RBG 是美国最高法院第二位女性大法官。最开始听说 RBG 是在詹青云做客鲁豫的一集播客中（岩中花述 S5E1，03/12/2024）。当时好像正好是在 DC 市里面逛，听到 RBG 的墓就在 arlington national cemetary，本来打算去看看的，结果当时比较晚了就没去。当然后来有时间就去瞻仰了一下 RBG 和她丈夫的墓。

当时听播客的时候有一个点我印象很深，就是阿詹说 RBG 是一个相信慢慢努力的人。因为法律的改变是非常缓慢的，她不会去想着一定要做那些有着划时代意义的大案子，而是一点点地搭建人们对男女不应该区别对待的认知。当 RBG 处在一个保守派占多数的最高法院的时候，她会努力去和保守派法官妥协，就算放弃自己意见中的一些激进的部分，也要去争取保守派的票从而赢得这个 case。在她发现无法胜利的时候，她仍然会站出来并更加努力地表达自己 “I dissent” 的态度，尽管当时的判决并不会改变。这种精神虽然不会在现实中有立即的作用，但也是非常有价值的。比如她在 Ledbetter v. Goodyear Tire & Rubber Co. 案的反对意见¹中建议国会立法推翻最高法院的决定，结果在奥巴马当选总统之后就实现了。

正好我最近突然意识到我自己其实就是处在一个 “无法接受微小的进步” 的状态里。很多时候需要去做一些细枝末节的事情，但是我在做的时候会没有意义感，从而无法专心做事。说来我意识到我处在这个状态也是从金刚经中的 “应无所住而生其心” 来的。当时听王德峰讲六祖惠能和神秀的偈句的不同²，一时间突然意识到我和神秀犯的错误其实是一样的：就是沉浸在小乘佛教的自了汉的境界中了。而要达到大乘菩萨的境界，是需要在现实世界中产生影响，去帮助具体的人，做具体的事的。如果 RBG 只在小乘佛教的境界中，她大可以在一些 5 比 4 的判决中拒绝和保守派的法官妥协，就说我自己坚持了自己的原则，但是以案子的失败作为代价。虽然这样做自己的 “心” 没有 “惹尘埃”，但是除了显得自己境界高没有任何现实的作用。我们意识到万物皆性空之后不能执着于空。

这两周看阿詹和阿庞的直播的时候又重新听到了她们对《异见时刻》的推荐。希望能从书中得到一些来自 RBG 的智慧和 inspiration。

https://supreme.justia.com/cases/federal/us/550/618/ ↩
https://www.bilibili.com/video/BV1Mu411Z7eN/ ↩

中美文化差异

2024-08-08 00:00:00

最近看了不少中国哲学的书和视频，想来结合我的经历说一下我浅薄的理解。我主要看的是复旦的王德峰老师的视频。最开始看王德峰老师是从他的 “中西方文化差异的渊源” 入坑的，然后又陆续看了马克思哲学、阳明心学、艺术哲学等等课程，感觉非常长脑子。他有很多片段在 B 站上都很火，特别是讲金刚经三句义的那一段。有兴趣的可以去搜一搜。

我现在在美国也待了有三年了。就我的感觉来说，中国的文化比较讲究平衡，凡事不做到极致，但是美国恰恰相反。美国人喜欢把所有事情都做到当前认知下的极致，然后就相对地固定下来。好像美国人倾向于相信对于每一件事情，世界上都有唯一最好的一个处理方式。而且一旦我们发现了这个方式，就要一直坚持。如果发现了问题，那就应该在现有方式的基础上修补，而不是去推翻之前已经存在的知识。我印象很深的一个事情就是我在 UCSD 的导师说他相信 “there has to be a best way to design it”。我不记得具体是 design 什么了，但是这种对 “the best way” 的执着当时对我有很大的冲击。

举例

在别的领域里也可以体现出美国的这种目标明确，努力到极致的文化的例子。

城市规划

我最开始看美国城市（特别是新规划的郊区）的地图的时候有一种感觉，就是感觉规划得非常清晰。你能看出来哪里是住宅区，哪里是商业区，哪里是医院，哪里是公园等等，在地图上非常清晰地用不同颜色标注出来了。而看国内城市的地图的时候就会发现好像所有东西是交织在一起的。我的猜想是，由于美国需要用概念和逻辑来找到那个 “最好” 的规划方案，把城市划分成不同的单一功能的区域可以显著降低在规划过程中的复杂度。由于推理的单位从单个的楼房变成了一片区域，他们在规划的过程中需要处理的变量也就更少了，也就更方便了。

但是这种单一功能的规划也会产生问题。这种规划会导致大多数人无法只通过走路从一个区到另一个区。比如住在 single family house 的人无法走路去一个 plaza 买菜。所以造成干什么都要开车的现象。有调查显示在美国，一半的行程是小于五公里的，但是就算这种短距离的出行需求也只能开车，这就加剧了交通的拥堵。所以现在美国又在研究新的模式，比如 TOD 就是一个最近很热的概念。

汽车文化

汽车文化应该是美国最核心的文化之一了。而开车本身就是一个目标非常明确的活动。你需要在脑子里想好一个目的地，然后可能要在地图软件里输入它，然后你就（像一个机器一样地）跟着地图的指引开车。开车和走路不同，开车的时候你无法自由地改变你的行进方向，也不能随时停下休息或者看风景。

有人可能说开车和走路不具备可比性，因为开车可达的半径比走路大多了。那如果我们把开车和乘坐公共交通比较的话，就会发现美国的汽车文化还是会导致你出行的目的性非常强。虽然乘坐公共交通也需要你有一个目的地，但是你的目的地是一大片区域，而不是某一个餐馆或商店。在美国的郊区，你开车到达一个 plaza 停下后，你的目标是很清晰的：我就是要去这个餐厅吃饭。吃完饭之后就回到车上了，你就又需要重新有意识地 “决定” 你的下一个目的地是哪里。如果是在城区选择乘坐公共交通，你在下车之后是一定会走一段路的，而且你的目的地在绝大部分情况下并不是某一个商店，而是一个行人友好的商圈。你在这个商圈中是可以自由地行走的，而且你在自由地行走的过程中会碰到各种意想不到的事情。说不定你看中了某个商店想进去逛逛，或者是你恰好碰到了一个好朋友。这种事情在美国郊区去哪儿都要开车的情境下是很难发生的。

“专业性”

最近还看了 Gad Elmaleh 在 Netflix 上的单口专场 American Dream（强推），里面提到了他作为一个法国移民在美国感受到的文化冲击。他说的很多东西都可以用做事到极致来概括。

他提到他在美国遇到了一个工作非常认真尽责的商场的导购。他想让导购帮忙找一件毛衣，导购找了半天回来很伤心地说没有找到，他正想安慰的时候导购突然说他再去 double check 一下，这让 Gad 非常惊讶，因为法国导购甚至不会 single check。首先这个故事可能有艺术加工的部分，但是一定程度上还是能反映美国人对工作的态度的。当然也可以说这是一种专业性的体现，但是专业性本身就是一种 “做事到极致”。我发现我现在有点反感这种专业性，因为过度的追求专业性其实是非常 dehumanizing 的，是一种对人的异化。我自己也在尝试去寻找这个平衡点应该在哪里，让我在保持专业性的同时也让它在一个可接受的程度里。

为什么呢

美国是一个很新的国家，没有什么历史，也没有什么包袱，所以它可以从零开始，但是这也意味着美国社会的共识是很少的。所以美国需要用最底层的语言和理性来构筑这个社会。只要是语言可以概括的东西一定要表达得很清楚。之前也看过一个说法是由于美国是各地的移民组成的国家，所以形成了一种 low context culture，所以需要尽量用语言把话说得很明白。

感受

感觉美国人每天都活在一个巨大的实验室里。几乎所有的行为都和 “科学研究” 的结果相关，依照逻辑的推理来做各种决定。比如在政治竞选中，你可以很清晰地说出哪些 “议题” 是你关心的，你的 “立场” 是什么，美国人有各种各样的词语来形容世间万物。其实我是很佩服这种 “我命由我不由天” 的精神和希望改造世界的精神的。

美国社会的模式很像加密货币使用的模式。加密货币有价值是因为它用了算力作为壁垒。因为算力不是一个容易获得的资源，所以算力所产出的加密货币才有价值，尽管不存在一个中央银行来管控货币。而美国的模式就是先假设所有人都是自私的，然后每个人都为自己的利益奋斗。因为人的智力、能力等等不是一个容易获得的资源，所以不需要一个中心的权威来告诉人们资源该怎么分配，而是说赢了这个博弈游戏的人获得资源。

东西方哲学也很像 lambda calculus 和图灵机之间的关系。两者其实都是宇宙的真理，只不过一个自上而下，一个自下而上。但是归根到底两者是等价的，描述的都是人世间的规律。马克思说资本主义发展到最后一定会进入社会主义。我的一个理解可以说是资本主义是指科学的，使用抽象概念，注重达到抽象指标的发展，而社会主义是更加人本的发展。其实现在在美国也在往这方面进步。比如说医疗保险里面处方药的价格是按能吃多少天计算的，也就是说它规定好了无论你吃什么药，你有一个固定的预期每个月需要花多少钱，这就是更加人本的模式。但是我们怎么才能达到这种更加人本的发展模式呢？可能也只能借鉴西方的发展模式。就像 lambda calculus 非常抽象，但是我们可以用图灵机去实现它。

相关阅读

Amy Ko 的博客文章：Cars are unjust
我有一篇讲 lambda calculus 的博客：链接
城市规划和公共交通的 YouTube Channel: Not Just Bikes
王德峰老师的 B 站主页
Gad Elmaleh: American Dream

关于基于表达式的编程语言的一些思考

2021-12-25 00:00:00

最近学 Go 语言又想起之前看过的一个 talk，presenter 说他几乎不用 else 关键字。因为一般情况下，if 语句的其中一个 branch 会比较短（比如处理特殊情况），这样可以在这个 branch 结束后直接从函数返回，后续的代码就不需要进行缩进了，如

func fact(n int) int {
    if n <= 1 {
        return 1
    }
    // no extra indent here!
    return fact(n - 1) * n
}

可以减少缩进当然是件好事。如果后续代码很长可以采用这种风格。但我觉得并不是所有的情况都适用于这种写法。相比之下我更喜欢这样的写法

int fact(int n) {
    return n <= 1 ? 1 : fact(n - 1) * n;
}

或者使用 else

fn fact(n: i32) -> i32 {
    if n <= 1 {
        1
    } else {
        fact(n - 1) * n
    }
}

Go 语言里没有三目运算符，因为语言设计者认为滥用三目运算符可能会降低可读性 ¹。三目运算符的可读性确实没有 if 语句高，但是问题的核心其实不在三目运算符。三目运算符的鼻祖 C 需要它是因为 C 的 if 语句不是一个表达式，所以需要一个新的语法来表示 if 表达式。相比很多语言就不需要三目运算符，因为它们的 if 本身就是一个表达式。同时 if 语句的可读性也比三目运算符高不少，用 else if 再添加几个 branch 也不会降低可读性。

对我来说基于表达式可以让代码更容易理解。在理解一个基于表达式的程序时，我们可以自底向上地学习程序，从小的表达式开始理解，再理解上级的表达式。如果表达式没有副作用，在学习了这个表达式之后就可以把它看作一个黑盒了。一般来说函数式的语言都会支持更多类型的表达式（如 if 表达式），函数式语言的宗旨之一也是通过组合无副作用的函数而实现更复杂的功能。

go.dev 上的观点应该可以算是语言设计者的吧 https://go.dev/doc/faq#Does_Go_have_a_ternary_form ↩

使用 bwrap 隔离 WPS Office

2021-08-20 00:00:00

看到依云在博客中提到了非特权沙盒工具 bwrap。博客的结尾提到可以用它来跑一些不太干净的软件，便来配置一下 WPS Office。

WPS 目前（AUR 版本 11.1.0.10702-1）还有使用反斜杠作为文件路径分隔符的问题，不过没有影响到外部的观感，只是在 ~/.local/share/Kingsoft 内部。但是它每次运行都会在后台启动 wpscloudsvr 进程，可能和云同步有关吧，每次还要 kill 一下，有点麻烦。另外作为那种不得不使用的商业软件，还是感觉隔离一下舒服一些。

使用的 bwrap 命令修改自依云的博客。wrap-wps 脚本如下：

#!/bin/bash

# 根据扩展名选择对应的 WPS 程序
file=$1
case $file in
    *.doc | *.docx) exe=/usr/bin/wps ;;
    *.xls | *.xlsx) exe=/usr/bin/et ;;
    *.ppt | *.pptx) exe=/usr/bin/wpp ;;
    *) exe=/usr/bin/wps ;;
esac

binds=()
for dir in fontconfig gtk-2.0 gtk-3.0 mimeapps.list Kingsoft; do
    binds+=(--ro-bind ~/.config/"$dir" ~/.config/"$dir")
done

# bind mount 需要操作的文件
if [[ -f "$file" ]]; then
    path="$(realpath "$file")"
    binds+=(--bind "$path" "$path")
fi

exec bwrap --unshare-all --die-with-parent \
    --ro-bind / / \
    --tmpfs /sys --tmpfs /home --tmpfs /tmp --tmpfs /run --proc /proc --dev /dev \
    --ro-bind "$XDG_RUNTIME_DIR" "$XDG_RUNTIME_DIR" \
    --ro-bind /tmp/.X11-unix /tmp/.X11-unix \
    "${binds[@]}" \
    --ro-bind ~/Documents ~/Documents \
    --bind ~/tmp ~/tmp \
    "$exe" "$@"

可以在使用此脚本之前运行一下 wps，让它生成 ~/.config/Kingsoft，避免每次启动还要同意一下许可证。

再写一个 application 文件并配置上文件类型关联。把 /usr/share/applications/wps-office-prometheus.desktop 复制到 ~/.local/share/applications/wps-office-wrap.desktop，并把 Exec 的命令改成上面的 wrap-wps，InitialPreference 调成 99，把各个 WPS 程序的 MimeType 合并。如下

diff --git a/usr/share/applications/wps-office-prometheus.desktop b/home/wang/.local/share/applications/wps-office-wrap.desktop
index 820214f..87ab130 100644
--- a/usr/share/applications/wps-office-prometheus.desktop
+++ b/home/wang/.local/share/applications/wps-office-wrap.desktop
@@ -2,7 +2,8 @@
 Comment=Use WPS Writer to office work.
 Comment[zh_CN]=使用 WPS 2019进行办公
-Exec=/usr/bin/wps %F
+Exec=/home/wang/scripts/wrap-wps %U
 GenericName=WPS
 GenericName[zh_CN]=WPS 2019
+MimeType=application/wps-office.et;application/wps-office.ett;application/wps-office.ets;application/wps-office.eto;application/wps-office.xls;application/wps-office.xlt;application/vnd.ms-excel;application/msexcel;application/x-msexcel;application/wps-office.xlsx;application/wps-office.xltx;application/vnd.openxmlformats-officedocument.spreadsheetml.sheet;application/wps-office.uos;application/wps-office.dps;application/wps-office.dpt;application/wps-office.dpss;application/wps-office.dpso;application/wps-office.ppt;application/wps-office.pot;application/vnd.ms-powerpoint;application/vnd.mspowerpoint;application/mspowerpoint;application/powerpoint;application/x-mspowerpoint;application/wps-office.pptx;application/wps-office.potx;application/vnd.openxmlformats-officedocument.presentationml.presentation;application/vnd.openxmlformats-officedocument.presentationml.slideshow;application/wps-office.uop;application/wps-office.wps;application/wps-office.wpt;application/wps-office.wpso;application/wps-office.wpss;application/wps-office.doc;application/wps-office.dot;application/vnd.ms-word;application/msword;application/x-msword;application/msword-template;application/wps-office.docx;application/wps-office.dotx;application/rtf;application/vnd.ms-word.document.macroEnabled.12;application/vnd.openxmlformats-officedocument.wordprocessingml.document;x-scheme-handler/ksoqing;x-scheme-handler/ksowps;x-scheme-handler/ksowpp;x-scheme-handler/ksoet;x-scheme-handler/ksowpscloudsvr;x-scheme-handler/ksowebstartupwps;x-scheme-handler/ksowebstartupet;x-scheme-handler/ksowebstartupwpp;application/wps-office.uot;
 Name=WPS 2019
 Name[zh_CN]=WPS 2019
@@ -16,4 +17,4 @@ X-KDE-SubstituteUID=false
 X-KDE-Username=
 Icon=wps-office2019-kprometheus
-InitialPreference=3
+InitialPreference=99
 StartupWMClass=wpsoffice

然后在 ~/.config/mimeapps.list 中配置默认程序

[Default Applications]
application/vnd.openxmlformats-officedocument.wordprocessingml.document=wps-office-wrap.desktop
application/vnd.openxmlformats-officedocument.spreadsheetml.sheet=wps-office-wrap.desktop
application/vnd.openxmlformats-officedocument.presentationml.presentation=wps-office-wrap.desktop
application/vnd.ms-word=wps-office-wrap.desktop
application/vnd.ms-excel=wps-office-wrap.desktop
application/vnd.ms-powerpoint=wps-office-wrap.desktop

PS. 合并 WPS 的 MimeType 可用以下的 zsh 命令（需要 extendedglob 选项）

grep MimeType /usr/share/applications/wps-office-^pdf* | cut -d'=' -f2 | paste -sd ''

从零开始的 λ 演算

2021-04-18 00:00:00

这是我在看完 PyCon 2019 演讲「Lambda Calculus from the Ground Up」之后做的一个文字版，原视频在 https://youtu.be/pkCLMl0e_0k。另见官网中的介绍，这里提供一个翻译。

最近关于编程风格的指南层出不穷。但是如果我们把风格限制为只允许出现单参数的函数会发生什么呢？没有模组，没有类，没有控制流，没有数据结构，甚至连整数、正则表达式等内建类型都没有，只有函数。用这种风格能写出程序吗？令人惊讶的是，答案是肯定的。在这个教程中，你将学到如何从零开始在 Python 中推导 λ 演算。

你不会在这个教程中学到有实际用处的东西。没有打包，没有工具，没有库，没有部署，也没有神奇的 Python 编程技术。你也不会学到会被你用在实际项目上的东西。但是你将获得很多乐趣，将感到惊叹，并学习一些基础的计算机科学，这是你进一步探索函数式编程、类型理论、编程语言等话题的起点。

规则

如上介绍所说，我们只允许函数调用，或者参数替换这一种操作。以下列举一些不被允许的操作：

def f(x):
    return x + 1  # 不允许使用数字和运算符 +

def f(x, y):
    ...  # 只允许单个参数

以下是一些合法的操作，但是他们好像没什么意义：

def f(x):
    return x

def f(x):
    return x(x)

def f(x):
    def g(y):
        return x(y)
    return g

所以在这样的一个如此抽象的系统中，我们可以做些什么？

布尔值（18:27）

首先来构造布尔值和布尔运算。可以借用选择器的概念来构造布尔值。TRUE 选择两个值中的第一个，而 FALSE 选择第二个。注意这里的 TRUE 和 FALSE 并不是一个具体的值，而是一种行为。

def TRUE(x):
    return lambda y: x

def FALSE(x):
    return lambda y: y

>>> TRUE('5v')('gnd')
'5v'
>>> FALSE('5v')('gnd')
'gnd'

接下来是布尔运算 NOT, AND 和 OR。注意到 NOT 的参数应该是 TRUE 或者 FALSE，它们都是需要两个输入的函数（柯里化的）。然后根据 TRUE 和 FALSE 在两个值中的选择情况便可构造出 NOT。

def NOT(x):
    return x(FALSE)(TRUE)

对于 AND，在它的第一个参数为 TRUE 的时候，值就等于第二个参数；在第一个参数为 FALSE 的时候，值为 FALSE（也就是它的第一个参数）。OR 可以根据类似的思想写出：

def AND(x):
    return lambda y: x(y)(x)

def OR(x):
    return lambda y: x(x)(y)

布尔运算演示

>>> NOT(TRUE)
<function FALSE(x)>
>>> NOT(FALSE)
<function TRUE(x)>

>>> AND(TRUE)(TRUE)
<function TRUE(x)>
>>> AND(TRUE)(FALSE)
<function FALSE(x)>
>>> AND(FALSE)(TRUE)
<function FALSE(x)>
>>> AND(FALSE)(FALSE)
<function FALSE(x)>

>>> OR(TRUE)(TRUE)
<function TRUE(x)>
>>> OR(TRUE)(FALSE)
<function TRUE(x)>
>>> OR(FALSE)(TRUE)
<function TRUE(x)>
>>> OR(FALSE)(FALSE)
<function FALSE(x)>

数字（34:45）

因为我们能够做的只有函数调用，所以可以尝试用调用函数的次数表示数字，比如 TWO(f)(x) 的含义是以 x 为初始值，调用 f 两次：

ONE = lambda f: lambda x: f(x)
TWO = lambda f: lambda x: f(f(x))
THREE = lambda f: lambda x: f(f(f(x)))
FOUR = lambda f: lambda x: f(f(f(f(x))))

零表示为调用函数零次，即不调用函数：

ZERO = lambda f: lambda x: x

为了能够方便地展示我们的系统中的数字，在此写一个函数用来将系统中的数字转为 Python 中的一个 int。这个函数并不在 λ 演算系统中，只是为了方便地查看系统中的数字。

def toint(n):
    return n(lambda x: x + 1)(0)

>>> toint(THREE)
3

加法和乘法（50:02）

使用 Peano 公理的思想，先实现一个数字的后继。

SUCC = lambda n: lambda f: lambda x: f(n(f)(x))

在这个实现中，SUCC 的返回值是一个数（因为拥有 lambda f: lambda x: xxx 这样的「接口」），而这个返回的数是以 x 为初始值调用了 n 次函数 f（用 n(f)(x) 表示）后又多调用了 f 一次的结果，所以表示 n + 1。

>>> toint(SUCC(THREE))
4

有了 SUCC 就可以实现加法了。x + y 就是在 x 的基础上调用 y 次 SUCC。而数字的行为正好是调用某个函数多少次。

ADD = lambda x: lambda y: y(SUCC)(x)

乘法就是将「调用函数 f x 次」（即 x(f) 这个行为）重复 y 次：

MUL = lambda x: lambda y: lambda f: y(x(f))

从上面的定义可以看出乘法就是用函数的复合，即 MUL x y = y ∘ x。

加法和乘法的演示：

>>> toint(ADD(FOUR)(THREE))
7
>>> toint(MUL(FOUR)(THREE))
12

二元组（2:03:49）

为了实现减法，我们需要先实现二元组。

CONS(a)(b) 将会返回一个「选择器」，这个选择器根据给它的参数选择 a 和 b 中的一个。这里的函数名借用了 Lisp 中的名字。

CONS = lambda a: lambda b: (lambda s: s(a)(b))
CAR = lambda p: p(TRUE)
CDR = lambda p: p(FALSE)

>>> p = CONS(2)(3)
>>> CAR(p)
2
>>> CDR(p)
3

这里的 CONS 接受两个参数并构造了一个二元组，CAR 和 CDR 分别取二元组中的第一个和第二个值。

减法（2:12:15）

下面借助二元组来实现一个数的前驱。我们可以从 (0, 0) 开始增加，(1, 0), (2, 1) …… 二元组的第二个数是第一个数的前驱，而第一个数就是增加的次数。

T = lambda p: CONS(SUCC(CAR(p)))(CAR(p))

>>> a = FOUR(T)(CONS(ZERO)(ZERO))
>>> toint(CAR(a))
4
>>> toint(CDR(a))
3

上面的 a 是从 (0, 0) 开始执行了函数 T 4 次后的结果，它本身是一个二元组，第二个值就是 4 的前驱 3。于是实现前驱的方式为从 CONS(ZERO)(ZERO) 开始执行函数 T n 次，再取二元组的第二个值：

PRED = lambda n: CDR(n(T)(CONS(ZERO)(ZERO)))

>>> a = FOUR(THREE)
>>> toint(a)
81
>>> b = PRED(a)
>>> toint(b)
80

然后仿造加法构造减法：

SUB = lambda x: lambda y: y(PRED)(x)

>>> a = SUB(FOUR)(TWO)
>>> toint(a)
2

判断一个数是否为零（2:24:12）

由于 ZERO 的行为是直接返回第二个输入，所以下面的第二个括号中为 TRUE。而其它的数都会调用第一个输入，所以直接让这个输入返回 FALSE。

ISZERO = lambda n: n(lambda _: FALSE)(TRUE)

>>> ISZERO(ZERO)
<function TRUE(x)>
>>> ISZERO(ONE)
<function FALSE(x)>

递归（2:30:13）

我们已经有了 AND, SUCC, ADD, CONS, CAR 和 ISZERO 等等函数，现在我们要来挑战写出阶乘函数。阶乘在普通 Python 中的一种写法是

fact = lambda n: 1 if n == 0 else n * fact(n-1)

它只用了判断是否为零，乘法和减法三种操作。把它转化为 λ 演算中的形式，得到

FACT = lambda n: ISZERO(n) \
                 (ONE) \
                 (MUL(n)(FACT(PRED(n))))

但是这个实现有问题：

>>> FACT(THREE)
RecursionError: maximum recursion depth exceeded

惰性求值（2:34:40）

原因是 Python 函数不是惰性求值（lazy）的，递归发生在 ISZERO 判断之前。为了规避这个限制，我们实现以下的 lazy 版本

L_TRUE = lambda x: lambda y: x()
L_FALSE = lambda x: lambda y: y()
L_ISZERO = lambda n: n(lambda _: L_FALSE)(L_TRUE)

FACT = lambda n: L_ISZERO(n) \
                 (lambda: ONE) \
                 (lambda: MUL(n)(FACT(PRED(n))))

>>> a = FACT(THREE)
>>> toint(a)
6

避免引用自己（2:47:30）

目前还有一个问题，在 λ 演算中没有全局变量，没有把值「存储」在一个变量中的概念。而我们在 FACT 的定义中使用了 FACT 这个名字。

我们也用了 ISZERO 和 ONE 等等名字啊？

事实上这些名字不需要存储的概念。可以把所有出现了 ONE 的地方换成它的定义（相当于 :%s/\<ONE\>/(lambda f:lambda x:f(x))/g）而程序还是会正确运行。而不能换 FACT 的原因是它的定义本身就使用了 FACT 这个名字。

如何在实现 FACT 的时候不引用它自己的名字？为了方便先用 fact 函数来试验，我们不希望在下面的实现中出现 fact：

fact = lambda n: 1 if n == 0 else n * fact(n-1)
#                                     ^^^^ bad

一种方式是把 fact 作为参数传进去，但是这样还是用了 fact 这个名字，而且这个写法在 fact 还没定义的时候就使用了它。

fact = (lambda f: lambda n: 1 if n == 0 else n * f(n-1)) \
       (fact)
#       ^^^^ ?

解决方案是直接复制粘贴，而不是把自己的名字传进参数：

fact = (lambda f: lambda n: 1 if n == 0 else n * f(n-1)) \
       (lambda f: lambda n: 1 if n == 0 else n * f(n-1))

我们还需要修正一下 f 的调用方法（因为需要先传入 f 再传入 n）。下面是最终的结果：

fact = (lambda f: lambda n: 1 if n == 0 else n * f(f)(n-1)) \
       (lambda f: lambda n: 1 if n == 0 else n * f(f)(n-1))
#                                                ^^^^

>>> fact(4)
24

可以把 fact 直接换成它的定义：

>>> (lambda f: lambda n: 1 if n == 0 else n * f(f)(n-1)) \
... (lambda f: lambda n: 1 if n == 0 else n * f(f)(n-1))(4)
24

不动点（3:00:38）

以上的实现有一点不好，它把一个很长的括号重复了两次。我们也可以借助不动点实现 fact。

回到之前尝试实现 fact 的时候，

fact = (lambda f: lambda n: 1 if n == 0 else n * f(n-1))(fact)

如果把中间的部分抽出来

R = lambda f: lambda n: 1 if n == 0 else n * f(n-1)

那么 fact = R(fact)，即 fact 是 R 的一个不动点。如果有一个可以计算不动点的函数，就可以得到 fact 了。

假设这个函数存在，设它为 Y。那么有 Y(R) = R(Y(R))。变形：

Y(R) = (lambda x: R(x))(Y(R))

仿照上一节中的做法，把括号中的表达式复制一遍，再修正一下 x 的调用方法：

Y(R) = (lambda x: R(x))(lambda x: R(x))

Y(R) = (lambda x: R(x(x)))(lambda x: R(x(x)))

那么我们就得到了 Y

Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))

Y 组合子（3:13:20）

这里的 Y 就是著名的 Y 组合子（Y combinator）。但是

>>> R = lambda f: lambda n: 1 if n == 0 else n * f(n-1)
>>> fact = Y(R)
RecursionError: maximum recursion depth exceeded

要解决这个问题，可以把 x(x) 换成 lambda z: x(x)(z)，它可以延后 x 的求值。

Y = lambda f: (lambda x: f(lambda z: x(x)(z)))(lambda x: f(lambda z: x(x)(z)))

>>> R = lambda f: lambda n: 1 if n == 0 else n * f(n-1)
>>> fact = Y(R)
>>> fact(4)
24

把 Y 用在其它函数上：

>>> fib = Y(lambda f: lambda n: 1 if n <= 2 else f(n-1) + f(n-2))
>>> fib(10)
55

实现 FACT：

>>> FACT = Y(
...     lambda f: lambda n: L_ISZERO(n) \
...                         (lambda: ONE) \
...                         (lambda: MUL(n)(f(PRED(n))))
... )
>>> a = FACT(FOUR)
>>> toint(a)
24

本文中的代码已整理到 Gist 上。

补充

惰性求值一节中也可以使用另一种方法。参考 Y 组合子一节，用 lambda x: f(x) 代替 f，这样不需要新定义 lazy 版本的函数。因为万物皆是函数，所以不需要担心 f(x) 因为 f 不是函数而出错。

FACT = lambda n: ISZERO(n) \
                 (lambda x: ONE(x)) \
                 (lambda x: MUL(n)(FACT(PRED(n)))(x))

FACT = Y(
    lambda f: lambda n: ISZERO(n) \
                        (lambda x: ONE(x)) \
                        (lambda x: MUL(n)(f(PRED(n)))(x))
)

总结

这里推导的 λ 演算没有什么实际用途，没有谁会用这里的 λ 演算写一个现实中使用的程序；
但是 λ 演算的思想在函数式语言中随处可见，非函数式语言也都在慢慢吸收函数式语言中的一些的思想和概念；
λ 演算就像机器语言一样。现在绝大多数人都在写高级语言，但是高级语言在某种程度上是机器语言的抽象，了解一些机器语言或者汇编的知识有助于写出更好，效率更高的代码。类似地，了解 λ 演算对理解和运用函数式语言和其它语言中的函数式元素是很有益的。

从 Manjaro 迁移到 Arch Linux

2021-03-21 00:00:00

今天我把系统换成了 Arch Linux，用的是 Btrfs 文件系统，套上 LUKS 加密（加密包括 /boot）。由于我已经在虚拟机里面实验过整个过程，所以今天的安装过程非常顺利，一共只用了一两个小时。

2021-03-25 更新：增加了 redshift 无法使用 geoclue 一节
2021-04-18 更新：增加了将 ~/.cache 单独分为一个子卷一节

背景

前几天用 btrfs-convert 把我的 Manjaro 的文件系统换成了 Btrfs，然后继续开发我的 Btrfs 快照管理工具 dosnap。奇怪的是，在出错的时候（如 panic!）程序不会退出，而是直接卡住。这还不是最致命的，过了几秒钟我发现我的 polybar 不见了，然后发现我的家目录里少了一些东西，包括 ~/.config。还好我之前有做快照，可以直接用 rsync 恢复数据。但是在我的一个 Arch Linux 虚拟机中程序如果出错会正确退出。不知道是为什么，可能是 btrfs-convert 的什么 bug。然后就想到用 Arch 虚拟机也有很长时间了，于是打算直接把物理机也换到 Arch Linux 上来。

备份

可以使用 Btrfs 的 send/receive 功能进行备份。注意备份的移动硬盘也需要是 Btrfs 文件系统。先对各个子卷做只读快照，然后对每个快照进行 btrfs send：

sudo btrfs send /mnt/_snapshots/${SNAPSHOT_NAME?} | sudo btrfs receive ${EXTERNAL_DRIVE?}

然后再记录一下安装过的软件：

pacman -Qe >${EXTERNAL_DRIVE?}/pacman-qe

安装

启动 archiso，然后调整一下终端字体

setfont ter-v28b

Installation Guide

打开 installation guide，一直做到 Partition the disks 之前。

由于磁盘已经分区，所以不需要再分区了。直接上 LUKS 并格式化为 Btrfs。注意需要用 luks1，因为 GRUB 目前还不支持 LUKS2。

cryptsetup --type luks1 luksFormat /dev/nvme0n1p4
cryptsetup open /dev/nvme0n1p4 archlinux
mkfs.btrfs -L archlinux /dev/mapper/archlinux

然后创建子卷并挂载分区

mount /dev/mapper/archlinux /mnt
btrfs subv create /mnt/@
btrfs subv create /mnt/@home
btrfs subv create /mnt/@opt
btrfs subv create /mnt/@var
umount /mnt

opt='noatime,ssd,space_cache=v2,compress=zstd'
mount -o $opt,subvol=@ /dev/mapper/archlinux /mnt
mkdir /mnt/{efi,var,home,opt}
mount /dev/nvme0n1p1 /mnt/efi
mount -o $opt,subvol=@home /dev/mapper/archlinux /mnt/home
mount -o $opt,subvol=@opt /dev/mapper/archlinux /mnt/opt
mount -o $opt,subvol=@var /dev/mapper/archlinux /mnt/var

对 /var/log/journal 禁用 CoW：

mkdir -p /mnt/var/log/journal
chattr +C /mnt/var/log/journal

然后从 installation guide 的 Installation 一节开始继续一直做到结尾，记得要在 pacstrap 的时候加上 btrfs-progs。

额外的操作

安装到这里还需一些额外的操作。更改 /etc/mkinitcpio.conf 的 BINARIES，然后在 HOOKS 中的 filesystems 之前加入 encrypt：

BINARIES=(/usr/bin/btrfs)
HOOKS=(base udev autodetect modconf block encrypt filesystems keyboard fsck)

然后重新生成 initramfs

mkinitcpio -P

更改 /etc/default/grub 中的内核命令行，这里我还顺便打开了 cgroup v2。 PARTUUID 可以使用 blkid 命令查看。

GRUB_CMDLINE_LINUX_DEFAULT="loglevel=3 quiet systemd.unified_cgroup_hierarchy=1"
GRUB_CMDLINE_LINUX="cryptdevice=PARTUUID=xxx:archlinux"

同步家目录

新建用户，并从备份中用 rsync 把家目录同步回来：

# run as wang
rsync -a ${EXTERNAL_DRIVE?}/home-snap/wang/* ~
rsync -a ${EXTERNAL_DRIVE?}/home-snap/wang/.* ~

安装软件包

安装我自己常用的软件

cd ~/.dotfiles/weirane-dotfiles-deps
makepkg -si

用下面的命令查看有哪些之前安装过而不在本机上的包，然后选择要安装的包并安装。

comm -23 <(cut -d' ' -f1 ${EXTERNAL_DRIVE?}/pacman-qe | sort) \
         <(pacman -Qq | sort) | less

配置

下面进行一些增加安全性或者便携性的配置。

加密 swap

为防止关机后 swap 中残留明文的内存数据，需要将 swap 加密。我不需要 hibernation，所以参考 ArchWiki，将以下内容加入 /etc/crypttab：

swap  PARTUUID=xxx  /dev/urandom  swap,cipher=aes-xts-plain64,size=512

将原来 /etc/fstab 中 swap 的一行改为

/dev/mapper/swap        none            swap            defaults        0 0

Key in initramfs

可以在 initramfs 中放一个 LUKS key，这样在开机的时候就不需要输两次 LUKS 密码了。我一般将 key 放在 /etc 中。注意要调整 key file 和装有 key file 的 initramfs 的权限。

sudo dd bs=512 count=4 if=/dev/urandom of=/path/to/key
sudo cryptsetup luksAddKey /dev/nvme0n1p4 /path/to/key
chmod 000 /path/to/key
chmod -R g-rwx,o-rwx /boot

把 key 加入 /etc/mkinitcpio.conf 中的 FILES：

FILES=(/path/to/key)

改 /etc/default/grub 中的内核命令行，加入 cryptkey=rootfs:/path/to/key：

GRUB_CMDLINE_LINUX="cryptdevice=PARTUUID=xxx:archlinux cryptkey=rootfs:/path/to/key"

最后重新生成 initramfs 和 GRUB config

sudo mkinitcpio -P
sudo grub-mkconfig -o /boot/grub/grub.cfg

解决问题

xbacklight

进入图形界面后发现 polybar 中的亮度模块没有显示，xbacklight 命令没有输出。参考 ArchWiki 之后发现应该安装 xf86-video-intel 并将下面的配置写入 /etc/X11/xorg.conf.d/20-xbacklight.conf：

Section "Device"
    Identifier  "Intel Graphics"
    Driver      "intel"
    Option      "Backlight"  "intel_backlight"
EndSection

redshift 无法使用 geoclue

运行 redshift 有如下报错

Trying location provider `geoclue2'...
Using provider `geoclue2'.
Using method `randr'.
Waiting for initial location to become available...
Unable to start GeoClue client: GDBus.Error:org.freedesktop.DBus.Error.AccessDenied: 'redshift' disallowed, no agent for UID 1000.
Access to the current location was denied by GeoClue!
Make sure that location services are enabled and that Redshift is permitted
to use location services. See https://github.com/jonls/redshift#faq for more
information.
Unable to get location from provider.

查阅 ArchWiki，将以下内容写入 ~/.config/systemd/user/geoclue-agent.service

[Unit]
Description=redshift needs to get a (geo)clue

[Service]
ExecStart=/usr/lib/geoclue-2.0/demos/agent

[Install]
WantedBy=default.target

运行命令 systemctl --user enable --now geoclue-agent.service 之后就可以使用 redshift 了。

将 `~/.cache` 单独分为一个子卷

我现在对我的家目录每两小时进行快照，用了一段时间后发现每个快照都有至少 30 MB 的 exclusive data。比较后发现主要是 ~/.cache 中的数据，所以想把它单独分为一个子卷。

登出当前用户，并在 tty 登陆 root 用户。把 ~/.cache 这个目录空出来，并创建子卷

cd /home/wang
mv .cache .cache2
btrfs subv create /home/wang/.cache

然后把数据复制回来，再恢复权限。

cp -a --reflink .cache2/* .cache
chown wang:wang .cache
rm -r .cache2

分开 ~/.cache 之后每两小时快照的 exclusive data 基本上在 20 MB 之下，效果还可以。

总结

整个过程挺顺利的，现在应该只剩一些之前在 /etc 中的配置没来得及同步了。由于家目录是直接 rsync 过来的，所以所有的数据都还在，家目录中的程序的配置也没有丢失， firefox 等程序也不需要重新登录或者进行其它的配置。

Weirane修改