归约策略（reduction strategy）规定：当一个项的多个位置都能改写时，选择哪个位置、哪条规则作为下一步。求值策略（evaluation strategy）则规定一门语言怎样求得程序的结果，包括先算哪些子表达式、函数参数何时计算、是否计算函数体内部，以及算到什么形式就停止。文献有时混用这两个词；这里用前者强调“选归约路线”，用后者强调运行时的整体约定。能直接应用一条计算规则的子表达式，称为可归约式（redex，reducible expression）。

先看一个只含精确整数运算、没有副作用的例子。括号固定语法树；允许在任意子表达式里计算一次加、减、乘或整除时，下面的项至少有两条路线：

如果规定“先完整求出左操作数，再求右操作数，最后计算根”，求值器就选蓝色实线路线，右边虚线路线不属于这个受限制的一步关系。策略只限制何时用计算规则，不改它算出的数值。运算符优先级解决的是怎么解析字符串，不是这里的先后顺序：语法树已经由括号固定，两条路线没有重新分组，也没有把浮点加法当成可任意结合的运算。

真实语言里，JavaScript、Python 的普通函数调用会先求实参再执行函数体，通常称为按值调用（call-by-value）；JavaScript 还规定实参从左到右求值。Haskell 使用按需调用（call-by-need）：需要某个参数的值时才算，并共享这次计算的结果。例如 Haskell 的 const const 满足 const x y = x const x y = x ， error error 则用于产生错误； const 1 (error "boom") const 1 (error "boom") 返回 1 1 ，因为第二个参数不会被用到；JavaScript 的 ((x, y) => x)(1, (() => { throw new Error("boom"); })()) ((x, y) => x)(1, (() => { throw new Error("boom"); })()) 会先计算第二个实参而抛错。两门语言都可以有明确的策略，但选的是不同路线和停止条件。

有副作用时，连最后的普通数值也可能不同。设 JavaScript 中 let n = 0 let n = 0 ， f = () => ++n f = () => ++n ， g = () => n * 10 g = () => n * 10 。 f() + g() f() + g() 按从左到右求值给出 11 11 ；若另一门语言规定先算右边，先得到 g() = 0 g() = 0 ，再得到 f() = 1 f() = 1 ，结果就是 1 1 。所以“随便选一条路线”不是无害的实现细节； [例] 不完整的规格 里没写明的顺序必须在规格里补上。

多条路线能否重新汇合，是另一个性质，叫合流性（confluence）。这里临时把一般归约关系也记成 $⟶$，把零步或有限多步记成 ${⟶}^{\ast }$（正式定义见 [定义] 多步归约 ）：若 $𝑡{⟶}^{\ast }𝑢$ 且 $𝑡{⟶}^{\ast }𝑣$，总存在 $𝑤$，使 $𝑢{⟶}^{\ast }𝑤$ 且 $𝑣{⟶}^{\ast }𝑤$，就称这个关系合流。上图展示了一个可汇合的分叉；只画出这一个例子并没有证明整套关系合流。

合流不要求“下一步唯一”：$𝑢$、$𝑣$ 可以不同，只要求它们之后还可以到同一项。若某个项能到达两个范式（不能继续归约的项，正式定义见 [定义] 范式与受阻 ），合流保证这两个范式相同，因为范式已经无法再走向第三个不同的项。若没有合流保证，就不能从“各条路最后都停了”推出结果唯一：假想规则同时允许某个 $𝑡$ 归约到常量 $0$ 和 $1$，而两个常量都不能再归约，它们就永远无法汇合。选择策略可以挑出其中一个，却不消除原关系里的这种分歧。但合流不保证终止，也不保证任意策略都能找到已经存在的范式。

λ 演算（Lambda Calculus）是只用变量、函数和函数应用描述计算的形式系统。$𝜆𝑥.𝑀$ 表示参数为 $𝑥$、函数体为 $𝑀$ 的函数；$𝑀𝑁$ 表示把 $𝑀$ 应用到 $𝑁$。$𝜆$ 读作 lambda（“兰姆达”）。变量出现的位置若受某个 $𝜆$ 的参数绑定，称为绑定出现；否则称为自由出现。例如 $𝜆𝑥.𝑦$ 中参数 $𝑥$ 只规定绑定范围，函数体里的 $𝑦$ 是自由变量。一般的 β-归约（beta reduction，$𝛽$ 读作 beta）允许在任何子项中使用

$$\left(𝜆𝑥.𝑀\right)𝑁⟶𝑀\left[𝑁/𝑥\right]$$

