编程练习解答与技术分析

### 编程练习解答与技术分析 #### 1. 条件表达式求值相关证明 在条件表达式求值的证明中，有几种不同的情况需要考虑。 - **Case E - If**：对于表达式 `if t1 then t2 else t3`，若 `t1 -→ t′1`，根据归纳假设，要么 `t′1 -→ ∗true` 且 `t2 -→ ∗v`，要么 `t′1 -→ ∗false` 且 `t3 -→ ∗v`。将 `t1 -→ t′1` 这一步添加到 `t′1 -→ ∗true` 或 `t′1 -→ ∗false` 的推导中，就能得到所需结果，且得到的求值序列比原序列更短。 - **Case E - IfTrue**：`if true then t2 else t2 -→ t2 -→ ∗v`，此情况直接可得结果。 - **Case E - IfFalse**：`if false then t2 else t2 -→ t3 -→ ∗v`，同样直接可得结果。 命题“如果 `t -→ ∗v` 那么 `t ⇓v`”的证明，通过对小步求值步骤数进行归纳。若 `t -→ ∗v` 为 0 步，则 `t = v`，根据 B - Value 可得结果；否则，对 `t` 的形式进行情况分析。当 `t = if t1 then t2 else t3` 时，根据引理，要么 `t1 -→ ∗true` 且 `t2 -→ ∗v`，要么 `t1 -→ ∗false` 且 `t3 -→ ∗v`。假设是前一种情况，由于 `t1 -→ ∗true` 和 `t2 -→ ∗v` 的求值序列比 `t` 的短，归纳假设适用，可得 `t1 ⇓true` 和 `t2 ⇓v`，再用规则 B - IfTrue 可推出 `t ⇓v`。其他项构造器的情况类似。 #### 2. 递归函数 `eval` 的问题与改进 原 `eval` 函数每次调用自身时会在调用栈中添加一个 `try` 处理程序，由于每次求值步骤都有一次递归调用，栈最终会溢出。因为将对 `eval` 的递归调用包装在 `try` 中，它并非尾调用。改进后的 `eval` 函数如下： ```ocaml let rec eval t = let t’opt = try Some(eval1 t) with NoRuleApplies -> None in match t’opt with | Some(t’) -> eval t’ | None -> t ``` #### 3. 一些函数的定义 - **逻辑运算函数** - `or = λb. λc. b tru c;` - `not = λb. b fls tru;` - **自然数相关函数** - `scc2 = λn. λs. λz. n s (s z);` - `times2 = λm. λn. λs. λz. m (n s) z;` 更紧凑的形式为 `times3 = λm. λn. λs. m (n s);` - `power1 = λm. λn. m (times n) c1;` 或 `power2 = λm. λn. m n;` - `subtract1 = λm. λn. n prd m;` - `equal = λm. λn. and (iszro (m prd n)) (iszro (n prd m));` - **列表相关函数** - 一种定义方式： ```ocaml nil = λc. λn. n; cons = λh. λt. λc. λn. c h (t c n); head = λl. l (λh.λt.h) fls; tail = λl. fst (l (λx. λp. pair (snd p) (cons x (snd p))) (pair nil nil)); isnil = λl. l (λh.λt.fls) tru; ``` - 另一种定义方式： ```ocaml nil = pair tru tru; cons = λh. λt. pair fls (pair h t); head = λz. fst (snd z); tail = λz. snd (snd z); isnil = fst; ``` #### 4. 阶乘函数的实现 为防止阶乘函数发散，使用 `if` 而非 `test`，若使用 `test` 则需用虚拟的 lambda 抽象保护两个分支。实现如下： ```ocaml ff = λf. λn. test (iszro n) (λx. c1) (λx. (times n (f (prd n)))) c0; factorial = fix ff; equal c6 (factorial c3); ``` #### 5. 丘奇数转换函数 ```ocaml cn = λf. λm. if iszero m then c0 else scc (f (pred m)); churchnat = fix cn; equal (churchnat 4) c4; ``` #### 6. 列表求和函数 ```ocaml ff = λf. λl. test (isnil l) (λx. c0) (λx. (plus (head l) (f (tail l)))) c0; sumlist = fix ff; l = cons c2 (cons c3 (cons c4 nil)); equal (sumlist l) c9; sumlist’ = λl. l plus c0; equal (sumlist l) c9; ``` #### 7. 变量自由出现次数与项大小关系的证明 通过对 `t` 的大小进行归纳来证明。有三种情况： - 当 `t = x` 时，`|FV(t)| = |{x}| = 1 = size(t)`，直接可得。 - 当 `t = λx.t1` 时，由归纳假设 `|FV(t1)| ≤ size(t1)`，计算可得 `|FV(t)| = |FV