imunolionの日記

Coqでセンター試験のBasicを解く

2011年の定理証明Advent Calendarの記事です。
オトナの娯楽を目的にしていますので、

Basicの解説を目的にしていません!!
受験を控えてBasicわからんと言って、
Google先生に頼った数学II・B受験者はブラウザバックを推奨します。
コンピュータ科学に興味あったら受験終わったらここに戻ってくるといいよ!

2010年のセンター試験、数学II・Bの第6問です。
これをCoqをつかって証明してみようというお話です。

Nを与え、

を充足する自然数a,b,cのパターン数を求める問題。
aが取り得る範囲は[0, INT(N/3)]となることから、
この範囲からaを選んだとき、(b, c)のペアの数を求める。
ただし、INT(X)はXを越えない最大の自然数を求める関数。
選択するaが範囲を網羅したときペア数の和から、(a,b,c)のパターン数が分かる。

Nとaが与えられたとき、(b,c)のパターンを求める式は、

で与えることができる。

それでは本題。
以下のBASICプログラムが与えられたとき、
プログラム終了状態におけるXの値が答えになるわけだが、
その正しさはどのように証明を与えることができるだろうか。

100 INPUT N
110 LET X = 0
120 FOR A = 1 TO INT(N/3)
130 LET X = X + INT( (N-A)/2 ) - A + 1
140 NEXT A
150 PRINT X
160 END

このままBasicをCoq上で表現しようとすると、
色々問題が起きることは目に見えているため、
以下のような表現を考えてみる。

problem (N:nat) :=
  LINES ( LET_X 0 )(
    FOR_A(1)(INT3 N)(NEXT_X)
  )

なるほど、とても短いプログラム？ですね。
大体意味は朧げに見えてくるでしょうか？
NEXT_Xは"LET X = X + INT((N-A)/2) - A + 1"に対応しているとでも考えます。

じゃあ、これを構文として持てるような文法を考えてみよう。

Inductive statement:Type :=
| LET_X: nat -> statement
| NEXT_X: statement
| FOR_A: nat -> nat -> statement -> statement
| FOR_A2: statement -> statement
| LINES: statement -> statement -> statement
.

うーん、なんかぱっとしない。
AについてのFORループが2つに分かれていますね。
これは実は証明をちょとだけ簡単にするために、
FORループの初期化とループ中の操作的な意味論を区別するのに使います。

では少しずつこれに肉付けしていこうと思います。
まずは状態をどの様に定義するか、です。

Record State := mkState{
  n: nat;
  a: list nat;
  x: list nat;
  cond: bool (* 実はこれはFORには不要。whileやifを作るなら *)
}.

nはまぁ、自然数でいいんでしょうけれど、
aとかxがなぜかlistですねー。変なのー。
でもやっぱり最初はlist上で証明やった方がいいでしょう。
つまり、FORループの初期化でAのレンジをlistとして用意して、
ループに入るとそのlistから要素をひとつずつ消費していくイメージです。
Xのアップデートですが、差分項をlistの要素にしましょう。
だとするとこういう関数が必要になりそうですね。

Fixpoint INT3_inner (n:nat)(a:nat):nat :=
  match a with
    | O => O
    | S aa => if (ge_dec n (aa*3))
      then aa
      else INT3_inner n aa
  end.
Definition INT3 (n:nat): nat := INT3_inner n n.
Fixpoint INT2_inner (n:nat)(a:nat) :=
  match a with
    | O => O
    | S aa => if (ge_dec n (aa*2))
      then aa
      else INT2_inner n aa
  end.
Definition INT2 (n:nat): nat := INT2_inner n n.
Definition calc_bc (n a:nat):nat := INT2(n-a)-a+1.

Fixpoint from_inner(n m:nat):list nat :=
  match m with
    | O => nil
    | S _ =>
      match (m - n) with
        | O => nil
        | S ml =>
          match m with
            | O => nil
            | S mp => cons m (from_inner n mp)
          end
      end
  end.
Definition from (n m:nat):list nat := from_inner (n-1) m.
Fixpoint natsum (ls:list nat):nat :=
  match ls with
    | nil => 0
    | cons h t => h + natsum t
  end.

状態の生成はどんな感じでしょうか。

Definition fsem_LET_X (x:nat)(st:State):State :=
  mkState st.(n) st.(a) (cons x nil) st.(cond).
Definition fsem_LET_A (a:nat)(st:State):State :=
  mkState st.(n) (cons a nil) st.(x) st.(cond).
Definition fsem_FOR_A (start:nat)(ed:nat)(st:State):State :=
  mkState st.(n) (from start ed) st.(x) st.(cond).
Definition fsem_NEXT_X (st:State):State :=
  match st.(a) with
    | nil => mkState st.(n) st.(a) st.(x) st.(cond)
    | cons a0 b0 => mkState st.(n) b0 (cons (calc_bc st.(n) a0) st.(x)) st.(cond)
  end.

これらの補助関数を用いた意味論です。

Inductive sem: statement -> State -> State -> Prop :=
| s_LET_X :forall x st,
  sem (LET_X x) st (fsem_LET_X x st)
