構成の計算

Type theory created by Thierry Coquand

数理論理学とコンピュータサイエンスにおいて、構成計算はティエリー・コカンによって創始された型理論です。これは型付きプログラミング言語としても、数学の構成的基盤としても機能します。この第二の理由から、CoCとその派生はRocqやその他の証明支援系の基礎となっています。

その変種には、帰納的構造の計算（帰納的型を追加する）、（共）帰納的構造の計算（共帰納を追加する）、および帰納的構造の述語的計算（一部の非予測性を削除する）が含まれます^{[引用が必要]}。

一般的な特徴

CoCは、ティエリー・コカンによって最初に開発された高階型付きラムダ計算です。バレンドレヒトのラムダキューブの頂点に位置することでよく知られています。CoCでは、項から項、項から型、型から型、型から項への関数を定義することができます。

CoCは強力に標準化されており、したがって一貫性があります。^[1]

使用法

CoCはRocq 証明支援システムと並行して開発されてきました。理論に追加された機能（または潜在的な欠点の除去）は、Rocqでも利用可能になりました。

CoC のバリアントは、MatitaやLeanなどの他の証明支援ツールでも使用されます。

構成法の計算の基礎

構成計算は、カリー・ハワード同型性の拡張とみなすことができます。カリー・ハワード同型性は、単純型ラムダ計算の項を直観主義命題論理における自然演繹証明のそれぞれに関連付けます。構成計算は、この同型性を、量化文（以下「命題」とも呼ぶ）の証明を含む完全な直観主義述語計算の証明に拡張します。

条項

構成の計算における項は、次の規則を使用して構成されます。

• ${\displaystyle \mathbf {T} }$は用語（タイプとも呼ばれます）です。
• ${\displaystyle \mathbf {P} }$項（propとも呼ばれ、すべての命題の型）です。
• 変数（）は項です。 ${\displaystyle x,y,\ldots }$
• およびが項である場合、 も同様です。 ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle (AB)}$
• および が項であり、 が変数である場合、以下も項になります。 ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle x}$
  • ${\displaystyle (\lambda x:A.B)}$、
  • ${\displaystyle (\forall x:A.B)}$。

言い換えれば、バッカス・ナウア記法の構文は次のようになります。

${\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}e.e\mid \forall x{\mathbin {:}}e.e}$

構成の計算には 5 種類のオブジェクトがあります。

1. 証明、つまり命題を型とする用語。
2. 命題（小さな型とも呼ばれる）
3. 述語、命題を返す関数です。
4. 大きな型、これは述語の型です (は大きな型の例です)。 ${\displaystyle \mathbf {P} }$
5. ${\displaystyle \mathbf {T} }$それ自体が大きな型の型です。

β-等価性

型なしラムダ計算と同様に、構成計算では項の同値性という基本的な概念、つまり-同値性を用います。これは-抽象化の意味を捉えています。 ${\displaystyle \beta }$ ${\displaystyle \lambda }$

• ${\displaystyle (\lambda x:A.B)N=_{\beta }B(x:=N)}$

${\displaystyle \beta }$-同値性は、構成の計算における合同関係であり、

• かつならば。​ ${\displaystyle A=_{\beta }B}$ ${\displaystyle M=_{\beta }N}$ ${\displaystyle AM=_{\beta }BN}$

判断

構成の計算により、型付けの判断を証明することができます。

${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}$、

これは次のような意味合いとして読み取ることができる

変数がそれぞれ型 を持つ場合、項は型 を持ちます。 ${\displaystyle x_{1},x_{2},\ldots }$ ${\displaystyle A_{1},A_{2},\ldots }$ ${\displaystyle t}$ ${\displaystyle B}$

構成の計算における有効な判断は、一連の推論規則から導出されます。以下では、は型割り当ての列 、は項、は または のいずれかを意味します。 は、を項の自由変数に置き換えた結果を意味します。 ${\displaystyle \Gamma }$ ${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }$ ${\displaystyle A,B,C,D}$ ${\displaystyle K,L}$ ${\displaystyle \mathbf {P} }$ ${\displaystyle \mathbf {T} }$ ${\displaystyle B[x:=N]}$ ${\displaystyle N}$ ${\displaystyle x}$ ${\displaystyle B}$

推論規則は次の形式で記述される。

${\displaystyle {\frac {\Gamma \vdash A:B}{\Gamma '\vdash C:D}}}$、

つまり

が有効な判断であれば、 も有効な判断です。 ${\displaystyle \Gamma \vdash A:B}$ ${\displaystyle \Gamma '\vdash C:D}$

構成の計算のための推論規則

1 . ${\displaystyle {{} \over \Gamma \vdash \mathbf {P} :\mathbf {T} }}$

2 . ${\displaystyle {{\Gamma \vdash A:K} \over {\Gamma ,x:A,\Gamma '\vdash x:A}}}$

3 . ${\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash B:L \over {\Gamma \vdash (\forall x:A.B):L}}}$

4 . ${\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 . ${\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}$

6 . ${\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}}$

論理演算子の定義

構成計算には基本的な演算子がほとんどありません。命題を形成する唯一の論理演算子は です。しかし、この演算子1つで他のすべての論理演算子を定義するのに十分です。 ${\displaystyle \forall }$

${\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}}}$

データ型の定義

コンピュータ サイエンスで使用される基本的なデータ型は、構成の計算によって定義できます。

ブール値

${\displaystyle \forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A}$

ナチュラルズ

${\displaystyle \forall A:\mathbf {P} .(A\Rightarrow A)\Rightarrow A\Rightarrow A}$

製品 ${\displaystyle A\times B}$

${\displaystyle A\wedge B}$

分離和集合 ${\displaystyle A+B}$

${\displaystyle A\vee B}$

ブール値と自然数はチャーチ符号化と同様に定義されていることに注意してください。しかし、命題の外延性と証明の無関係性から、追加の問題が生じます。^[2]

参照

• 純粋な型システム
• ラムダキューブ
• システムF
• 依存型
• 直観主義型理論
• ホモトピー型理論

参考文献

1. コカン, ティエリー; ガリエ, ジャン H. (1990年7月). 「クリプキ的解釈を用いた構成理論の強正規化の証明」.技術報告 (Cis) (568): 14.
2. “標準ライブラリ | Coq Proof Assistant”. coq.inria.fr . 2020年8月8日閲覧。

出典

• コカン, ティエリー;ユエ, ジェラール(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と書きます。 ${\displaystyle \forall x:A.B}$
• バンダー, MW; セルディン, ジョナサン P. (2004). 「構成の基本計算法の変種」. CiteSeerX  10.1.1.88.9497 .
• Frade, Maria João (2009). 「帰納的構成の計算法」(PDF) . 2014年5月29日時点のオリジナル(トーク)からのアーカイブ。 2013年3月3日閲覧。
• Huet, Gérard (1988). 「構成計算における帰納法原理の形式化」(PDF) . Fuchi, K.; Nivat, M. (編). 『未来世代コンピュータのプログラミング』 North-Holland. pp.  205– 216. ISBN 0444704108. 2015年7月1日時点のオリジナル（PDF）からアーカイブ。— CoCの適用

Retrieved from "https://en.wikipedia.org/w/index.php?title=Calculus_of_constructions&oldid=1324227341"