《编程的修炼（中英双语）》章节试读

《编程的修炼（中英双语）》的笔记-第245页 - 第16章 再论归并

试着用这章的技巧求解 https://leetcode.com/problems/longest-substring-without-repeating-characters/ 这道题.
对于一个字符串s, 满足
R0: (A i, j: 0 ≤ i < s.dom, i < j ≤ s.dom, s(i) ≠ s(i+1) ≠ ... ≠ s(j - 1) and (s(i) = s(j) or s(i + 1) = s(j) or ... or s(j - 1) = s(j)))
那么, 我们把任意满足 R0 的i, j 作为 s 的索引, 得到的字符子串 s.slice(i, j) 称为 s 的不连续字符子串.
这个定义稍显冗长. 由于集合在数学上有元素不重复的特性, 让我们引入一个集合p.
令 p 为 s.slice(i, j) 中每个字符聚合后组成的集合, 根据不连续字符子串的定义, 我们可以得到一个蕴涵 R0 的等式:
P0: (A i, j, 0 ≤ i < s.dom, i ≤ j ＜ s.dom, p.dom = j - i).
由于题目要求的是最长的子串, 让我们再加上一个约束:
P1: (E m, m >= j - i)
由此, 我们得到了 P = P0 + P1 的约束, 即最长不连续字符子串长度问题的形式化定义.
P0 的定义, 让我们看到可以使用一个重复结构来解决它.
显而易见, 当
i = 0, j = 0, p = ∅
时, P 是成立的.
而 B(i, j): `i = s.dom or j = s.dom` 可以作为终止条件, 从而, 我们得到这样的程序结构:
i, j, m, p = 0, 0, 0, ∅
do i ≠ s.dom and j ≠ s.dom ->
"keep P invariant, and move step forward to non B(i, j)"
od
P1 的定义, 让我们看到可以使用一个选择结构来解决它.
显而易见, 当 m < j - i 时, P1 将不成立, 我们可以通过赋值语句 "m := j - i" 来让其成立.
即:
i, j, m, p = 0, 0, 0, ∅
do i ≠ s.dom and j ≠ s.dom ->
"keep P invariant, and move step forward to non B(i, j)"
if m < j - i -> m := j - i [] m ≥ j - i -> skip fi
od
print(m)
回到 P0 的不变性问题. 我们考虑以下几种可能的操作:
1. i, j := i, j + 1
2. i, j := i + 1, j
分开讨论两种情况.
1. i, j := i, j + 1 有可能使得 P0 不成立. 考虑它对应的指令序列:
"p:add(s(j)); j := j + 1;"
如果 s(j) 在 p 中不存在, 即 p(s(j)) = undefined, 那么 P0 左边执行 "p:add(s(j))" 后将使 p.dom 值域加1, 从而 P0 保持不变;
如果 s(j) 在 p 中已经存在, 即 p(s(j)) ≠ undefined, 那么, P0 左边将保持, 右边加1, 从而 P0 被破坏.
我们将不得不在指令外面加上一个 guard:
"if p(s(j)) = undefined -> p:add(s(j)); j := j + 1; fi"
2. i, j := i + 1, j, 必然可以使得 P0 成立, 因为 i 加上了 1, 所以 P0 等式的右边减小了1, 又因为 p 从 s.slice(i, j) 变为 s.slice(i+1, j), 所以 p.dom 也减少了 1. 这符合一个事实, 如果 s.slice(i, j) 是不连续字符子串, 那么 s.slice(i+1, j) 也必然是不连续字符子串. 我们可以根据这种情况得到一个指令序列:
"p:rem(s(i)); i := i + 1;"
由于 case1 有可能 abort, 我们需要为其补充剩下的可能性对应的操作.
case2 得到的指令序列由于没有更多约束, 我们可以将其作为剩下的所有可能的情况的操作.
从而, 我们得到了整个程序是:
i, j, m, p = 0, 0, 0, ∅
do i ≠ s.dom and j ≠ s.dom ->
if p(s(j)) = undefined -> p:add(s(j)); j := j + 1;
[] p(s(j)) ≠ undefined -> p:rem(s(i)); i := i + 1
fi;
if m < j - i -> m := j - i [] m ≥ j - i -> skip fi;
od
print(m)
以上两种情况的运行将必然导致 i, j 的增加, 从而外围的重复结构可以得到终止.
我们得到了一个解.
更多的优化还是有的, 例如, 如果有 s(j+1) 在 s.slice(i,j) 中的位置 k, 那么 i 可以更快的接近终点, 通过使用 "i := i + k".
然而我认为这里得到的解已经足够简明与清晰.
以上分析使用了`再论归并`一章提到的技巧:
从一个集合转移元素到另一个集合的同时, 保持不变性.

