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 ⊥。由於這無限遞迴，它等價於⊥。