無限反復を含むパズル/ゲームをCoqで定義する

Coq、もっと言えば数学的にパズルやゲーム等を扱う上で無限反復の難しさがあります。

Coqでは再帰関数として停止性が明らかなものしか認められないという制限があるためです。¹

しかし一方で現実で扱う問題には無限反復は日常的にあります。

迷路では通ったところを繰り返しぐるぐる回ればいくらでも続けることができ、

囲碁では３コウといって、反復が続いて抜けられないので無勝負となる場合があります。

このような状況では数学は無力なのでしょうか。

サンプル問題：迷路

サンプル問題として迷路を考えます。

このように2をスタート、0をゴールする一直線上の迷路問題です。
一度の移動で右または左に1動くことができる、とします。

皆さんは解けますか？

ナイーブな再帰関数定義

自分の状態（位置）を自然数nとし、左右への移動を定義します。

Definition go_right (n : nat) := S n.
Definition go_left  (n : nat) := pred n.

このとき、この迷路を解く（解けるならtrueを返す）プログラムは以下のように書けます。

Fixpoint maze (n : nat) : bool :=
  match n with
  | 0 => true
  | _ => maze (go_right n) || maze (go_left n)
  end.

Compute maze 2.

しかし！残念ながらCoqはこの関数を受理しません。

Recursive definition of maze is ill-formed.

この関数は停止性の根拠がなく、実際、計算順が左からならばn = 2でも停止しません。²

解決法１：帰納的にゴール到達可能状態を定義

解決方法の一つは、後退解析の考え方に基づく方法です。
ゴールの状態を始点とし、ゴール到達一歩前、二歩前、…のように順繰りに全てのゴール到達可能な状態をカバーしていきます。

Inductive goal_reachable : nat -> Prop :=
  | OnGoal : goal_reachable 0
  | RightToGoal (n : nat) (H : goal_reachable (go_right n)) : goal_reachable n
  | LeftToGoal (n : nat) (H : goal_reachable (go_left n)) : goal_reachable n.

すると2がゴール到達可能であることを「左がゴール到達可能なら到達可能」ルールの適用で証明できます。

Example goal_reachable_2 : goal_reachable 2.
Proof.
  apply LeftToGoal.
  simpl.
  apply LeftToGoal.
  simpl.
  apply OnGoal.
Qed.

一方で、後退解析を用いることは、「最初にスタートにいる」というパズル/ゲームの自然な定義から離れてしまう感じもします。

解決法2:深度制限付き再帰関数の極限値で定義

そこで再帰関数での定義を再度試みます。

Fixpoint maze (d n : nat) : bool :=
  match n with
  | 0 => true
  | _ =>
    match d with
    | 0 => false
    | S d' => maze d' (go_right n) || maze d' (go_left n)
    end
  end.

停止性を明示するために、再帰の最大深さdを設定しました。

Compute maze 0 2.
Compute maze 1 2.
Compute maze 2 2.

     = false
     : bool
     = false
     : bool
     = true
     : bool

深さ2あればゴールに到達できることがわかります。
一方でこの2は結果的にわかった値であり、予め知ることはできません。

そこで、逆に「ゴール到達可能」の定義を変える方法があります。

Definition goal_reachable' (n : nat) :=
  exists m : nat, forall d : nat, m <= d -> maze d n = true.

「あるmがあって、全てのdについてm <= dなら制限深さdでゴール到達可能」

これは、「制限深さが無い」を「制限深さが無限」と読み換えて、ε-N論法により極限値を定義したことになります。³

ゴール到達可能の証明も行えて、この新しい定義を人間側が受け入れるならこれでもOK、といえます。

Require Import Bool.

Example goal_reachable'_2 : goal_reachable' 2.
Proof.
  exists 2.
  intros d H.
  induction d.
  - inversion H.
  - destruct d.
    + inversion H.
      inversion H1.
    + simpl.
      apply orb_true_iff.
      right.
      apply orb_true_iff.
      right.
      destruct d.
      * simpl.
        reflexivity.
      * simpl.
        reflexivity.
Qed.

おわりに

無限をどう扱うにしても何かしらのしこりは残るのですが、一方で無限を気にせず生活できる人間というのは数学を超えた高度な存在なのか、それとも定義に失敗した存在なのでしょうか。

1. FunctionやProgram Fixpointで停止性の証明付きで再帰関数を書けますが、停止しない可能性がある関数は書けません。 ↩

2. 2から3への移動を禁じても、1と2の間を往復し続けるでしょう。 ↩

3. Wikipedia 「イプシロン-デルタ論法」より「数列の収束」の項参照。　https://ja.wikipedia.org/wiki/%E3%82%A4%E3%83%97%E3%82%B7%E3%83%AD%E3%83%B3-%E3%83%87%E3%83%AB%E3%82%BF%E8%AB%96%E6%B3%95 ↩