ティエリー・コカンが考案した型理論
数理論理学 と コンピュータサイエンス において 、 構成法 ( CoC ) は Thierry Coquand が考案した 型理論です。これは 型付き プログラミング言語 としても、 数学の 構成的 基盤としても機能します 。この 2 番目の理由から、CoC とその派生型は Coq やその他の 証明支援ツール の基礎となっています。
その変種には、帰納的構造の計算（ 帰納的型を追加する）、（共）帰納的構造の計算（共帰納を追加する）、および帰納的構造の述語的計算（一部の 非予測性を 削除する）が含まれます 。
一般的な特徴 CoC は、当初 Thierry Coquand によって開発された高階型 付きラムダ計算 です。Barendregtの ラムダ キューブ の頂点に位置するものとしてよく知られています。CoC 内では、項から項への関数だけでなく、項から 型 、型から型、型から項への関数を定義することができます。
CoCは 強力に標準化されており 、したがって 一貫性がある 。 [1]
使用法 CoC は Coq 証明支援機能 と並行して開発されてきました。理論に機能が追加される (または潜在的な障害が除去される) と、それらは Coq で利用できるようになります。
CoC のバリエーションは、 Matita や Lean などの他の証明支援ツールでも使用されます。
構成の計算の基礎 構成の計算は、カリー・ハワード同型性 の拡張と見なすことができます 。カリー・ハワード同型性は、 単純型ラムダ計算の項を 直観主義命題論理 の 各 自然演繹証明に関連付けます。構成の計算は、この同型性を完全な直観主義 述語計算 の証明に拡張します 。これには、量化ステートメント (「命題」とも呼ばれます) の証明が含まれます。
条項 構成の計算における項は、次の規則を使用して構成され
ます 。
T
{\displaystyle \mathbf {T} }
は用語（ タイプ とも呼ばれます）です。
ポ
{\displaystyle \mathbf {P} }
項（ prop とも呼ばれ、すべての命題の型）です。 変数（ ）は項です。
x 、 ええ 、 …
{\displaystyle x,y,\ldots }
およびが項である 場合 、 も項です 。
あ
{\displaystyle A}
B
{\displaystyle B}
（ あ B ）
{\displaystyle (AB)}
およびが 項であり、が変数である 場合 、以下も項になります。
あ
{\displaystyle A}
B
{\displaystyle B}
x
{\displaystyle x}
（ λ x : あ 。 B ）
{\displaystyle (\lambda x:AB)}
、
（ ∀ x : あ 。 B ）
{\displaystyle (\forall x:AB)}
。 言い換えれば、バッカス・ナウア記法 の構文は 次のようになります。
e ::=
T
∣
ポ
∣ x ∣ e e ∣ λ x
:
e 。 e ∣ ∀ x
:
e 。 e
{\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}ee\mid \forall x{\mathbin { :}}ええ}
構成の計算には 5 種類のオブジェクトがあります。
証明、つまり 命題 の型を持つ用語 。 命題、 小さな型 としても知られています 。 述語 ：命題を返す関数です。 大規模な型 、これは述語の型です ( は大規模な型の例です)。
ポ
{\displaystyle \mathbf {P} }
T
{\displaystyle \mathbf {T} }
それ自体が大きな型の型です。
判決 構成の計算により、 型付けの判断 を証明することができます。
x
1
:
あ
1
、
x
2
:
あ
2
、 … ⊢ t : B
{\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}
、 これは次のような意味合いとして読み取ることができる
変数がそれぞれ型 を持つ 場合 、項は 型 を持ちます 。
x
1
、
x
2
、 …
{\displaystyle x_{1},x_{2},\ldots }
あ
1
、
あ
2
、 …
{\displaystyle A_{1},A_{2},\ldots }
t
{\displaystyle t}
B
{\displaystyle B}
構成の計算に対する有効な判断は、一連の 推論規則 から導き出されます。以下では、 は 一連の型割り当てを意味し
、 は 項を意味し、 は または の いずれかを意味します 。 は、項 の 自由変数 を項 に 置き換え た結果を意味するものとします 。
Γ
{\displaystyle \ガンマ}
x
1
:
あ
1
、
x
2
:
あ
2
、 …
{\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }
あ 、 B 、 Ｃ 、 だ
{\displaystyle A,B,C,D}
け 、 ら
{\displaystyle K,L}
ポ
{\displaystyle \mathbf {P} }
T
{\displaystyle \mathbf {T} }
B [ x := いいえ ]
{\displaystyle B[x:=N]}
いいえ
{\displaystyle N}
x
{\displaystyle x}
B
{\displaystyle B}
推論規則は次の形式で記述される。
Γ ⊢ あ : B
Γ ′
⊢ Ｃ : だ
{\displaystyle {\frac {\Gamma \vdash A:B}{\Gamma '\vdash C:D}}}
、 つまり
が有効な判断であれば 、 も有効な判断です 。
Γ ⊢ あ : B
{\displaystyle \Gamma \vdash A:B}
Γ ′
⊢ Ｃ : だ
{\displaystyle \Gamma '\vdash C:D}
構成の計算のための推論規則 1 .
Γ ⊢
ポ
:
T
{\displaystyle {{} \over \Gamma \vdash \mathbf {P} :\mathbf {T} }}
2 .
Γ 、 x : あ 、
Γ ′
⊢ x : あ
{\displaystyle {{} \over {\Gamma ,x:A,\Gamma '\vdash x:A}}}
3 .
Γ ⊢ あ : け Γ 、 x : あ ⊢ B : ら
Γ ⊢ （ ∀ x : あ 。 B ） : ら
{\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash B:L \over {\Gamma \vdash (\forall x:AB):L}}}
4 .
Γ ⊢ あ : け Γ 、 x : あ ⊢ いいえ : B
Γ ⊢ （ λ x : あ 。 いいえ ） : （ ∀ x : あ 。 B ）
{\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B)}}}
5 .
Γ
⊢
M
:
(
∀
x
:
A
.
B
)
Γ
⊢
N
:
A
Γ
⊢
M
N
:
B
[
x
:=
N
]
{\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}
6 .
Γ
⊢
M
:
A
A
=
β
B
Γ
⊢
B
:
K
Γ
⊢
M
:
B
{\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}}
論理演算子の定義 構成の計算には基本的な演算子がほとんどありません。命題を形成する唯一の論理演算子は です 。ただし、この 1 つの演算子で他のすべての論理演算子を定義するのに十分です。
∀
{\displaystyle \forall }
A
⇒
B
≡
∀
x
:
A
.
B
(
x
∉
B
)
A
∧
B
≡
∀
C
:
P
.
(
A
⇒
B
⇒
C
)
⇒
C
A
∨
B
≡
∀
C
:
P
.
(
A
⇒
C
)
⇒
(
B
⇒
C
)
⇒
C
¬
A
≡
∀
C
:
P
.
(
A
⇒
C
)
∃
x
:
A
.
B
≡
∀
C
:
P
.
(
∀
x
:
A
.
(
B
⇒
C
)
)
⇒
C
{\displaystyle {\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:A.B&(x\notin B)\\A\wedge B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)&\\\exists x:A.B&\equiv &\forall C:\mathbf {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}}
データ型の定義 コンピュータ サイエンスで使用される基本的なデータ型は、構造の計算によって定義できます。
ブール値
∀
A
:
P
.
A
⇒
A
⇒
A
{\displaystyle \forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A}
ナチュラル
∀
A
:
P
.
(
A
⇒
A
)
⇒
A
⇒
A
{\displaystyle \forall A:\mathbf {P} .(A\Rightarrow A)\Rightarrow A\Rightarrow A}
製品
A
×
B
{\displaystyle A\times B}
A
∧
B
{\displaystyle A\wedge B}
不連続和集合
A
+
B
{\displaystyle A+B}
A
∨
B
{\displaystyle A\vee B}
ブール値と自然数はチャーチ符号化 と同じように定義されていることに注意してください 。しかし、命題の拡張性と証明の無関係性から追加の問題が生じます。 [2]
参照
参考文献
^ Coquand, Thierry; Gallier, Jean H. (1990 年 7 月)。「クリプキのような解釈を用いた構成理論の強い正規化の証明」。 技術レポート (Cis) (568): 14。 ^ 「標準ライブラリ | Coq 証明アシスタント」 。coq.inria.fr。2020 年 8 月 8 日 閲覧 。
出典
Coquand, Thierry ; Huet, Gérard (1988). 「構成の計算」 (PDF) . 情報と計算 . 76 (2–3): 95–120. doi : 10.1016/0890-5401(88)90005-3 . オンラインでも自由にアクセスできます: Coquand、Thierry;ジェラール・ユエ (1986)。構造微積分学 (技術報告書)。 INRIA 、Centre de Rocquencourt。 530。 用語がかなり異なることに注意してください。たとえば、 ( ) は [ x : A ] B と書きます 。
∀
x
:
A
.
B
{\displaystyle \forall x:A.B}
Bunder, MW; Seldin, Jonathan P. (2004). 「基本的な構成計算のバリエーション」 CiteSeerX 10.1.1.88.9497 . Frade, Maria João (2009). 「Calculus of Inductive Constructions」 （PDF） 。2014-05-29 の オリジナル （トーク）からアーカイブ 。2013-03-03 に取得 。 Huet, Gérard (1988)。「構成の計算における帰納原理の形式化」 (PDF) 。Fuchi, K.、 Nivat, M. (編)。 未来世代コンピュータのプログラミング 。North-Holland。pp. 205–216。ISBN 0444704108 2015年7月1日時点の オリジナル （PDF）よりアーカイブ。 — CoCの適用
![{\displaystyle B[x:=N]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/61566653d9ef5af79e883a86e031d16e4626e2bf)
![{\displaystyle {\Gamma \vdash M:(\forall x:AB)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/28333e638179f17baa4c4ac9bc55476dd9d90f23)
