2

game組み合わせゲームの誘導型を定義しようとしています。lessOrEq2 つのゲームが、greatOrEq、lessOrConfまたはであるかどうかを判断する比較方法が必要greatOrConfです。次に、2 つのゲームが両方とも である場合に等しいかどうかを確認できlessOrEqますgreatOrEq。

しかし、このチェックを行うための相互再帰的なメソッドを定義しようとすると、次のようになります。

エラー: の減少引数を推測できませんfix。

これは、再帰呼び出しごとにどちらか一方のゲームのサイズだけが減少するためだと思います (両方ではありません)。これをCoqにどのように示すことができますか?

これが私のコードです。失敗する部分は、 、 、 の相互再帰的gameCompareなinnerGCompare定義listGameCompareですgameListCompare。

Inductive game : Set :=
 | gameCons : gamelist -> gamelist -> game
with gamelist : Set :=
 | emptylist : gamelist
 | listCons : game -> gamelist -> gamelist.

Definition side :=
 game -> gamelist.

Definition leftSide (g : game) : gamelist :=
 match g with
  | gameCons gll glr => gll
 end.

Definition rightSide (g : game) : gamelist :=
 match g with
  | gameCons gll glr => glr
 end.

Inductive compare_quest : Set :=
 | lessOrEq : compare_quest
 | greatOrEq : compare_quest
 | lessOrConf : compare_quest
 | greatOrConf : compare_quest.

Definition g1side (c : compare_quest) : side :=
 match c with
  | lessOrEq => leftSide
  | greatOrEq => rightSide
  | lessOrConf => rightSide
  | greatOrConf => leftSide
 end.

Definition g2side (c : compare_quest) : side :=
 match c with 
  | lessOrEq => rightSide
  | greatOrEq => leftSide
  | lessOrConf => leftSide
  | greatOrConf => rightSide
 end.

Definition combiner :=
 Prop -> Prop -> Prop.

Definition compareCombiner (c : compare_quest) : combiner :=
 match c with
  | lessOrEq => and
  | greatOrEq => and
  | lessOrConf => or
  | greatOrConf => or
 end.

Definition nextCompare (c : compare_quest) : compare_quest :=
 match c with
  | lessOrEq => lessOrConf
  | greatOrEq => greatOrConf
  | lessOrConf => lessOrEq
  | greatOrConf => greatOrEq
 end.

Definition cbn_init (cbn : combiner) : Prop :=
 ~ (cbn False True).

Fixpoint gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
 innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2)
with innerGCompare (next_c : compare_quest) (cbn : combiner)
      (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
 cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s)
with listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
 match g1s with
  | emptylist => cbn_init cbn
  | listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2)
 end
with gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
 match g2s with
  | emptylist => cbn_init cbn
  | listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr)
 end.

Definition game_eq (g1 : game) (g2 : game) : Prop :=
 (gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).
4

2 に答える 2

3

この問題を解決するためにできることは、おそらくいくつかあります。あなたのコードが何をしようとしているのか本当に理解できなかったので、これから言及するよりも効率的な方法があるかもしれません。

できることの 1 つgameCompareは、関数の代わりに (おそらく相互に) 帰納的な関係として定義することです。あなたが Coq にどの程度精通しているかはわかりませんが、答えが大きくなりすぎるので詳しくは説明しませんが、 などの概念を定義する場合、帰納関係を使用すると、関数よりもはるかに柔軟性が高くなりますgameCompare。誘導関係を定義する方法の詳細については、Benjamin Pierce の著書Software Foundationsを参照してください。

このアプローチの欠点の 1 つは、帰納関係は関数とは異なり、実際には何も計算しないことです。これにより、使用が困難になる場合があります。特に、関数呼び出しを単純化できるように帰納命題を単純化することはできません。

問題に適用しやすい別のアプローチは、再帰呼び出しごとに減少する「時間」数値パラメーターを関数に追加することです。これにより、関数は自明に終了します。次に、それを機能させるには、十分に大きな「時間」パラメーターを使用して最初の呼び出しを行うことを確認する必要があります。これを行う方法の例を次に示します。

Fixpoint gameSize (g : game) : nat :=
  match g with
    | gameCons gl1 gl2 => 1 + gameListSize gl1 + gameListSize gl2
  end

with gameListSize (gl : gamelist) : nat :=
  match gl with
    | emptylist => 1
    | listCons g gl => 1 + gameSize g + gameListSize gl
  end.

Definition gameCompareTime (g1 g2 : game) : nat :=
  gameSize g1 + gameSize g2.

Fixpoint gameCompareAux (time : nat) (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
  match time with
    | O => True
    | S time =>
      compareCombiner c
                      (listGameCompare time
                                       (nextCompare c)
                                       (compareCombiner c)
                                       (g1side c g1)
                                       g2)
                      (gameListCompare time
                                       (nextCompare c)
                                       (compareCombiner c)
                                       g1
                                       (g2side c g2))
  end

with listGameCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
  match time with
    | 0 => True
    | S time =>
      match g1s with
        | emptylist => cbn_init cbn
        | listCons g1s_car g1s_cdr => cbn (gameCompareAux time c g1s_car g2) (listGameCompare time c cbn g1s_cdr g2)
      end
  end

with gameListCompare (time : nat) (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
  match time with
    | 0 => True
    | S time =>
      match g2s with
        | emptylist => cbn_init cbn
        | listCons g2s_car g2s_cdr => cbn (gameCompareAux time c g1 g2s_car) (gameListCompare time c cbn g1 g2s_cdr)
      end
  end.

Definition gameCompare c g1 g2 :=
  gameCompareAux (gameCompareTime g1 g2) c g1 g2.

Definition game_eq (g1 : game) (g2 : game) : Prop :=
 (gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).

このgameCompareTime関数は、両方のゲームのサイズの合計を計算します。これは、 の呼び出しツリーの深さの妥当な境界のようですgameCompareAux。をインライン化したことに注意してください。これinnerGCompareにより、境界の計算が少し簡単になるからです。時間が終了すると (つまり、パターン マッチングの 0 ブランチ)、任意の値 (Trueこの場合は ) を返します。これは、そのケースに到達する前に終了するのに十分な時間を関数に与えるためです。

このアプローチの利点は、実装が比較的簡単なことです。欠点は、何かを証明するには、終了時間を明示的に推論gameCompareする必要がgameCompareAuxあり、非常に面倒な場合があることです。

于 2013-06-25T17:52:57.383 に答える