FJを探してみる。 - Scala で TAPLを勉強しつつ LLVM コンパイラを作る日記

論文は見つかったのですけど、英語で難しい。
ってことで、実装ないんかと探してみると、実装の論文は見つかったんですけど、実装そのものは見つかりませんでした。

http://d.hatena.ne.jp/osiire/20090507

http://ocaml-nagoya.g.hatena.ne.jp/yoshihiro503/20091207/1260194719

ScalaBaseってイベントのUStreamを見ました。
FScalaってかんじの説明が面白かったというか、やっぱり難しいんだなと安心したというか、そんな感じでした。
Scalaの型チェックの停止性の証明をしたいんだけど、フルScalaの型チェックの停止性を証明するにはローカルの型推論があるんで、問題あるから、制限を付けてるって話らしいです。

あと、数学は結局、繰り返し練習が大切だって話だったので演習してみました。もう、眠くないし、苦手意識もどっかにいったので、嫌じゃないですからね。楽しく行きますよ。

TAPL 演習3.2.4

S(i)	= pow(	S(i-1)	,3)+	S(i-1)	3 + 3

ってかんじなので、

object q3_2_4 {
  def main(argv:Array[String]) {
    def sizeS(i:Int):Int = {
      i match {
        case 0 => 0 // s0は0
        // {true,false,0}で3
        // {succ t1,pred t1, izero t1| t1 ∈ Si} でsizeS(i)*3
        // {if t1 then t2 else t3 | t1,t2,t3 ∈ Si}でsizeS(i)の3乗
        case i => val n = sizeS(i-1); 3 + 3 * n + n * n * n
      }
    }
    println(sizeS(3))
  }
}

で、59439。

これは、無駄にCoqで計算。

Fixpoint sizeS(i : nat) : nat :=
  match i with
  | 0 => 0
  | S m => let n := sizeS(m) in 3 + 3 * n + n * n * n 
  end.
Eval compute in (sizeS(3)).

すばらしいぜCoq。iでマッチしてi-1とかではうまくかけなかった。ペアノ数恐るべしってことで、大分悩んだりしました。

演習3.2.5

もうね、証明なんて忘れてるので、長々書いてみますよ。

累積的である事を示せと。機能的に証明すれば良いんだよね。
S0は空集合φ。
S1は{true,false,0}だから、φ∪{true,false,0}でS1はS0∪S1の追加分になってる。
S2は{true,false,0}∪{succ true, pred true, izero true, succ false, pred false, izero false, succ 0, pred 0, izero 0}∪
{if ...}
で S2はS0∪S1の追加分∪S2の追加分になってる
S3はS0∪S1の追加分∪S2の追加分∪S3の追加分ってなっていっており累積的になってる。

って感じなのかなと思うけどこれだと永遠に終わらない。。。

答え見て見る。

機能的に証明するってことは、iが0のときとiが0より大きい時が示せれば良いんだよな。再帰関数作るみたいな感じだよね。

iが0のとき

機能的に証明する一番小さい所なので特にしょうめいすることはない。始まりだからね。

iが1より大きいとき

j<=0のときにj = i + 1だったら、Sj⊆Siと仮定する。
仮定してるんだから、まだ決まってないんでこの仮定を証明すれば良いんだよな。Si⊆Si+1が示せれば良いってことだ。

と、いうことはだ

任意の項 t ∈ Siについて、t∈Si+1が示せれば良いってことだ。
任意のって全部ってことだわな。Coqでいうとforallだよなたぶん。
∀t t∈ Si -> t ∈ Si+1の証明をすると。

∀をそういえば、TAPLでは使わないのかな。せっかく覚えたのに。ならばもならばだ。

仮にだ、t ∈ Siと仮定した場合にSiの定義が3つの集合の和集合だから、次の３つの事が示されると良い。

H1: t ∈ {true,false,0}の場合と
H2: t ∈ {succ t1,pred t1, izero t1| t1 ∈ Sj} の場合と
H3: t ∈ {if t1 then t2 else t3 | t1,t2,t3 ∈ Sj}の場合だ。

Coqだとこのへんがintrosでできそうな所なのかな。
で、Coqのcaseとかあの辺を使う感じだよな。
多少めんどくさいけど１個ずつ証明するぜ

