如何形式化验证一场技术面试

完整代码可见https://github.com/KonjacSource/NQueens.

标题捏自https://aphyr.com/posts/342-typing-the-technical-interview, 这里有一篇中文翻译https://zhuanlan.zhihu.com/p/84634204, 不会写小作文, 所以只偷个名字😢.

本文意图展示一下如何确保正确性地编写一个程序, 我们会使用Agda, 在编写代码的同时证明代码的正确性.

题目是N皇后问题, 即, 如何在一个 n×n 的国际象棋棋盘上布置 n 个皇后使她们不能互相攻击.

我们建立一个模块(还是借用Haskell的高亮😢)

module NQueens (n : ℕ) where 

Agda允许模块具有参数, 这里参数 n 就代表棋盘的规模, 当其他人导入这个模块的时候就需要提供一个具体值.

我们可以用两个数表示一个棋子的位置

Pos : Set 
Pos = Fin n × Fin n

其中 Fin n 是一个具有 n 个元素的类型, 可以用它来表示一个大于等于 0, 小于 n 的自然数, 每个 Pos 由两个 Fin n 构成, 用来表示横纵坐标.

所以放置了 m 个棋子的棋盘的类型就是

Board : ℕ → Set 
Board m = Vec Pos m

现在我们考虑如何表达一个棋盘是安全的.

两个棋子是否在同行?

row : Pos → Pos → Set 
row (x₁ , y₁) (x₂ , y₂) = y₁ ≡ y₂

同列?

col : Pos → Pos → Set 
col (x₁ , y₁) (x₂ , y₂) = x₁ ≡ x₂

同斜线?

raise : ∀ {m} → Fin m → Fin (suc m)
raise zero = zero 
raise (suc x) = suc (raise x)

∣_-_∣ : ∀ {m} → Fin m → Fin m → Fin m
∣ zero  - zero  ∣ = zero
∣ zero  - suc n ∣ = suc n
∣ suc m - zero  ∣ = suc m
∣ suc m - suc n ∣ = raise ∣ m - n ∣

slash : Pos → Pos → Set 
slash (x , y) (x′ , y′) = ∣ x - x′ ∣ ≡ ∣ y - y′ ∣ 

同斜线就是判断两个棋子横纵坐标分别相减之后的绝对值是否相等.

把上面这些命题组合, 我们就得到了两个棋子不能互相吃到的命题,

safe : Pos → Pos → Set 
safe p q = ¬ (row p q) 
             × ¬ (col p q) 
             × ¬ (slash p q) 
           ⊎ p ≡ q -- 如果两棋子位置相同, 那么它们就是同一个棋子, 所以也应当被认为是安全的.

我们现在需要用到一个十分好用的类型 Dec, 它的定义如下,

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

Dec A 意味着 A 是一个可判定的命题, 一个 Dec A 的元素不仅要机械得判断 A 是否成立, 还要给出 A 成立或不成立的理由(就是一个A或¬ A的实例), 关于 Dec 更详细的介绍参见https://agda-zh.github.io/PLFA-zh/Decidable/.

现在我们要说, 对于任何两个位置 p q : Pos, safe p q 是可判定的,

-- 判定两个坐标是否相等
_≟ᵖ_ : (p q : Pos) → (Dec (p ≡ q))
_≟ᵖ_ = ≟-× _≟_ _≟_ 
  where 
    ≟-× : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′}
        → (eqA : (a b : A) → Dec (a ≡ b)) → (eqB : (a b : B) → Dec (a ≡ b)) 
        → (x y : A × B)
        → Dec (x ≡ y)
    ≟-× eqA eqB (xa , xb) (ya , yb) 
        with eqA xa ya
    ...    | no ¬a = no (λ {refl → ¬a refl})
    ...    | yes a 
          with eqB xb yb 
    ...      | no ¬b = no (λ {refl → ¬b refl})
    ...      | yes b = yes
                      (subst (λ s → (xa , xb) ≡ (s , yb)) a 
                    $ (subst (λ s → (xa , xb) ≡ (xa , s)) b refl))             
-- 判定是否同行
row? : (p q : Pos) → Dec (row p q)
row? (x₁ , y₁) (x₂ , y₂) = y₁ ≟ y₂
-- 判定是否同列
col? : (p q : Pos) → Dec (col p q)
col? (x₁ , y₁) (x₂ , y₂) = x₁ ≟ x₂
-- 判定是否同斜线
slash? : (p q : Pos) → Dec (slash p q)
slash? (x , y) (x′ , y′) = ∣ x -ᶠ x′ ∣ ≟ ∣ y -ᶠ y′ ∣ 
-- 判定是否安全
safe? : (p q : Pos) → Dec (safe p q)
safe? p q =     ¬? (row? p q)
          ×-dec ¬? (col? p q)
          ×-dec ¬? (slash? p q)
          ⊎-dec (p ≟ᵖ q)

现在我们可以来判断一个棋盘是否安全了,

