Coq で遊ぶその4: Coq の変なところ色々。簡約。宣言と定義。型。

Coq in a Hurry ではこの後 Inductive Types の話になりますが、難しすぎてついてゆけないのでInteractive Theorem Proving and Program Development (Coq'Art) isbn:3540208542でゆきます。この本は重くて固くて取っ付きにくいですが、基本的な事から順番に書いてあるので、他のチュートリアルより内容は簡単です。今日は証明から離れてプログラミング言語としての Coq の側面を見てゆきます。

評価(簡約)の変なところ

Coq はプログラム実行環境ではなく、プログラム開発を支援する為の設計環境としてデザインされています。だから変な所が沢山あります。たとえばたかが 3 + 4 を計算するのに、

Coq < Check 3 + 4.
3 + 4
     : nat

としても駄目で、

Coq < Eval cbv delta iota beta in 3 + 4.
     = 7
     : nat

のように何やら呪文めいたコマンドが必要になってきます。「計算する」というのは、ある式をルールに従って書き換えて行く事です。しかし Coq の目的はプログラムを実行するのでは無く、開発を助ける事なので、おせっかいを焼いて勝手に書き換える事はしません。その代わり細かく書き換え方法を指定出来るようになっているのです。

Eval コマンドは簡約ルールという物を使って式を書き換えられるだけどんどん書き換えて行きます。また、複数のルールがある時は書き換えの順番が問題になりますが、cbv (call by value - 引数を先) か、lazy (外から先)を選べるようになっています。

delta(δ) 簡約

delta 簡約は変数名を値で置き換えます。

Coq < Definition three := 3.
three is defined

Coq < Eval cbv delta in three.
     = 3
     : nat

beta (β) 簡約

beta 簡約は関数適用をします。例えば f(x) = x + 4 のような関数があった時に、f(3) を beta 簡約すると 3 + 4 になります。

Coq < Eval cbv beta in (fun x:nat => x + 4) 3.
     = 3 + 4
     : nat

zeta (ζ) 簡約

zeta 簡約はローカル変数を書き換えて let 文を簡約します。

Coq < Eval cbv zeta in let x := 3 in x + 4.
     = 3 + 4
     : nat

iota (ι) 簡約

iota 簡約はその他凄い事をするらしいです。よくわかりませんが、足し算とかする時には必要になります。3 + 4 がそれぞれのルールでどのように簡約されて行くのかを実験してみます。

Coq < Eval cbv delta in 3 + 4 (* delta 簡約で + の定義を置き換える *).
     = (fix plus (n m : nat) {struct n} : nat :=
          match n with
          | 0 => m
          | S p => S (p + m)
          end) 3 4
     : nat

Coq < Eval cbv delta iota in 3 + 4 (* iota 簡約をしてみる *).
     = (fun n m : nat =>
        match n with
        | 0 => m
        | S p =>
            S
              ((fix plus (n0 m0 : nat) {struct n0} : nat :=
                  match n0 with
                  | 0 => m0
                  | S p0 => S (p0 + m0)
                  end) p m)
        end) 3 4
     : nat

Coq < Eval cbv delta iota beta in 3 + 4 (* 関数適用 *).
     = 7
     : nat

Coq の簡約にはいくつかすごい性質があります。

簡約は必ず停止します。無限ループには絶対ならないそうです。
t という一つの式が、簡約の仕方によって t1 と t2 という別の式になったとします。すると t1 と t2 をさらに頑張って簡約すると必ず一つの式 t3 が出来るそうです。
簡約しても全体の型は変わりません。

宣言と定義の変なところ

Coq では、ある新しい名前を付けるのに宣言と定義という二つの方法があります。宣言は名前に型を割り当て、定義は名前に型と値を割り当てます。

Coq < Parameter some_number : nat (* 宣言。型を割り当てる *).
some_number is assumed

Coq < Definition four:nat := 4 (* 定義。型と値を割り当てる *).
four is defined

Coq < Check some_number + four.
some_number + four
     : nat

他のプログラミング言語でも、例えば C のヘッダファイルのシグネチャのように名前と型を割り当てる物はありますが、それでも必ず実行時には値が入っているので、この Coq の型だけで値が無いというのはかなり変です。私の強引な理解では、宣言というのは some_number := nat new という風に新たなインスタンスを作って名前をつける物で、定義というのは、four := some_number のように既存のインスタンスに別名を付ける事なのかなと思ってますが、間違ってたらまた書きます。

また、forall も宣言として働くので、これが forall が理解しにくい原因かなと思っています。これから勉強して行きたいと思います。

型の変なところ

type (型)とその値の階層は次のようになっています。大きく Set (データとプログラムに関するもの) と Prop (証明に関するもの) に分かれています。Type、Set、Prop のように型の型になる物を sort と呼びます。Coq 内の値は必ず一つだけ型を持ちます。例えばある数値が同時に自然数に属していたり、整数に属していたりという事は無く、それぞれ独立しています。継承もありません。

Type など : Universe(宇宙) 型の型
- Set : (Set の要素を Specification(仕様) と呼ぶ)
  - nat など : データ型 (データ型や関数の要素を Program(プログラム) と呼ぶ)
    - 0, 1, 2, ... など
  - nat -> nat など : 関数型
    - fun x:nat => x など
  - bool : 真偽データ型
    - true : データとしての真
- Prop : (Prop の要素を Proposition (命題)と呼ぶ)
  - 1 = 1 等 : 命題 (命題の要素を proof (証明)と呼ぶ)
  - True : 常に真の命題
    - I : 常に真の命題の証明
  - False : 偽に偽の命題
- Set->Set など : 高階型

前にType の型は Type だという事を書きましたが、これは嘘で、少なくとも Coq'Art には、Type の型は Type(1) であり、Type(1) の型は Type(2) であり。。。と永遠に続くと書いてあります。これが本当に現実の Coq で実装されているかどうかは知りません。あと、ややこしい事に、-> には使われ方によって関数を表す場合と高階型を表す場合があります。

Coq の型はファーストクラスオブジェクトです。つまり、数字なんかの値と同じように演算したり変数に代入する事が出来ます。なので typedef のような事がしたければ単に代入を使えば良いです。

Coq < Definition natToNat := nat -> nat.
natToNat is defined

Coq < Check (fun x:nat => x + 1) : natToNat.
(fun x : nat => x + 1):natToNat
     : natToNat

Coq の型で一番変なところは、依存型と呼ばれる物です。普通のプログラミング言語では、ある関数の引数と返り値の型はあらかじめ決まっていますが、依存型を使うと引数に応じて別の型を返す事が出来ます。また調べてから書きます。

言語ゲーム

とあるエンジニアが嘘ばかり書く日記