プログラミング言語の基礎概念

なんか読書会がもうすぐあって結構な人気らしい。行って覗いてみたい気もするが、すでに定員一杯らしいし、Haskell知らんし、そもそも勉強会読書会なるものについてける気もしないしちょっと無理だろう。

件の本は、オンライン演習は一通りやったけど、そういえば肝心の本本体はほとんど全く読んでなかった。

メタ定理を証明せよ。とか謎言葉が最初の方に書いてあって、さっさとあきらめたのであった。

そういうわけで再び挑戦のために読んでみることにする。coqで。

まずは第一章の導出システムで、ペアノ自然数の定義だ。

Inductive nat : Type :=
 | Z : nat
 | S : nat -> nat.

「ソフトウェアの基礎」に、そのまんまのものがあるし、そもそもCoqでnat型はあらかじめ用意されてるが気にしない。

最初の導出システムでは、和と積の二つだけを扱う。

1.1と1.2の和の形式と推論規則の定義

Inductive plusR : nat -> nat -> nat -> Prop :=
 | P_Zero : forall n, plusR Z n n
 | P_Succ : forall n1 n2 n, plusR n1 n2 n -> plusR (S n1) n2 (S n).

記法を本と同じものにする。(このへん、よく分かってない。)

Notation "x 'plus' y 'is' z" := (plusR x y z) (at level 50, y at level 49).

機能してるかチェック。

Check plusR Z Z Z. (* ===> Z plus Z is Z : Prop  *)
Check Z plus (S Z) is S Z.  (* ===> Z plus (S Z) is S Z : Prop *)
Check Z plus (S Z) is Z.  (* ===> Z plus (S Z) is Z : Prop  *)  

おーけー。0 plus 1 is 0 みたいな命題も書こうと思えば書ける。(証明/導出は出来ない)

続いてかけ算。

Reserved Notation "x 'times' y 'is' z" (at level 40).
Inductive timesR : nat -> nat -> nat -> Prop :=
 | T_Zero : forall n, Z times n is Z
 | T_Succ : forall n1 n2 n3 n4,
     n1 times n2 is n3 ->
     n2 plus n3 is n4  ->
     S n1 times n2 is n4
where "x 'times' y 'is' z" := (timesR x y z).

練習問題の1.2をやってみる。

Example ex1_2_1 : 
 S(S(S Z)) plus S Z is S(S(S(S Z))).
apply P_Succ.
apply P_Succ.
apply P_Succ.
apply P_Zero.
Show Proof. (* ===>  
(P_Succ (S (S Z)) (S Z) (S (S (S Z)))
   (P_Succ (S Z) (S Z) (S (S Z)) (P_Succ Z (S Z) (S Z) (P_Zero (S Z)))))
*)
Qed.

おー出来た。当たり前だ。

まあCoqのタクティックを使ったからと言って、別段導出が特に簡単になるわけではまったくないのが残念なところであるが。

T_Succとかちっとも変数みつけてくれないし。

Example ex1_2_3 :
  S(S(S Z)) times Z is Z.
Proof.
  apply T_Succ. (*===> Error: Unable to find an instance for the variable n3. *)

間違った変数をアサインしても、別にエラーにしてくれないし。

Example ex1_2_3 :
  S(S(S Z)) times Z is Z.
Proof.
  apply T_Succ with (S Z).
(*
2 subgoals, subgoal 1 (ID 25)
  
  ============================
   S (S Z) times Z is S Z   <===????
*)

Coqの証明オブジェクトをオンライン演習の

S(Z) times S(Z) is S(Z) by T-Succ {
  Z times S(Z) is Z by T-Zero {};
  S(Z) plus Z is S(Z) by P-Succ {
    Z plus Z is Z by P-Zero {}
  }
}

みたいなのにexport出来ないもんだろうか。HaskellやOCamlにexport出来るらしい(自分はやったことはないが)ので、出来なくはないと思うんだけど。