《编程的修炼（中英双语）》的笔记-第60页

Exercise: `prove wp("S1;S2", R) satisfied the property of monotonicity`:
From Q => R,
We have wp(S2, Q) => wp(S2, R),
then wp(S1, wp(S2, Q)) => wp(S1, wp(S2, R)).
Because wp("S1;S2", Q) = wp(S1, wp(S2, Q)), and wp("S1;S2", R) = wp(S1, wp(S2, R)),
We have wp("S1;S2", Q) => wp("S1;S2", R).
Property has been proved.

《编程的修炼（中英双语）》的笔记-第209页 - 线性检索定理

课后用书中提到的技巧推演了一下 `leetcode #1` 的题目.
### 题目
> Given an array of integers, find two numbers such that they add up to a specific target number. The function twoSum should return indices of the two numbers such that they add up to the target, where index1 must be less than index2. Please note that your returned answers (both index1 and index2) are not zero-based.
> **Input**: numbers={2, 7, 11, 15}, target=9
> **Output**: index1=1, index2=2
Or in jargon:
Giben an array of integers c, a specific number N, establish
R: (E I, J: 1 ≤ I < J ≤ c.dom : c(I) + c(J) = N)
### 一种解
P: (c i, j: 1 ≤ i < j ≤ c.dom)
B: c(i) + c(j) ≠ N
BB: (A i, j, c(i) + c(j) ≠ N)
non BB: (E i, j, c(i) + c(j) = N)
(i = 1 and j = 2) 蕴涵 P, 即 (i = 1 and j = 2) => P, 可作为初始语句.
又, P and non BB => R, 可知此处使用循环语句, 以 B 作为循环条件, 若循环能终止, 则循环可终止于 non BB 的状态, 而该状态又蕴涵最终结果, 题目可解:
i, j := 1, 2
do c(i) + c(j) ≠ N ->
{ 保证P的不变性, 并使循环递减接近终止条件: c(i) + c(j) = N}
od
print(i, j)
考虑语句"j := j + 1", 其最弱前条件
wp("j := j + 1", j ≤ c.dom) = (j + 1 ≤ c.dom) = (j ≤ c.dom - 1)
即: 使 "j := j + 1" 能安全运行的最弱前条件为 j ≤ c.dom - 1
我们就有了
i, j := 1, 2
do c(i) + c(j) ≠ N ->
if j ≤ c.dom - 1 -> j := j + 1 fi { 保证P的不变性, 并使循环递减接近终止条件: c(i) + c(j) = N}
od
print(i, j)
然而, 终止性此时不能得到保证, 因为这个选择结构有可能 abort(当 j = c.dom 时).
选取一个当前状态的单调递减的函数t, 采用 t = -i * c.dom-j. 为了保证 t 的单调递减, 当 j = c.dom 时, 我们需要开发出一句指令S, 使 S 执行后循环确切的导致了 t 的减小, 它的最弱前条件
wdec(S, t)
= (tmin ≤ t - 1)
= (tmin ≤ -i * c.dom - c.dom)
= (tmin ≤ -(i + 1) * c.dom)
tmin 为 t 的最终值的上确界.
我们从题目条件处可知, i < j, 我们有:
使 i + 1 < j 成立的 jmin 的值应为 i + 2,
故 tmin= -(i + 1) * c.dom - (i + 2), 从而, 指令S应为 "i, j := i + 1, i + 2"
完整的程序是:
i, j := 1, 2
do c(i) + c(j) ≠ N ->
if j ≤ c.dom - 1 -> j := j + 1 [] j = c.dom -> i, j := i + 1, i + 2 fi
od
print(i, j)
### 另一种解
我们已经形式化地推导得到了这个程序, 不用计算机运行也可以知道它的正确性.
然而在正确性之外, 这个程序的效率并没有得到最大化.
考虑这个例子, 看到的情况是, 对同一个 j 值可能频繁地计算 c(j) 与另一数之和, 并与 N 比较.
然而, N 值是给定的, 对于给定的 j, N - c(j) 也是恒定的.
这暗示我们引进一个变量, 对于 j 的谓词判定只计算一次. 例如 d, 使 N - c(j) 的结果存入变量标量中, 满足:
d(N - c(j)) = d(c(i)) = j.
于是我们有了一组新的不变式和谓词:
P: (E j, 1 ≤ j ≤ c.dom, d(N - c(j)) = j)
B: d(c(j)) = undefined
P and non BB => R
(j = 1
易得, 下面的语句
j := 1
do d(c(j)) = undefined -> { 保持P的不变性, 并使 j 递增, 靠近结果 d(c(j)) ≠ undefined } od
循环终止后, d(c(j)) = i, 即:
j := 1
do d(c(j)) = undefined -> { 保持P的不变性, 并使 j 递增, 靠近结果 d(c(j)) ≠ undefined } od
i := d(c(j))
print(i, j)
对于给定的j, 条件P告诉我们, 只需让 d(N - c(j)) = j 即可保持 P 的不变性, 而这可以通过修改数组来完成:
d:(N - c(j)) = j
而终止性理论又要求循环能不断接近最终结果, 选取一个单调递减的函数 t = n - j, 只要每次让 j := j + 1 可以满足.
综上, 我们得到了:
j := 1;
do d(c(j)) = undefined -> d:(N - c(j)) = j; j := j + 1 od;
i := d(c(j));
print(i, j);
这里使用了一个数组 d 来存储一些信息, 不过幸运的是, 在工程上, 编程语言通常给出了名如 HashMap, dict 等字眼的实现, 效率也是令人满意的.
### 总结
* 完满终止结构的设计, 一定要为终止性选择一个适当的证明, 并按此证明的假设来设计程序. 不同的判定谓词B与不变式P会推导出非常不一样的程序.
* t 的选择不重要, 只要找到一个`单调递减`的t 即可, 单调递减的t意味着每个卫式命令的选择都将导致 t 的有效减小, 从而向终点靠近.
* 完成了一个正确程序的开发并不意味着问题的终止, 正确性(数学上的修炼)与效率(工程上的修炼)是编程的两个关注点.
* 上面两种解, 在程序结构上被称为 `Linear Search Theorem`(Chapter 12, `A Discipline of Programing`), 是一种用于搜寻满足某个判断准则的最小值(他至少等于或大于某个下界)的简单技巧.

《编程的修炼（中英双语）》的笔记-第34页

Property 1. for any mechanism S, we have
wp(S, F) = F
Not so sure if I understand it.
I guess F is a fact that any state is dissatified post-condition.
So the entire property reduce that weakest pre-condition is going to be dissatisfied as well.
Assume this property is false, i.e wp(S, F) != F, we have at least one pre-condition satisfied wp(S, F).
But according to our assumption, this will not happened.
So this assumption is a contradiction, viz. property 1 is proved.