pCICについて - Sis puella magica!

TSG Advent Calendar 2015 - Adventarの12/13の記事です。

序文 - pCICとは

pCICはPredicative Calculus of (Co)Inductive Constructionsのことで、coqの型システムのことです。
定理証明支援系と言われるcoqですが、そもそもcoqで「証明する」とはどういうことでしょうか。
coqにおける命題は型(type)に、その証明は項(term)に対応しています(Curry-Howard同型を思い出してください)。つまり、coqである命題Pを証明するということは、型Pを持つ項を探してくることに対応しています。
このことから、coqの動作を理解する上でpCICを理解することは重要だと考えられます。
この記事はcoqの本質とも言えるpCICの側面からcoqの動作について理解しようという趣旨で書かれています。自分が探した限り、そのような記事はあまりなさそうなので書くことにしました。

命題はtypeに、証明はtermに

例として

forall (P Q : Prop), P -> Q -> P.

という簡単な命題を考えてみます。

まず

Definition K : forall (P Q : Prop), P -> Q -> P.

と書くと、Kは型だけ定義されて項は定義されていない状態になります。
proof editing modeで

Show Proof.

とすると今の証明の状態が表示されるので、最初の状態なら

?1

と表示されるでしょう。?1はplaceholderで、まだ定義されていない項を表しています。
もう少し進んで

intros.
Show Proof.

としてみると

(fun (P Q : Prop) (H : P) (H0 : Q) => ?5)

と表示されます。

  P : Prop
  Q : Prop
  H : P
  H0 : Q
  ============================
   P

?5というplaceholderは今のゴールに対応していて、P, Q, H, H0という変数を使って型Pを持つ項を作って?5の位置に入れれば証明が完成することが分かります。Hは既に型Pを持っているので、assumptionで?5にHを入れて証明は完了です。
この作業を通して、型 forall (P Q : Prop), P -> Q -> P を持つ項を定義し、それにKという名前をつけました。

Print K.

でそれを確認できます。
証明とは言っても、ある型を持つ項を定義するだけなので、最初から項を与えてしまっても同じことです。それを確認するためにK'を定義しました。
先ほどplaceholderがゴールに対応していると言いましたが、複数のゴールがあるときは複数のplaceholderがあるときです。上のコードの後半はそれを確認するための例です。

ちなみに

forall x : P, M.

という形の式でMにxが(自由に)現れない場合

P -> M

と表現されます。
つまり「ならば」を意味する"->"は実際にはforallです。

pure type system

pCICについてはChapter 4 Calculus of Inductive Constructionsに書いてあるので、これを解説すればよいのですが、やや複雑なので、先にpure type systemについて説明したいと思います。
pure type systemは型付きラムダ計算のフレームワークの一つで、適当なパラメーターを設定すれば単純型付きラムダ計算や多相型、依存型を含んだ型付きラムダ計算の体系なども作ることができます。pCICもベースはこのpure type systemなので(たぶん)、最初にpure type systemを簡単に理解しておくとpCICもスムーズに理解できるかと思います。
pure type systemについてはpure type system in nLabとかLectures on the Curry-Howard Isomorphismとかを見ると良いと思います。
pure type systemは $(S, A, R)$ の三つ組をパラメーターとして与えることで定まります。termとtypeは構文的には同じで、constant, variable, abstruction, product, applicationによって、再帰的に定義されます。
$T := c | x | \lambda x : T . T | \Pi x : T . T | T T$
このconstantを与えるのが $S$ (sort)です。また、 $\lambda, \Pi$ は変数を束縛します。
そして、このtermを用いてtype judgement $\vdash$ を定義します。この定義についてはnlabを参照してください。 $A$ は(axioms)に、 $R$ は(product)に使われています。
$\Gamma \vdash M : t$ の $\Gamma$ はcontextと呼ばれることが多いです。これは変数宣言のリストと考えてください。慣れている人にはわざわざ説明する必要はないと思いますが、 $\vdash$ という記号は大抵「 $\vdash$ の左を仮定した時に $\vdash$ の右が導ける」という意味で使われ、今回使う $x_1 : t_1, \dots, x_n : t_n \vdash M : t$ も「変数 $x_1$ が型 $t_1$ , .. , 変数 $x_n$ が型 $t_n$ であると仮定した時に、項 $M$ は型 $t$ である」と考えてください。
$\Gamma$ は順序も重要なので気をつけてください。