其中 $𝑀\left[𝑁/𝑥\right]$ 是把 $𝑀$ 中自由出现的 $𝑥$ 替换成 $𝑁$，必要时先把绑定变量改名，以免把 $𝑁$ 的自由变量误捕获。β-归约也允许在函数体内部归约，不要求 $𝑁$ 已是值，所以通常有多条路线。Church–Rosser 定理说，一般 β-归约是合流的（把只差绑定变量名字的项视为同一个项）。这里引用这一经典结果而不展开其证明；它说明一般 β-归约虽然有多条路线，仍不会从同一个项得到两个不同的 β-范式。参见 Church–Rosser 定理。

例如 $\left(𝜆𝑥.𝑥\right)\left(\left(𝜆𝑦.𝑦\right)𝑧\right)$ 可以先归约外层，得到 $\left(𝜆𝑦.𝑦\right)𝑧$，也可以先归约实参，得到 $\left(𝜆𝑥.𝑥\right)𝑧$；两边都再归约到 $𝑧$。但令 $\mathrm{\Omega }=\left(𝜆𝑥.𝑥𝑥\right)\left(𝜆𝑥.𝑥𝑥\right)$（$\mathrm{\Omega }$ 读作 omega，“欧米伽”），它一步归约回自己，永远不会算完。$\left(𝜆𝑥.𝑧\right)\mathrm{\Omega }$ 若先算外层就得到范式 $𝑧$，若坚持先算实参就会在 $\mathrm{\Omega }$ 上无限归约。一般 β-归约仍然合流，却不能靠合流保证这条策略终止。

因而要分清三件事：确定性管每一步是否唯一，合流性管不同路线能否重新汇合，终止性（termination）管是否可能一直算下去。引入确定的归约策略可以把多路线关系限制成可由单后继函数实现的关系，但它不自动保持所有可达结果；要声称“最终结果不变”或“总能找到范式”，还需要相应的证明。 [定义] 一步归约 的十条求值规则已经规定了策略， [定理] 确定性 证明的正是这套规则的确定性。

Option<T> Option<T> 是 Rust 里表示“可能有值、可能没有”的类型，只有两种取值： Some(x) Some(x) 和 None None 。在返回 Option Option 的函数里，表达式 e? e? 的意思是：

• 如果 e e 是 Some(x) Some(x) ，整个 e? e? 的值就是 x x ，继续往下执行；
• 如果 e e 是 None None ，函数立刻返回 None None ，后面的代码不再执行。

在 Rust 求值器 step step 中， Succ(t1) Succ(t1) 匹配一个后继项， step(t1) step(t1) 返回 Option<Term> Option<Term> ，表示子项是否存在一步后继。这个分支可以写成两种等价形式：

// 用 ?
Succ(t1) => Some(Succ(Box::new(step(t1)?))),

// 不用 ?，展开写
Succ(t1) => match step(t1) {
    Some(t1_) => Some(Succ(Box::new(t1_))),
    None => return None,
},

// 用 ?
Succ(t1) => Some(Succ(Box::new(step(t1)?))),

// 不用 ?，展开写
Succ(t1) => match step(t1) {
    Some(t1_) => Some(Succ(Box::new(t1_))),
    None => return None,
},

例如，读取字符串的首字符，并把 ASCII 小写字母转成大写：

fn first_char_upper(s: &str) -> Option<char> {
    let c = s.chars().next()?;   // 空字符串时这里直接返回 None
    Some(c.to_ascii_uppercase())
}
assert_eq!(first_char_upper("rust"), Some('R'));
assert_eq!(first_char_upper(""), None);

fn first_char_upper(s: &str) -> Option<char> {
    let c = s.chars().next()?;   // 空字符串时这里直接返回 None
    Some(c.to_ascii_uppercase())
}
assert_eq!(first_char_upper("rust"), Some('R'));
assert_eq!(first_char_upper(""), None);

对照 [定义] 一步归约 中的同余规则：E-Succ 说“若 ${𝑡}_1⟶{𝑡}_{1^{\prime }}$，则 $\text{succ }{𝑡}_1⟶\text{ succ }{𝑡}_{1^{\prime }}$”。 step(t1)? step(t1)? 先去找 ${𝑡}_{1^{\prime }}$，找到了就拿来搭结论；找不到（前提不成立），结论就推不出来，整个函数返回 None None 。这正好是“子项不能归约，整个项也不能沿这条规则归约”。 类型检查器 type_of type_of 里的 type_of(t1)? type_of(t1)? 也是同样的意思：按照 [定义] 类型与类型判断 的规则，子项没有类型，就无法满足相应构造的定型前提，检查器返回 None None 。

Rust 求值器 step step 实现 [定义] 一步归约 的规则。Rust 的 match match 按顺序尝试分支，这本身是一种“优先级”，而求值规则没有写这种优先级。为什么这样写不会改变语义？因为 [定理] 确定性 的证明已经说明，对每个 $𝑡$ 至多一条规则适用，所以按什么顺序试结果都一样。没有那条定理，“先试 E-PredSucc 再试 E-Pred”就是一个偷偷加进来的、规则里没有的决定。