付録アイデア。継続モナド

数独ソルバで継続モナドを使うと、肝はこれ：

「このマスに 1〜9 のどれを入れるか」という分岐点で、
失敗したら残りの候補を試すための“続き”を保存する。

普通に書くと再帰バックトラックだが、継続モナドで書くと「探索の制御」を抽象化できる。

まず普通のバックトラック

疑似コードはこう。

solve(board):
if 空マスがない:
return board
cell := 次の空マス
for n in 1..9:
if n を置ける:
board' := board に n を置いたもの
result := solve(board')
if result が成功:
return result
return failure

これは本質的に

候補を選ぶ
↓
先へ進む
↓
ダメなら戻る
↓
次の候補を選ぶ

という構造。

⸻

継続モナドで見る

継続モナドの型はだいたいこう。

Cont r a := (a → r) → r

これは

a を得たあとに何をするか

を引数に取る計算。

数独探索では、a は「候補として選んだ数字」、r は「最終的な探索結果」にする。

Cont (Option Board) Nat

なら、

Nat を選ぶ探索
最終的には Option Board を返す

という意味になる。

⸻

候補選択を Cont で表す

例えば、候補リストから一つ選ぶ関数をこう考える。

def choose (xs : List Nat) : Cont (Option Board) Nat :=
fun k =>
try each x in xs:
k x

ここで k が「x を選んだ後の残りの探索」。

つまり

k x

は、

x を置いたあと、残りのマスを解く

という継続。

もし k x が失敗したら、次の x を試す。

⸻

数独の探索本体

イメージはこう。

def solve (board : Board) : Cont (Option Board) Board := do
match findEmptyCell board with
| none =>
pure board
| some cell =>
let candidates := possibleNumbers board cell
let n ← choose candidates
let board' := place board cell n
solve board'

かなり普通のモナドコードに見える。

でも choose の中で、

失敗したら次の候補へ

という制御を持っている。

⸻

もう少し具体化する

Cont そのものより、数独では「失敗可能な継続」を使いたいので、結果型を固定する。

abbrev Search α := Cont (Option Board) α

choose はこういう意味になる。

def choose (xs : List α) : Search α :=
fun k =>
match xs with
| [] => none
| x :: xs =>
match k x with
| some answer => some answer
| none =>
choose xs k

ここが核心。

match k x with
| some answer => some answer
| none => try next candidate

つまり、

候補 x を選んで先に進む
成功したら即返す
失敗したら別候補

を choose に押し込めている。

⸻

数独ソルバの形

すると本体はかなりきれいになる。

def solve (b : Board) : Search Board := do
match findEmpty b with
| none =>
pure b
| some pos =>
let ns := candidates b pos
let n ← choose ns
let b' := put b pos n
solve b'

これだけ見ると、

空マスを探す
候補を選ぶ
置く
再帰する

だけ。

バックトラックの制御は choose 側に隠れている。

⸻

何が嬉しいのか

普通の再帰バックトラックだと、各所に

match solve b' with
| some ans => some ans
| none => continue

みたいな処理を書く。

継続モナドにすると、

let n ← choose ns

と書くだけで、

候補列挙
失敗時の巻き戻し
成功時の早期終了

をまとめて扱える。

⸻

ただし注意

数独を解くだけなら、継続モナドは必須ではない。

Lean なら普通に

Option
List
StateT
ExceptT

あたりで書く方がわかりやすいことも多い。

継続モナドが面白いのは、

「失敗したらここへ戻る」
「成功したら探索全体から脱出する」
「複数解を列挙する」
「途中状態を保存して再開する」

みたいな制御を、明示的にプログラム可能にするところ。

数独はその典型例。

No repository file or test is named. First locate the book's appendix or content structure and review how Lean examples are organized; done would be an agreed appendix covering the Sudoku backtracking example and its continuation-monad explanation.