這是一篇關於二分搜尋法(Binary Search)變體、Python 實作與正確性證明的技術文章。
二分搜尋法 (Binary Search):區間定義與正確性證明 二分搜尋法的核心難點在於邊界處理(Off-by-one error)。解決此問題的最佳理論工具是 迴圈不變量 (Loop Invariant)。
本文將針對三種場景:尋找特定值、尋找左側邊界 (bisect_left)、尋找右側邊界 (bisect_right),分別展示 左閉右閉 [L, R] 與 左閉右開 [L, R) 的實作,並證明其正確性。
1. 核心理論:迴圈不變量 (Loop Invariant) 在二分搜尋中,我們維護一個「搜尋區間」,並保證目標值(若存在)或目標插入點永遠位於該區間內。
初始化 (Initialization): 迴圈開始前,不變量成立。 維持 (Maintenance): 每次迭代縮小區間後,不變量依然成立。 終止 (Termination): 迴圈結束時,區間縮小至空或一點,此時的狀態即為答案。 時間複雜度證明 (Master Theorem): 遞迴關係式:$T(n) = T(n/2) + O(1)$ 根據主定理 (Master Theorem) Case 2 ($a=1, b=2, d=0$),複雜度為 $\Theta(\log n)$。
2. 尋找特定目標值 (Find Exact Target) 目標:若 nums 中存在 target,返回索引;否則返回 -1。
2.1 左閉右閉區間 [left, right] 定義: 搜尋區間為 $nums[left \dots right]$。 不變量: 若 $target$ 存在,則 $target \in nums[left \dots right]$。 終止條件: left > right (區間為空)。 def search_closed(nums: list[int], target: int) -> int: """Finds target in a sorted list using [L, R].""" left, right = 0, len(nums) - 1 while left <= right: mid = left + (right - left) // 2 # Prevent overflow if nums[mid] == target: return mid elif nums[mid] < target: left = mid + 1 # [mid+1, right] else: right = mid - 1 # [left, mid-1] return -1 2.2 左閉右開區間 [left, right) 定義: 搜尋區間為 $nums[left \dots right-1]$。 不變量: 若 $target$ 存在,則 $target \in nums[left \dots right-1]$。 終止條件: left == right (區間為空)。 def search_open(nums: list[int], target: int) -> int: """Finds target in a sorted list using [L, R).""" left, right = 0, len(nums) while left < right: mid = left + (right - left) // 2 if nums[mid] == target: return mid elif nums[mid] < target: left = mid + 1 # [mid+1, right) else: right = mid # [left, mid) return -1 3. 尋找左側邊界 (bisect_left) 目標:尋找第一個滿足 $nums[k] \ge target$ 的索引 $k$。等同於 C++ std::lower_bound。
...