Four ways of implementing a backtrack search

This is a stub article.
By now I have known four ways of implementing a backtrack search.
1.Using a recursive function. This is the plain vanilla way, which I learnt from "Programming Abstractions in C".
2.Explicitly managing the stack.
3.Using "amb" to employ non-deterministic computation, and
4.Using streams. The SICP implements the "control" aspect in Prolog with streams.

央视又在愚民

我承认，这个标题没有意义，因为说央视在播送一样。我要指出，这一回，央视动用了大量资源，集中于一个问题进行误导和分散注意力的宣传。这次南方几省的自然灾害，应视为大自然对中国政府的一次警告，要求其全面重新审视中国的经济发展环境，以负责任的方式发展经济。央视为了避免中国人思考和追问这个问题，树立了“抗灾救灾的勇气”，“人们在灾害面前显示的团结友爱”等主题以转移注意力，并再次企图证明所有中国人都应该保持政治一致。
在当今的中国，宜人的环境已经成了一种稀缺资源，在富人对穷人的剥削新增了一种－环境剥削。富人的成产（工厂）、生活（汽车、航空旅行、室内电器）方式对环境的影响比穷人大出许多，而自然灾害给穷人带来更大的痛苦，这正是环境剥削。而央视的新闻宣传充满了激越的战天斗地的感情，几乎不见对受灾人民痛苦的关注。

我抵制2008奥运会开幕式

不管身边的怎么起哄，我是绝对不会看的。因为我讨厌张艺谋－他代表的是冷酷的独裁者和贪婪的资本主义。他搞的开幕式在我眼里就像春节联欢晚会一样－充斥着以华丽空洞的歌声媚上的宋祖英和以嘲讽底层人民为能事的欺下的赵本山。记得曾听到过官方“公开征集选拔开幕式导演”的（假）消息，以后很长时间没有任何动静，也不知道都有谁应征了，突然一天有消息说彩排进行到某个阶段了！这是才知道（但是没有惊奇）导演是张艺谋。人民就这样又被蒙了一回。

本blog是针对Dijkstra的书A discipline of programming的第3章The characterization of semantics的读书笔记。
第19页的PROPERTY 4，4'比较confusing at first。我们可以在逻辑上进一步分解本章中的概念：
Let s be a state of the system. Let P be a predicate. Denote the true value of P on state s by Ps (think it as "P applied on s"). Let = denotes logical equivalence. Define predicate "Q⇒R" as: (Q⇒R)s = Qs→Rs (→ being the logic implication operator). Define predicate "Q or R" as: (Q or R)s = Qs∨Rs (∨ being the logic or operator). Define "Q and R" correspondingly. Denote the final state reached by machine S starting on initial state i by S(i). By the definition of the weakest precondition wp(S, R)s = RS(s). Equipped these notations, a formal proof of Property 3 can be conducted, which aids understanding of this property.
Proof of (wp(S, Q) and wp(S, R)) = wp(S, Q and R):
(wp(S, Q) and wp(S, R))s = wp(S, Q)s ∧ wp(S, R)s = QS(s) ∧ RS(s)
and
wp(S, Q and R)s = (Q and R)S(s) = QS(s) ∧ RS(s)
hence they are equal.
In the same way, Property 4, or (wp(S, Q) or wp(S, R)) = wp(S, Q or R) can be proved. Then the question is why Property 4 is a one-way implication? The key is to realize that in the above proof, we assumed S(s) is a single state, since we only defined the true value of a predicate on a single state. This means all the arguments holds only for deterministic machine. To deal with nondeterministic machine, first let S(i) be the set of possible final states reached from initial state i. Then we must define PW, in which P is a predicate and W is a set of states. Because a nondeterministic machine from a initial state i may produce any one of its possible final states in S(i), in order for a predicate to be true, all the final states must statisfies it. Thus: PW = ∀s∈W, Ps. Based on this definition P(W1∪W2) = PW1 ∧ PW2 (Note on the left-hand side is the set union, but on the right is the logic and, instead of or!). Now let's see why we have one-way implication in Property 4:
Suppose S(s) = {s1, s2, ... sn}. On the left-hand side:
(wp(S, Q) or wp(S, R))s = wp(S, Q)s ∨ wp(S, R)s = QS(s) ∨ RS(s) = Q{s1, s2, ... sn} ∨ R{s1, s2, ... sn} = (Qs1 ∧ Qs2 ∧ ... ∧Qsn) ∨ (Rs1 ∧ Rs2 ∧ ... ∧Rsn)
On the right-hand side:
wp(S, Q or R)s = (Q or R)S(s) = (Q or R){s1, s2, ... sn} = (Q or R)s1 ∧ (Q or R)s2 ∧ ... ∧(Q or R)sn = (Qs1 ∨ Rs1) ∧ (Qs2 ∨ Rs2) ∧ ... ∧ (Qsn ∨ Rsn)
Using propositional logic, we know the left-hand side ⇒ the right-hand side but not the other way round.
Finally, note if all ∨s are replaced by ∧s on both sides, they become equal, due to commutativity and associativity of the ∧ operator, which mean property 3 still holds for nondeterministic machines.