pCIC

ここからChapter 4 Calculus of Inductive Constructionsの内容に入っていきます。

Term

pure type systemのtermに let .. in .. を付け足したくらいしか差はありません。
coqではabstruction: $\lambda x : t. M$ は fun x: t => M に、product: $\Pi x : t. M$ は forall x:t, M に対応します。

Context

上で説明したpure type systemと少し変わるところは、context $\Gamma$ はglobal environment $E$ とlocal context $\Gamma$ に分けられ、 $E [ \Gamma ]$ と表されます。また、 $E [ \Gamma ]$ の中には変数の型の宣言 $x : t$ だけではなく、変数の定義 $x:=M : t$ も認められます。

Local context

最初の例で説明すると

  P : Prop
  Q : Prop
  H : P
  H0 : Q
  ============================
   P

における、横棒の上のやつのことです。
pure type systemでのcontextとほぼ同じですが、上で書いたように変数の定義も認められています。

Goal let n := 1 in n = 1.
intro.

  n := 1 : nat
  ============================
   n = 1

Environment

coqのリファレンスマニュアルには

An environment is an ordered list of declarations of global names. Declarations are either assumptions or “standard” definitions, that is abbreviations for well-formed terms but also definitions of inductive objects.

とあります。
Assumptionにはこの辺のtacticsが対応してます。ここに書いてあるのは実質AxiomとVariableの2つだけで、違いはVariableの方はSectionの中に閉じ込められることです。
Definitionにはこの辺のtacticsが対応してます。先ほどと同じように、DefinitionとLetがあって、LetはSectionの中に閉じ込められます。
Environmentを見るにはPrint Allというコマンドを使えば良さそうです。
次の例を試してみると動作がよく解ると思います。

bとdがSectionの外では見えなくなること、bとdを使って定義されたeがSectionの外ではどうなるのかということに注意してください。
EnvironmentにはInductiveの定義も含まれるようです。

Typing rules

だいたいpure type systemと同じなので三つ組 $(S, A, R)$ を与えるだけにとどめます。
$S = \{{\tt Prop}, {\tt Set}, {\tt Type}(i) | i \in \mathbb{N}\}$
$A = \{({\tt Prop}, {\tt Type}(i)) | i \in \mathbb{N}\} \cup \{({\tt Set}, {\tt Type}(i)) | i \in \mathbb{N}\} \cup \{({\tt Type}(i), {\tt Type}(j)) | i< j\}$
$R = \{(s, {\tt Prop}) | s \in S\} \cup \{({\tt Prop}, {\tt Set}), ({\tt Set}, {\tt Set})\} \cup \{({\tt Type}(i), {\tt Type}(j), {\tt Type}(k)) | i, j \le k\}$
ここで、 $(s1, s2) \in R$ は $(s1, s2, s2) \in R$ という意味であることに気をつけてください。

Conversion rules

pure type systemでは簡約はβ簡約だけでしたが、pCICではいくつかあります。そのため、pure type systemよりも(conversion)規則は複雑です。

β-reduction

通常のβ簡約

ι-reduction

inductive objectに関する簡約らしいです。

δ-reduction

$E$ や $\Gamma$ に変数の定義( $x:=M : t$ )が含まれるとき、項の中の $x$ を $M$ で置き換えることです。

ζ-reduction

δ-reductionと似ていますが、
${\tt let}\; x:=M \; {\tt in} \; N$ を $N\{x:=M\}$ とする簡約です。

η-conversion

$M$ と $\lambda x : t . M x$ ( $x$ は $M$ の自由変数に含まれない)を同一視することです。

最後に

実はまだInductive Definitions以降はちゃんと読んでいないのでInductiveについてはよくわかっていません。Inductiveについてはそのうち書こうかなと思っています。
pure type systemについてももう少し詳しく説明するべきだった気もするので気が向いたら書きます。