H1: t ∈ {true,false,0}の場合は、
　Si+1の定義から明らかにSi ∈ Si+1だ。
　え？なんでかって？だってそうだろう。Si+1にも{true,false,0}が含まれてるんだから。Si+1の定義にも{true,false,0}が含まれているから、明らかにSi ∈ Si+1なんだ。わかったか？当たり前だろ。次いくぞ。

H2: t ∈ {succ t1,pred t1, izero t1| t1 ∈ Sj} の場合だな。
　tはSjだぞ。
　この場合は、Sj⊆Siって仮定してるから、t1 ∈ Si だ。そんでもって、Si+1は、定義から{succ t1,pred t1, izero t1| t1 ∈ Si+1}でってなってだな、tを含んでるので、t ∈ Si+1だぞと。
言う事だよ。

最後はH3: t ∈ {if t1 then t2 else t3 | t1,t2,t3 ∈ Sj}の場合だ。
これもH2と似たような話だけど、この場合も、Sj⊆Siって仮定してるから、t1 ∈ Si だよな。さらに、t2もt2 ∈ Siでt3もt3 ∈ Siってなると。この２つが余計にくっついてるのがH2との違いだな。でもって、H2と同じような話で、定義から{if t1 then t2 else t3 | t1,t2,t3 ∈ Si+1}で、tを含んでるので、t ∈ Si+1だ。

で、この３つが証明されたので、
任意の項 t ∈ Siについて、t∈Si+1が示せたし、iが0でも0より大きい場合でも証明出来たので、 Sj⊆Siの仮定は正しかった。そう俺は正しかったんだぜ。ということで、証明は終わりだ。Q.E.D.だってことだと。分かった？わかんねーよ。

なぜわかんないかっていうと、ごめん、数学的な帰納法の証明は昔やった覚えはあるんだけど、良く覚えてないんだっていう事に気がついた！！再帰的にしょうめいするのはわかるんだが、よくよく覚えてないので、なんか納得いかんのだよ。

ってことで、wikipediaを見るよ。

数学的帰納法の例

任意の自然数 n について、
1 + 2 + … + n = n(n + 1)/2

であることを数学的帰納法を用いて証明する。

って言う例がある。1+2+3+4+5+6+7+8+9+10...=っていうやつだね。どっかの偉い先生は答えがパッとでたけど、どうしてか説明はできなかったとかいうやつだ。
俺はこの証明の仕方を忘れてるので出来ない。でも高校だか、中学のころにそんなのやったっていうプライドだけはある。恥ずかしすぎる。
昔は出来たと思うけど、もう証明なんてしてないから忘れたんだよね。うん。３Dとかやるにしても、公式さえあればよかったんで。ああ、恥ずかしい。ってことで、

このために自然数 n に関する命題 P(n) を
1 + … + n = n(n + 1)/2 である
とする。

これは問題ないっすよね。

まず、P(1)、つまり
1 = 1 (1+1)/2
は右辺を直接計算することができ、正しいことが確かめられる。

最初の仮定はOKってことだな。

次に、任意の自然数 k をとる。今、P(k) が正しいと仮定すると P(k + 1) も正しい。実際、仮定P(k) より

1+...+k = k(1+k)/2
であるので、
1+...+k+(k+1) = (1+...+k)+(k+1)
= k(1+k)/2 + (k+1) = k(1+k)/2+2(1+k)/2
= (k+2)(1+k)/2 = (1+k)(2+k)/2
である。

仮定P(k)は正しいとP(k+1)も正しいということは、数学的帰納法に寄って証明された事になりますと。

では、Coqで証明してみましょう。
あれ、できない。。。
焦る。数時間過ぎ去る。ぐぐってようやく見つける。

Require Import Arith.

Fixpoint sum (n: nat) :=
  match n with
  | O => 0
  | S m => n + sum m
  end.

Theorem Sum_of_nat:
  forall (n: nat),  2 * sum n = n * (n + 1).
Proof.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  ring_simplify.
  rewrite IHn.
  ring.
Qed.

整数の帰納法はいろいろと面倒いらしいです。
ring_simplifyとかringとか知らないですよ。何それ。
ってかんじだったんですけど、とにかくこんな感じで書けると。

で、3.2.5をCoqで証明なんて出来るのかね。もういいよ。
って思ってしまったりして次回に続く