| s_NEXT_X: forall st,
  sem NEXT_X st (fsem_NEXT_X st)
| s_FOR_A:forall st ed s st1 st2 st3,
  st2 = fsem_FOR_A st ed st1 ->
  sem (FOR_A2 s) st2 st3 ->
  sem (FOR_A st ed s) st1 st3
| s_FOR_A2_CONS:forall s st1 st2 st3,
  st1.(a) <> nil ->
  sem s st1 st2 ->
  sem (FOR_A2 s) st2 st3 ->
  sem (FOR_A2 s) st1 st3
| s_FOR_A2_NIL:forall s st,
  st.(a) = nil ->
  sem (FOR_A2 s) st st
| s_LINES :forall s1 s2 st1 st2 st3,
  sem s1 st1 st2 ->
  sem s2 st2 st3 ->
  sem (LINES s1 s2) st1 st3
  .

よーし、証明やってみよう!
まずは実行結果のXのうち、差分listを表現しているst2.(x)を見てみましょう。
それぞれの要素がレンジを表すaの要素に対して、
INT( (N-A)/2 ) - A + 1を満すかどうか。

1 subgoal
  
  ============================
   forall st1 st2 : State,
   sem (FOR_A2 NEXT_X) st1 st2 ->
   natsum (x st2) = 
   natsum (x st1)
 + natsum (map (calc_bc (n st1)) (a st1))

さて、FORループがあるので帰納法を使うのが自然でしょう。
ですが何に対する帰納法にするのが妥当でしょうか？
ここでようやくaをlistで表現していることが意味をもってきます。
ループはlistであるaの要素が尽きるまで消費するのです。

2 subgoals
  
  st1 : State
  Heql : nil = a st1
  st2 : State
  H : sem (FOR_A2 NEXT_X) st1 st2
  ============================
   natsum (x st2) = 
natsum (x st1) + natsum (map (calc_bc (n st1)) nil)

Hに対してinversionすれば、

• st1.(a)が空でないとき
• 空のとき

についての証明になります。
前者は帰納法の前提に対して矛盾です。
後者はlistの和であるnatsumがOを返し、st1.(x) = st2.(x)が使えます。
これはループの終了条件であるs_FOR_A2_NILのおかげです。

さて、帰納法の後半戦に入りここからが勝負どころ。

  IHl : forall st1 : State,
        l = a st1 ->
        forall st2 : State,
        sem (FOR_A2 NEXT_X) st1 st2 ->
        natsum (x st2) =
        natsum (x st1)
     +  natsum (map (calc_bc (n st1)) l)
  ============================
   forall st1 : State,
   a0 :: l = a st1 ->
   forall st2 : State,
   sem (FOR_A2 NEXT_X) st1 st2 ->
   natsum (x st2) = 
   natsum (x st1)
 + natsum (map (calc_bc (n st1)) (a0 :: l))

見るからに辛そうですね。
とりあえず、a0::lとなっているところを、
a0とlに分解しないことにはIHlが適用できません。

  ============================
   natsum (x st2) =
   natsum (x st1)
 + natsum (calc_bc (n st1) a0 :: map (calc_bc (n st1)) l)

むむむ。
慣れている方、勘のいい方はこのあたりで気がつかれるはず。

   (natsum (x st1) + (calc_bc (n st1) a0))
 + natsum(map (calc_bc (n st1)) l)

加算の場所をnatsumのunfold/foldしてplus_assocすると、
何か前半が見覚えのある項になりませんか？
そうです、LET X = X + ...と同じことを意味しているのです。
つまり、FORループを1順外すことによって、
中間状態であるst3として見ると、
st3.(x) = (natsum (calc_bc (n st1) a0 :: x st3))!!
となれば、IHをst1ではなくst3で使用すればいいのです。
あとは丁寧に盛り付けをすれば、この証明は完了です。
この証明ができれば、本題はちょっと形式が違うだけの代物。

Theorem problem_correct: forall N st1 st2,
  sem (Problem3 N) st1 st2 ->
  natsum st2.(x) = natsum (map (calc_bc st1.(n))(from 1 (INT3 N)) ).

こっちは先程と何が違うのかというと、
Problem3となっているのは最初のBasicからつくったlispっぽいプログラム全体になる。
先程証明につかった、st1.(a)はループの初期化によって生成されたものになります。
inversionを適用して項を書き換えることによって先程の命題に帰着します。

まとめ

• Basicもどきのlispっぽい何かで書かれた命令型!プログラムをCoqで表現した
• おもちゃみたいなセマンティクスを与えているので証明できるよ
• 証明っていうけど、設問の本質の部分って証明してなくね？？

(まぁ、INT( (N-A)/2 ) - A + 1になることをちゃんと証明すればいいんでしょうけれど、あんまりおもしろくはなさそう。 )

課題

• Basicとか、サブセットすぎてタイトル詐欺だろ
• 行番号(状態にPCもたせる？)とGOTO文がBasicの本質だろJK
• 『第2回、第3回で考えて行きたいので命だけはお助けを』

Permalink | コメント(0) | トラックバック(0) | 23:31