“咬死了猎人的狗”可以是“（咬死了猎人）的狗”，一条狗；也可以是“咬死了（猎人的狗）”，一个事件。两种读法用的字完全相同，差别只在怎样分组。

程序里同样的事随处可见。 1 + 2 * 3 1 + 2 * 3 是 $\left(1+2\right)\times 3=9$ 还是 $1+\left(2\times 3\right)=7$？ if a then if b then x else y if a then if b then x else y 里的 else else 属于哪个 if if ？

一份规格写道：“ if if 的条件必须是布尔值，两个分支的类型相同。”读起来没什么问题，但它完全没有涉及下面的情况：

1. 如果条件恒为真，else 分支永远不会执行，那我们还检查 else 分支吗？
2. “类型相同”是字面上一样，还是可以自动转换？
3. 检查器拒绝一个程序时，能不能指出它违反的是哪一条？

再如“ f() + g() f() + g() 先算两边再相加”。如果 f f 和 g g 都会打印东西，先打印谁？（也就是说没规定求值顺序）

[附注] 不完整规格中的类型检查问题 按一套明确的类型规则回答前三个问题；求值顺序的影响见 [附注] 求值策略、归约策略与合流性 。

“所有测试都没通过”可以是“每个测试都失败了”，也可以是“并非所有测试都通过了”，后者只要有一个失败就成立。两种读法的差别在于“所有”和“没”哪个管着哪个。

把量词的作用范围明确写出来：前者是“对每个 $𝑥$，$𝑥$ 都没通过”，后者是“并非（对每个 $𝑥$，$𝑥$ 都通过）”。写出来之后，两句话长得就不一样了。

下面是贝里悖论（Berry paradox）的一个汉语版本。

考虑这个短语：“不能用少于二十个字来定义的最小正整数”。

汉字只有有限多个，少于二十个字的短语也只有有限多个，它们最多定义有限多个正整数。所以确实存在不能用少于二十个字定义的正整数，其中有一个最小的，记为 $𝑛$。可上面那个短语本身只有十八个字，它恰好定义了 $𝑛$。于是 $𝑛$ 能用少于二十个字定义，矛盾。

附：毕的二阶导 —— 迷惑的贝里悖论：20个汉字真的能表达所有自然数吗？

把思想写成精确符号、使推理能够逐步核对的愿望很老。17 世纪末，莱布尼茨（Leibniz）设想过一种“普遍文字”（characteristica universalis），以及配套的推理演算（calculus ratiocinator）：思想写成符号，推理变成计算，争论的双方只需说一句“我们来算一算”（Calculemus）。

两百年后，弗雷格（Frege）在 1879 年的《概念文字》（Begriffsschrift）里真的造出了这样一门语言，它是现代逻辑的起点之一。他在序言里说，日常语言的推理里，常有没被察觉的前提悄悄混进来；他想要的是一条没有缝隙的推理链，每一步都看得见用了什么。 [约定] 阅读约定 也采用了这种证明写法：每个隐含的前提都要摆到台面上。

莱布尼茨的梦想没有完全实现。20 世纪的哥德尔（Gödel）和图灵（Turing）证明了，有些问题原则上就不能靠“算一算”来裁决。在程序语言理论中， [定义] 一步归约 与 [定义] 类型与类型判断 用规则精确定义运行和类型， [推论] 类型安全 则从这些规则证明良类型程序不受阻，是这种可核对推理的一个小例子。

这里约定的树（tree）是由节点（node）和连接节点的边（edge）组成的有限结构，有一个指定的根（root）。除根以外，每个节点恰有一个父节点（parent）；从根沿父子方向走到任意节点的路径唯一，不会绕回原处。每个节点可以带一个符号作为标签。

• 一条边连接父节点与它的子节点（child），也叫“孩子”。同一父节点的孩子有顺序，因此这是有序树；例如 [定义] 项的集合 中条件、then 分支、else 分支的位置不能互换。
• 没有孩子的节点称为叶子（leaf）；至少有一个孩子的节点称为内部节点（internal node）。根也可能是叶子：只有一个节点的树就是如此。
• 从某个节点沿父子方向走一步或多步能到达的节点，叫它的后代（descendant）。以一个节点为根，连同它的所有后代和连接它们的边，构成一棵子树（subtree）。整棵树也算以原根为根的子树；排除它自己时，称为真子树。

例如表示 $\text{pred }\left(\text{succ }0\right)$ 的树有三个节点。根标着 $\text{pred}$，它的孩子标着 $\text{succ}$，后者的孩子标着 $0$。前两个是内部节点，$0$ 是叶子；以 $\text{succ}$ 为根的子树表示 $\text{succ }0$。这里“子节点”指一个节点，“子树”指从那个节点开始的整块结构。