依赖类型真好玩

这篇文章的话题是「依赖类型」。很多人,甚至是写过多年程序的人,可能都没有接触过这个概念。简单说,如果一个类型依赖于一个不是类型的东西,那它就是依赖类型。其实我本人是这个话题的门外汉,那我怎么想起来写这样的一篇文章了呢?因为我刚刚读完《The Little Typer》,感觉非常新奇有趣,所以想写一写。如果我能把这份乐趣分享给你,那我会很高兴的~ (^_^)

A Sane Introduction to Emacs

This post is about GNU Emacs. There are so many articles written for beginners, but I'm often dissatisfied and frustrated by their selection of materials. I believe, to use Emacs, you don't have to be a genius. Getting started with Emacs should be as easy as using Notepad!

我的 iGEM 2018

一个月前的今天,我应该还在和队友们肝 Wiki Freeze……虽然时间过去这么久 了,但是,还是想写一些东西。

况且许久不写文字的话,语言能力是会退化的(笑)。已经不知道多少次打开编 辑器、写了多少半成品,但因为组织不好内容而放弃了。以后还是要多写写呀。

slab 分配器

话说知识推理系列坑的时间有点久,所以感觉在此期间写点别的也不错……刚好 距离第一篇博文发布正好一周年,就写点简单的东西吧。(x)

推理知识(2) 何谓「知识」

读过上一篇文章后,读者有没有感觉到此类谜题的有趣之处呢?上期我们故意留了若干悬念,这期便是揭晓谜底的时候。对这些问题的深入考察将为建立理论带来好处。

脏孩子问题的进一步解释

首先我们敏锐地察觉到一些假设,正是有些假设太强,以至于显得不切实际,才让我们感觉这道题有难度。

  • 「孩子们都能理解别人说的话」:这是比较普通的假设。
  • 「孩子们都很聪明」:考察推理过程,这假设意味着如果甲知道某件事,另一个人乙知道「甲知道这件事」,那么乙也知道这件事。

此外,我们故意遗漏了一点(你发现了吗?),「孩子们都很诚实」,保证他们不会说谎。如果他们会说谎,显而易见我们找不出符合逻辑的解答。

此外,如果脸上有泥巴的孩子数 $k \geq 1$,那么父亲的宣告「至少一人脸上有泥巴」就似乎是无用的,果然如此吗?重新考察证明过程,我们发现父亲的宣告实际上提供了归纳基础。好的,这的确是个回答,但不够令人满意。那么有没有更「直观」的解释呢?

让我们回到问题本身。假如脏孩子数 $k = 2$,而且父亲不加宣告,此时他们会如何推理?

  1. 显然每个孩子都知道「至少有 1 个孩子脸上有泥」。
  2. 假设「我」是一个孩子,我的脸上可能有泥也可能没有泥。父亲第一次询问,我将回答不知道。而从别人的回答我将无法得到任何有用的信息!
  3. 父亲第二次询问,与第一次询问情形相同。这一过程将无限重复下去。
  4. 从而将孩子们将永远回答「不知道」。

可见,父亲的宣告是有用的。但是,假设父亲给每个孩子私下里透露「至少有一个孩子脸上有泥」,那么孩子将感到很奇怪,因为「我」已经知道这件事了。

现在我们再设想一个情景:$k = 2$,父亲在给孩子甲透露这个信息的时候,允许其他所有孩子窃听(每个孩子自己窃听自己的,并不知道别人也在窃听),现在重新考察这个场景。

  1. 每个孩子都知道「至少有 1 个孩子脸上有泥」,并且知道「其他所有人都知道至少 1 个孩子脸上有泥」。
  2. 假设孩子甲、乙脸上有泥。第一次询问,甲乙将回答不知道。此时甲知道乙知道至少有一人脸上有泥,而乙回答了不知道,甲于是推知「乙看到了至少一人脸上有泥」(否则乙将知道自己脸上有泥),而甲此时只看到一人脸上有泥,于是推知自己脸上有泥。乙的推理过程与甲相同。而脸上没有泥的丙也将获知「至少两人脸上有泥」,但至于自己脸上有没有泥还不知道。
  3. 第二次询问,甲乙回答有,脸上没泥的所有孩子回答不知道。
  4. 第三次询问,脸上没泥的孩子根据推理,将知道自己脸上没有泥。

注意我们的推理过程,对于脸上有泥的孩子来说,他们使用了一个「知识」:所有人知道至少一人脸上有泥。而这个知识在第一个假想场景中并不存在。

