Haskell/解决方案/语义学
| 练习 |
|---|
证明power2是严格的。虽然可以基于power2 n是 的“显而易见”的事实来证明，但最好使用不动点迭代来证明。 |
记住
power2 0 = 1 power2 n = 2 * power2 (n-1)
首先，我们需要考虑⊥ - 1是⊥还是不是。使用与⊥ + 1情况类似的推理，我们可以确定⊥ - 1确实是⊥。从那里，我们知道power2 ⊥是2 * power2 ⊥。由于这无限递归，它等价于⊥。
| 练习 |
|---|
证明power2是严格的。虽然可以基于power2 n是  的“显而易见”的事实来证明，但最好使用不动点迭代来证明。 |
记住
power2 0 = 1 power2 n = 2 * power2 (n-1)
首先，我们需要考虑⊥ - 1是⊥还是不是。使用与⊥ + 1情况类似的推理，我们可以确定⊥ - 1确实是⊥。从那里，我们知道power2 ⊥是2 * power2 ⊥。由于这无限递归，它等价于⊥。