allCombine : (n : ℕ) → Vec (Fin n × Fin n) (n * n) 
allCombine n = 
  Vec.concat $ 
    Vec.map (λ f → Vec.map (_, f) (Vec.allFin n)) (Vec.allFin n) 

-- 从棋盘上选两棋子做组合, 返回所有的取法
eachSafe : ∀ {n} → Board n → Vec (Σ Set Dec) (n * n)
eachSafe b = Vec.map 
  (λ {(i , j) → 
    ( safe  (lookup b i) (lookup b j) 
    , safe? (lookup b i) (lookup b j))}) 
  (allCombine _)

-- 对一个列表里的命题做合取
allProp : ∀ {n} → Vec Set n → Set
allProp [] = ⊤
allProp (x ∷ xs) = x × allProp xs

-- 整个棋盘是否安全?
AllSafe : ∀ {n} → Board n → Set 
AllSafe {n} b = allProp (Vec.map proj₁ (eachSafe b))

AllSafe 当然也是可判定的,

allProp? : ∀ {n} 
          → (vec : Vec (Σ Set Dec) n) 
          → Dec (allProp (Vec.map proj₁ vec))
allProp? [] = yes tt 
allProp? ((x , xd) ∷ xs) = xd ×-dec allProp? xs

AllSafe? : {n : ℕ} → (b : Board n) → Dec (AllSafe b)
AllSafe? {n} b = allProp? (eachSafe b)

如果一个棋盘是一个解, 那它不仅要满足AllSafe, 还要有恰好n个棋子在上面,

Solution : Board n → Set 
Solution = AllSafe

我们搜索答案的策略是一行一行地放置棋子, 我们保证在搜索过程棋子要保证顺序. 所以我们再来定义一个谓词, 用来检定一个棋盘是否是有序的,

OrderBoard : ∀ {m} → Board m → Set 
OrderBoard {m} [] = ⊤ 
OrderBoard {m} ((_ , row₁) ∷ rest) = suc (toℕ row₁) ≡ m × OrderBoard rest

OrderBoard? : ∀ {m} → (b : Board m) → Dec (OrderBoard b)
OrderBoard? {m} [] = yes tt
OrderBoard? {m} ((_ , row₁) ∷ rest) 
  with suc (toℕ row₁) ≟ⁿ m | OrderBoard? rest 
...  | yes a               | yes b = yes (a , b)
...  | _                   | no ¬b = no  (¬b ∘ proj₂)
...  | no ¬a               | _     = no  (¬a ∘ proj₁)

OrderSafe : ∀ {m} → Board m → Set 
OrderSafe board = AllSafe board × OrderBoard board

OrderSafe? : ∀ {m} → (b : Board m) → Dec (OrderSafe b)
OrderSafe? board = AllSafe? board ×-dec OrderBoard? board

然后我们再来定义一个Dec版本的filter, 它接受一个可判定的谓词f, 经他过滤之后的列表的每个元素都自动具有f要求的性质,

decFilter : ∀ {m} {A : Set} 
          → (f : A → Set) 
          → (∀ a → Dec (f a)) 
          → Vec A m → List (Σ A f) 
decFilter f f-dec [] = [] 
decFilter f f-dec (x ∷ xs) 
  with f-dec x 
...  | yes a = (x , a) ∷ decFilter f f-dec xs
...  | no ¬a = decFilter f f-dec xs

现在我们终于可以来搜索了,

putNext : {m : ℕ} 
        → m < n
        →      (Σ (Board      m ) OrderSafe) 
        → List (Σ (Board (suc m)) OrderSafe)
putNext {m} h (board , safe , order) = decFilter OrderSafe OrderSafe? newBoard
  where 
    newBoard : Vec (Board (suc m)) n
    newBoard = Vec.map 
        (λ x → (x , fromℕ< h) ∷ board)
        (Vec.allFin n)

这个函数接收一个棋盘, 然后返回所有安全的下一个棋子布置.

反复迭代我们就可以得到一个完整的搜索函数,

solve : ∀ m → suc m ≤ n → List (Σ (Board (suc m)) OrderSafe)
solve zero (s≤s h) = putNext {zero} (s≤s z≤n) ([] , tt , tt)
solve (suc m) (s≤s h) = List.concatMap (putNext (s≤s h)) (solve m (ℕₚ.m≤n⇒m≤1+n h))

然后执行这个函数,

solutions′ : List (Σ (Board n) AllSafe)
solutions′ = case inspect n of λ where 
  (zero with≡ _) → []
  (suc n′ with≡ h) → subst (λ n → List (Σ (Board n) AllSafe)) (sym h) 
    (List.map (λ {(b , s , _) → (b , s)}) 
              (solve n′ (subst (_≤ n) h ℕₚ.≤-refl)))

solutions : List (Σ (Board n) Solution)             
solutions = solutions′ 

solutions就是N皇后问题所有的解, 注意这里列表的元素不仅包含了棋盘, 还包含了这个棋盘是解的证明, 这就是正确性的体现.