现在假设 $k = 3$,孩子们还是独自窃听,此时将发现无法找出脏孩子,我们需要更强的条件「所有人知道所有人知道至少一个人脸上有泥」。设甲乙丙脸上有泥,推理过程大致如下:

  1. 第一次询问:甲将推知至少有两人脸上有泥(甲已知「所有人知道至少一个人脸上有泥」,推理如 $k = 2$ 情形),他已经看到两人有泥,自己有没有还不知道。
  2. 第二次询问:甲乙丙仍然均回答不知道。此回合前,甲乙丙知道「至少两人脸上有泥」,而且甲知道乙丙知道「至少两人脸上有泥」,而乙却回答不知道,于是甲将推知至少三人脸上有泥。甲本人只看到两人,说明剩下那个人只能是自己了。

不难归纳得出,若 $k$ 个孩子要找出脏孩子,那么需要「所有人知道……所有人知道至少一人脸上有泥」中「所有人知道」出现 $k-1$ 次。假如要让 $k$ 任意大(一如上期所讲的脏孩子问题),那么这个「所有人知道」也需要出现无穷多次。

这意味着父亲的宣言非常特殊,他虽然只讲了一句话,但却给了所有人非常强大的知识。而且「宣言」这种行为本身也非常特殊,我们已经发现「私下告诉」和「私下告诉并且允许别人独立窃听」是无法达到宣言的效果的。提前剧透一下,我们把这种特殊的知识叫做公共知识。可见,「众所周知」其实是一件非常难做到的事情。这也给我们的脏孩子问题加了另一个隐含假设:父亲的宣告确实是有效的宣告,即成功地建立了公共知识。

何谓「知识」?

我们在考察脏孩子问题时一直在使用「知道」「知识」这两个词,但却是非严格地使用:尚未对这两词下一个定义。先看看词典怎么说。

汉语词典释义:

知识:人们在实践中获得的认识和经验。

维基百科对「knowledge」解释:

Knowledge is a familiarity, awareness, or understanding of someone or something, such as facts, information, descriptions, or skills, which is acquired through experience or education by perceiving, discovering, or learning.

这两个定义都强调了知识来自实践,但这与我们所要演算的对象没什么关系,毕竟我们在解决脏孩子问题时根本不在乎知识从哪儿来。要这么说就奇怪了,难道我们在滥用词语吗?某种程度上来说,确实如此。我们一直使用的「知识」实际上无非是「所知道的」的意思而已,那我们不妨就在我们的理论中如此定义「知识」一词?哦不,我们只是把问题推给了「知道」而已。话说回来,「知道」又是什么意思呢。

好吧好吧,我们放弃从「知识」和「知道」的原始意思中提炼定义的做法,而是从我们的问题的解答中提炼定义。不妨就把「知识」定义为:一个人所拥有的、可以作为推理依据的信息。「知道」就定义成:一个人拥有这个知识。虽然这个定义与我们日常使用的「知识」和「知道」差别很大,但又有足够相似,可以更轻松地在直觉上理解问题。

虽然上面给出的定义比词典上的定义更好(对我们的理论更有帮助),但是不够严格。下一讲我们将建立形式化的知识模型,从而给出严格定义。

思考题

虽然我们的问题和解法看着都不切实际,但还是希望能把这样的理论应用于实际中(哪怕不是直接应用于日常生活)。读者不妨思考, 在哪些别的领域中,这样的理论可能会有用? 在生活中,一群人之间如何建立公共知识?找出方法,并给出达成方法的各种前提条件。

推理知识(1) 从一道逻辑谜题说起

不知读者是否见过下面这个逻辑谜题?

一个家庭有 $n$ 个孩子。有一天这些孩子们出门玩,父亲叮嘱他们不要玩泥巴。但是这些孩子很淘气,还是去玩了泥巴,其中 $k$ ($1 \leq k \leq n$)个孩子弄脏了自己的脸。孩子们只能看到别人的脸,看不到自己的脸。回到家后,父亲对他们所有人同时说:「你们中至少有一个人的脸上有泥巴。」然后不断对他们所有人同时提问:「你们脸上有泥巴吗?」孩子们同时回答「有」「没有」或者「不知道」。假设这些孩子都非常聪明,他们的回答会是怎样的?

只有 41 字节的 A+B 程序

看到这样一段很短的完整 C 程序,可以输入两个个位数并算出和……长度只有 41 字节!其原理是?

从自输出程序到 Y 组合子

有一类程序可以打印出自己的源代码,这种程序叫做自输出程序,也叫做 Quine。本文将向你展示 Quine 和 Y 组合子之间的关系。

ownPaste

最近经常用 IRC,发送大段文本和图片就成了刚性需求,然而现有的公共 Pastebin 和图床在管理上不太方便:

  1. 我希望删除得越早越好,这些资料本身就是临时的,根本不必要长期存储。
  2. 我不希望被其他人看到。网上现有的服务通常有一个 Recent,很容易读到别人发的消息。

出于这两点考虑,我打算自制一个支持代码和文本的 Pastebin。这也是本文标题的由来,「ownPaste」意味着这是属于我一人的 pastebin,我对其有充分的控制权。