簡單的演算法證明操作技巧
我們想要證明下面的程式碼就是 \(y \to y+1\)
\begin{equation} inc = \begin{cases} 0 \to 1 \\ y \to 2 \cdot inc (\lfloor y/2 \rfloor) \quad (where \; y = 1 \pmod{2} ) \\ y \to y + 1 \end{cases} \end{equation}我的方法是根據每個情況分別證明
1. 簡單的部分
- \(y = 0\) 時 \(0 \to 1\) 這個情況可以直接得證
- 最後一個就是目標定義故得證
這兩個情況顯而易見
2. 遞迴部分
遞迴的部分比較複雜，首先我根據 \(y = 1 \pmod{2}\) 的特性知道
\[ y = 2m + 1 \]
- 所以 \(\lfloor y/2 \rfloor = \lfloor (2m+1)/2 \rfloor = \lfloor (m+0.5) \rfloor = m\)
- 接著因為 \(2 \times inc (\lfloor y/2 \rfloor) = 2 \times inc(m) = 2 \times (m+1) = 2m+2\)
最後回到 \(y = 2m+1\)，所以上式可以改寫成 \(y + 1\)，得證