型理論

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

数学論理学コンピュータサイエンスでは、型理論すべての「項」が「型」を持つ形式的なシステムです。型理論の「型」には、プログラミング言語の「型」と同様の役割があります。これは、用語に対して実行できる操作を指示し、変数の場合は、置き換えられる可能性のある値を指示します。

いくつかの型理論は、数学の基礎として理論を設定するための代替として機能します。基礎として提案された2つの影響力のある型理論は、アロンゾ・チャーチ型付きラムダ計算ペール・マルティン・レーフ直観的型理論です。ほとんどのコンピューター化された証明書記体系は、その基礎として型理論を使用しています。一般的なものは、ティエリー・コカンドの帰納的構造の微積分です

型理論は、バグを減らし、特定のコンパイラの最適化を容易にするために使用されるプログラミング言語機能である型システムと密接に関連しており、場合によっては重複しています。型理論と型システムは重複する可能性があるため、一部の専門家は「型システム」というフレーズを使用して特定の形式システムを指し、「型理論」というフレーズを使用してそれらの学術研究を指します。

歴史

型理論は、素朴集合論形式論理学に基づく数理論理学のパラドックスを回避するために作成されましたバートランド・ラッセルによって発見されたラッセルのパラドックスは、それ自体を含む「すべての可能なセット」を使用してセットを定義できるために存在しました。1902年から1908年の間に、バートランドラッセルは、問題を解決するためにさまざまな「タイプの理論」​​を提案しました。1908年までに、ラッセルは「還元公理」とともに型の「分岐」理論に到達しました。どちらもホワイトヘッドラッセルプリンキピアマテマティクで顕著に取り上げられました。このシステムは、型の階層を作成し、各具体的な数学的(および場合によっては他の)エンティティを型に割り当てることで、ラッセルのパラドックスを回避しました。特定のタイプのエンティティは、階層の下位にあるタイプのエンティティから排他的に構築されるため、エンティティがそれ自体を使用して定義されることはありません。

タイプは必ずしもロジックで使用されるとは限りませんでした。ラッセルのパラドックスを回避するための他のテクニックがありました。[1] 1つの特定のロジック、アロンゾチャーチラムダ計算で使用すると、タイプが定着しました

最も有名な初期の例は、アロンゾチャーチ単純型付きラムダ計算です。チャーチの型理論[2]は、形式体系が元の型なしラムダ計算を苦しめたKleene-Rosserパラドックスを回避するのに役立ちました。チャーチは、それが数学の基礎として役立つ可能性があることを実証し、高階述語論理と呼ばれていました。

「型理論」という句は、現在、一般的にラムダ計算に基づく型システムを指します。影響力のあるシステムの1つは、構成主義数学の基礎として提案されたPerMartin-Löf直観的型理論です。もう1つは、Thierry Coquandの構造の計算です。これは、 CoqLean、およびその他の「証明アシスタント」(コンピューター化された証明作成プログラム)によって基礎として使用されます。型理論は、ホモトピー型理論によって示されるように、活発な研究の領域です

型理論入門

型理論はたくさんあるので、すべてを説明するのは難しいです。このセクションでは、多くの主要な型理論の機能について説明します。型理論に不慣れな方への入門書です。このセクションは、型理論の完全な分類でも、それらの網羅的な説明でもありません

基本

用語と種類

型理論では、すべての項に型があります。用語とそのタイプは、「用語 :タイプ」と一緒に書かれることがよくあります。型理論に含める一般的な型は自然数であり、しばしば「"または" nat "。もう1つはブール論理値です。したがって、それらのタイプを含む非常に単純な用語は次のとおりです。

  • 0:nat
  • 42:nat
  • true:bool

用語は、関数呼び出しを使用して他の用語から構築できます。型理論では、関数呼び出しは「関数適用」と呼ばれます。関数適用は、指定されたタイプの項を取り、別の指定されたタイプの項になります。関数適用は、従来の「関数引数引数、...)」の代わりに「関数 引数 引数...」と書かれています。自然数の場合、2つの自然数を取る「add」と呼ばれる関数を定義することができます。したがって、それらのタイプに関するいくつかの用語は次のとおりです。

  • 0 0を追加:nat
  • 2 3を追加:nat
  • 1を追加(1を追加(1 0を追加)):nat

前項では、操作の順序を示すために括弧が追加されました。技術的には、ほとんどの型理論ではすべての操作に括弧が必要ですが、実際には括弧は書かれておらず、著者は読者が優先順位と結合性を使用してどこにあるかを知ることができると想定しています。同様に簡単にするために、「」と書くのが一般的な表記法です。「追加」の代わりに「 "。したがって、上記の用語は次のように書き直される可能性があります。

  • 0 + 0:nat
  • 2 + 3:nat
  • 1 +(1 +(1 + 0)):nat

用語には変数が含まれる場合もあります。変数には常に型があります。したがって、「x」と「y」が「nat」型の変数であると仮定すると、以下も有効な用語です。

  • x:nat
  • x + 2:nat
  • x +(x + y):nat

「nat」や「bool」以外にも種類があります。「追加」という用語はすでに見てきましたが、これは「nat」ではありませんが、2つの「nat」に適用されると「nat」に計算される関数です。「追加」のタイプについては、後で説明します。まず、「計算対象」について説明する必要があります。

計算

型理論には、計算の表記法が組み込まれています。次の用語はすべて異なります。

  • 1 + 4:nat
  • 3 + 2:nat
  • 0 + 5:nat

しかし、それらはすべて「5:nat」という用語で計算されます。型理論では、「還元」と「還元」という言葉を使って計算を指します。したがって、「0 + 5:nat」は「5:nat」に還元されます。「0+ 5:nat」と書くことができます5:nat "。計算は機械的であり、用語の構文 を書き直すことによって実行されます。

変数を含む用語も減らすことができます。したがって、「x +(1 + 4):nat」という用語は「x + 5:nat」になります。(チャーチ・ロッサーの定理のおかげで、用語内の任意のサブ用語を減らすことができます。)

さらに減らすことができない変数のない用語は「正規用語」です。上記のすべての用語は、正規の用語である「5:nat」になります。自然数の正規項は次のとおりです。

  • 0:nat
  • 1:nat
  • 2:nat

明らかに、同じ項を計算する項は同じです。したがって、「x:nat」と仮定すると、「x +(1 + 4):nat」と「x +(4 + 1):nat」という用語は、どちらも「x + 5:nat」に還元されるため、等しくなります。2つの項が等しい場合、それらを相互に置き換えることができます。平等は型理論の複雑なトピックであり、多くの種類の平等があります。2つの項が同じ項に計算されるこの種の平等は、「判断的平等」と呼ばれます。

関数

型理論では、関数は用語です。関数は、ラムダ用語にすることも、「ルールによって」定義することもできます。

ラムダ用語

ラムダ項は「(λvariablename:type1 .term)」のよう なりタイプは「type1 」になります。 type2 "。タイプ" type1 type2 "は、ラムダ項がタイプ" type1 "のパラメーターを取り、タイプ" type2 "の項に計算される関数であることを示します。ラムダ項内の項は、変数のタイプが"であると仮定すると、 " type2 "の値である必要があります。 type1 "。

ラムダ項の例は、引数を2倍にするこの関数です。

  • (λx:nat。(xxを追加)):natnat

変数名は「x」で、変数のタイプは「nat」です。「(addxx)」という用語は、「x:nat」と仮定すると、「nat」タイプになります。したがって、ラムダ用語は「nat」タイプになります。nat "は、引数として" nat "が指定されている場合、" nat "に計算されることを意味します。ラムダ項に対してリダクション(別名計算)が定義されます。関数が適用される(別名呼び出される)と、引数は次のようになります。パラメータの代わりに使用します。

以前、関数適用は関数項の後にパラメーターを置くことによって書かれることを見ました。したがって、タイプ「nat」のパラメーター「5」を使用して上記の関数を呼び出したい場合は、次のように記述します。

  • (λx:nat。(xxを追加))5:nat

ラムダ項はタイプ「nat」でしたnat」は、引数として「nat」を指定すると、「nat」タイプの用語を生成します。引数「5」を指定したため、上記の用語は「nat」タイプになります。用語「(addxx)」のパラメータ「x」の引数「5」。したがって、用語は次のように計算されます。

  • (5 5を追加):nat

これは明らかに次のように計算されます

  • 10:nat

ラムダ用語は、名前がないため、「無名関数」と呼ばれることがよくあります。多くの場合、読みやすくするために、ラムダ用語に名前が付けられます。これは単なる表記であり、数学的な意味はありません。一部の著者はそれを「表記上の平等」と呼んでいます。上記の関数には、次の表記を使用して名前を付けることができます。

  • ダブル:natnat :: =(λx:nat。(xxを追加))

これは上記と同じ関数ですが、書き方が異なります。つまり、用語

  • ダブル5:nat

まだ計算します

  • 10:nat

依存型

依存型とは、関数によって返される型がその引数の値に依存する場合です。たとえば、型理論に型「bool」を定義するルールがある場合、関数「if」も定義します。関数「if」は3つの引数を取り、「if true b c」は「b」に計算され、「if false bc」は「c」に計算されます。しかし、「if abc」のタイプは何ですか?

「b」と「c」が同じタイプの場合、「ifabc」が「b」と「c」と同じタイプであることは明らかです。したがって、「a:bool」と仮定すると、

  • 2 4の場合:nat
  • false trueの場合:bool

ただし、「b」と「c」のタイプが異なる場合、「ifabc」のタイプは「a」の値によって異なります。記号「Π」を使用して、引数を取り、型を返す関数を示します。「B」と「C」と「a:bool」、「b:B」と「c:C」のタイプがあるとすると、

  • if abc:(Πa:bool。BCBCの場合)

つまり、「if」項の型は、最初の引数の値に応じて、2番目または3番目の引数の型のいずれかになります。実際には、「if a B C」は「if」を使用して定義されていませんが、この紹介では詳細が複雑すぎます。

型には計算を含めることができるため、依存型は驚くほど強力です。数学者が「数が存在するそのような素数である」または「数が存在するそのようなプロパティ保持する」、それは依存型として表現することができます。つまり、プロパティは特定の「"そしてそれは結果のタイプに表示されます。

依存型には多くの詳細があります。これらは長すぎて、この紹介には複雑です。詳細については、依存型ラムダキューブに関する記事を参照してください。

宇宙

Π-用語は型を返します。では、それらの戻り値のタイプは何ですか?さて、型を含む型がなければなりません。他のタイプを含むタイプは「ユニバース」と呼ばれます。多くの場合、記号で書かれています時々、宇宙の階層があり、「 :"、" :"など。

宇宙は複雑です。宇宙にそれ自体が含まれている場合、それはジラールのパラドックスのようなパラドックスにつながる可能性があります宇宙の詳細は、この紹介には長すぎて複雑すぎます。

一般的な「ルールによる」タイプと用語

型理論は、推論規則によって定義されます。上記の「機能コア」のルールと、タイプと用語を作成するルールがあります。以下は、一般的なタイプとそれに関連する用語の非網羅的なリストです。

リストは「誘導型」で終わります。これは、リスト内の他のすべての型を作成できる強力な手法です。証明アシスタント「Coq」と「Lean」が使用する数学的基礎は、帰納型の「構造の微積分」(その「機能コア」)である「帰納的構造の微積分」に基づいています。

空のタイプ

のタイプには用語がありません。タイプは通常「" また ""。

何かが計算できないことを示すために使用されます。タイプ「A」の場合、タイプ「A」の関数を作成できます。「、「A」には用語がないことをご存知でしょう。「A」タイプの例としては、「番号が存在する」などがあります。両方のように偶数であり(例「A」の構成方法については、以下の「製品タイプ」を参照してください。)タイプに用語がない場合、「無人」と言います。

ユニットタイプ

ユニットタイプには、正確に1つの正規用語があります。タイプは「" また ""と単一の正規用語は" * "と書かれています。

ユニットタイプは、何かが存在するか、計算可能であることを示すために使用されます。タイプ「A」の場合、タイプ「」の関数を作成できます。「A」、あなたは「A」が1つ以上の用語を持っていることを知っています。タイプが少なくとも1つの用語を持っているとき、それは「人が住んでいる」と言います。

ブール型

ブール型には、正確に2つの正規項があります。タイプは通常「bool」または「" また ""。正規の用語は通常、「true」と「false」です。

ブール型は、次のようなエリミネーター関数「if」で定義されます。

  • 真の場合bcb
  • falsebcの場合c

製品タイプ

製品タイプには、順序対である用語があります。タイプ「A」および「B」の場合、製品タイプは「A」と表記されます。B」。正規用語はコンストラクター関数「pair」によって作成されます。用語は「pairab」です。ここで、「a」はタイプ「A」の用語であり、「b」はタイプ「B」の用語です。製品タイプは、エリミネーター関数「first」および「second」で次のように定義されます。

  • 最初(ペアab)a
  • 2番目(ペアab)b

順序対に加えて、このタイプは「A」と「B」を保持するため、論理演算子「and」に使用されます。両方のタイプのいずれかを保持するため 、交差点にも使用されます。

型理論に依存型がある場合、依存ペアがあります。従属ペアでは、2番目のタイプは最初の項の値に依存します。したがって、タイプは「a:A。B(a)」ここで、「B」のタイプは「A」です。U」。プロパティ「B(a)」を持つ「a」の 存在を示す場合に役立ちます。

合計タイプ

合計型は「タグ付き共用体」です。つまり、タイプ「A」と「B」の場合、タイプ「A + B」は、タイプ「A」の用語またはタイプ「B」の用語のいずれかを保持し、どちらを保持するかを認識します。この型には、コンストラクター「injectionLeft」と「injectionRight」が付属しています。「injectionLefta」の呼び出しは「a:A」を取り、「A + B」タイプの正規用語を返します。同様に、injectionRight b "は" b:B "を取り、タイプ" A + B "の正規項を返します。タイプは、タイプ" C "および関数" f:A "のように、エリミネーター関数" match "で定義されます。C」と「g:BC ":

  • 一致(injectionLeft a)C fg(fa)
  • 一致(injectionRight b)C fg(gb)

合計型は、論理和または共用体に使用されます。

自然数

自然数は通常、ペアノの公理のスタイルで実装されます。ゼロを表す「0:nat」という正規の用語があります。ゼロより大きい正規値は、コンストラクター関数 "S:natを使用しますしたがって、「S 0」は1です。「S(S 0)」は2です。「S(S(S 0)))」は3です。など。10進数は表記上これらの用語と同じです。

  • 1:nat :: = S 0
  • 2:nat :: = S(S 0)
  • 3:nat :: = S(S(S 0))
  • ..。

再帰を使用してすべてのnatの関数を定義するエリミネーター関数「R」で定義された自然数。関数「P:nat」を取ります定義する関数のタイプである「U」。また、ゼロでの値である「PZ:P0」という用語と関数「PS:Pn」を取ります。P(S n)」は、「n」の値を「n + 1」の値に変換する方法を示します。したがって、その計算規則は次のとおりです。

  • RP PZ PS 0PZ
  • RP PZ PS(S)。PS(RP PZ PS)。

以前に使用された関数「add」は、「R」を使用して定義できます。

  • 追加:natnatnat :: = R(λn:nat .natnat)(λn:nat。n)(λg:natnat。(λm:nat .S(gm)))

IDタイプ

アイデンティティタイプは、型理論における平等の3番目の概念です1つ目は「表記上の等式」です。これは「2:nat :: =(S(S 0))」のような数学的な意味はありませんが、読者には役立つ定義です。2つ目は、「判断の等式」です。これは、「x +(1 + 4)」と「x +(4 + 1)」のように、2つの項が同じ項に計算される場合で、どちらも「x +5」に計算されます。しかし、型理論には、「同一性型」または「命題的平等」として知られる別の形式の平等が必要です。

IDタイプが必要な理由は、いくつかの等しい用語が同じ用語に計算されないためです。「x:nat」と仮定すると、「x +1」と「1 + x」という用語は同じ用語に計算されません。「+」は関数「add」の表記であり、関数「R」の表記であることを思い出してください。「x」の値が指定されるまで「R」で計算することはできません。また、指定されるまで、「R」への2つの異なる呼び出しは同じ用語で計算されません。

IDタイプには、同じタイプの2つの用語「a」と「b」が必要であり、「a = b」と記述されます。したがって、「x +1」および「1+ x」の場合、タイプは「x + 1 = 1 + x」になります。正規用語は、コンストラクター「再帰性」を使用して作成されます。「再帰性a」という呼び出しは、「a」という用語を取り、「a = a」タイプの正規の用語を返します。

IDタイプによる計算は、エリミネーター関数「J」を使用して行われます。関数「J」を使用すると、「a」、「b」に依存する項、および「a = b」タイプの項を書き換えて、「b」を「a」に置き換えることができます。「J」は一方向であり、「b」を「a」に置き換えることしかできませんが、アイデンティティタイプが反射的対称的推移的であることを証明できます。

正規の項が常に「a = a」であり、「x +1」が「1+ x」と同じ項に計算されない場合、「x + 1 = 1 + x」の項を作成するにはどうすればよいですか?「R」関数を使用します。(上記の「自然数」を参照してください。)「R」関数の引数「P」は、「(λx:nat。x+ 1 = 1 + x)」と定義されています。他の引数は、帰納法の証明の一部のように機能します。ここで、「PZ:P0」は基本ケース「0+ 1 = 1 +0」および「PS:Pn」になります。P(S n)」は帰納的ケースになります。これは、基本的に、「x + 1 = 1 + x」の「x」が標準値に置き換えられた場合、式は「再帰性(x + 1)」と同じになることを意味します。 "。関数" R "のこのアプリケーションのタイプは" x:natx + 1 = 1 + x "。これと関数" J "を使用して、任意の項で" x +1 "を" 1 + x "に置き換えることができます。このようにして、IDタイプは次のような等式をキャプチャできます。判断の平等では不可能です。

明確にするために、タイプ「0 = 1」を作成することは可能ですが、そのタイプの用語を作成する方法はありません。タイプ「0 = 1」の用語がないと、関数「J」を使用して、別の用語の「1」を「0」に置き換えることはできません。

型理論における平等の複雑さは、それを活発な研究分野にします。ホモトピー型理論を参照してください。

誘導型

誘導型は、多種多様な型を作成する方法です。実際、上記のすべてのタイプおよびそれ以上は、帰納型のルールを使用して定義できます。タイプのコンストラクターが指定されると、エリミネーター関数と計算は構造再帰によって決定されます。

タイプを作成するための同様の、より強力な方法があります。これらには、帰納法帰納法が含まれます。スコットエンコーディングと呼ばれるラムダ項のみを使用して同様の型を作成する方法もあります

(注:型理論には通常、共誘導型は含まれません。これらは無限のデータ型を表し、ほとんどの型理論は、停止することが証明できる関数に限定されます。)

集合論との違い

数学の伝統的な基礎は、論理と組み合わせた集合論です。引用されている最も一般的なものは、「ZF」または選択公理では「ZFC」として知られているツェルメロフレンケル集合論です。型理論は、いくつかの点でこの基礎とは異なります。

  • 集合論には規則公理の両方がありますが、型理論には規則しかありません。集合論は論理の上に構築されています。したがって、ZFCは、一階述語論理の規則とそれ自体の公理の両方によって定義されます。公理は、論理的な導出なしに真として受け入れられる論理的なステートメントです。)型理論は、一般に、公理を持たず、推論規則によって定義されます。
  • 集合論と論理には排中律の法則があります。つまり、すべての定理は真または偽です。型理論が「and」と「or」の概念を型として定義するとき、それは、排中律を持たない直観主義論理につながります。ただし、法則は一部のタイプで証明できます。
  • 集合論では、要素は1つの集合に制限されません。要素は、サブセットおよび他のセットとの結合で表示できます。型理論では、用語は(一般的に)1つの型にのみ属します。サブセットが使用される場合、型理論は述語関数を使用するか、依存型の製品タイプを使用できます。ここで、各要素はサブセットのプロパティが保持する証拠とペアになっています共用体が使用される場合、型理論は、新しい正規項を含む合計型を使用します。
  • 型理論には、計算の概念が組み込まれています。したがって、「1 + 1」と「2」は型理論では異なる用語ですが、同じ値で計算されます。さらに、関数は計算上ラムダ項として定義されます。集合論では、「1 + 1 = 2」は、「1 +1」が値「2」を参照する別の方法であることを意味します。型理論の計算には、複雑な平等の概念が必要です。
  • 集合論は通常、数値を集合としてエンコードします。(0は空集合、1は空集合を含む集合など。自然数の集合論的定義を参照してください。)型理論は、教会符号化を使用して関数として、またはより自然に誘導型として数値を符号化できます。誘導型によって作成されたコンストラクター「0」と「S」は、ペアノの公理によく似ています。
  • 集合論には集合の内包的記法があります。定義可能な任意のセットを作成できます。これにより、非可算集合を作成できます。型理論は構文的であり、可算無限の項に制限されます。さらに、ほとんどの型理論では、常に停止し、再帰的に生成可能な項に制限するための計算が必要です。その結果、ほとんどの型理論は実数ではなく計算可能数を使用します。
  • 集合論では、選択公理は公理であり、特に非可算集合に適用される場合は物議を醸します。型理論では、同等のステートメントは定理(タイプ)であり、証明可能です(用語が存在します)。
  • 型理論では、証明は数学的対象です。タイプ「x + 1 = 1 + x」は、タイプの用語がない限り使用できません。その用語は、「x + 1 = 1 + x」という証明を表しています。したがって、型理論は、数学的対象として研究される証明を開きます。

型理論の支持者はまた、 BHK解釈による構成主義数学への接続、カリー・ハワード同形性による論理への接続、および圏への接続を指摘します。

技術的な詳細

型理論は数理論理学です。これは、判断をもたらす推論規則のコレクションですほとんどの論理には、「用語本当です。」または「用語整形式です。」[3]。型理論には、型を定義し、用語を型に関連付ける追加の判断があります。

用語

ロジック内の用語は、定数シンボル、変数、または関数適用として再帰的に定義され、用語は別の用語に適用されます。一部の定数記号は、自然数の「0」、ブール値の「true」であり、「S」や「if」のように機能します。したがって、いくつかの用語は、「0」、「(S 0)」、「(S(S x))」、および「真の場合0(S0)」です。

判断

ほとんどの型理論には4つの判断があります。

  • 「」タイプです。」
  • 「」タイプの用語です。」
  • "タイプタイプと等しい。」
  • "条項どちらもタイプですと等しい。」

判断は仮定の下で行うことができます。したがって、「タイプ「bool」の用語であり、はタイプ「nat」の用語であり、(xyyの場合)はタイプ「nat」の用語です。仮定の数学表記は、回転式改札口記号の前にある「 term  :type 」のコンマ区切りのリストです。'。したがって、サンプルステートメントは正式に次のように記述されます。

  • x:bool、y:nat(xyyの場合):nat

仮定がない場合、改札口の左側には何もありません。

  • S:natnat

仮定のリストは「コンテキスト」と呼ばれます。シンボルを見るのは非常に一般的です ''は、いくつかまたはすべての仮定を表すために使用されます。したがって、4つの異なる判断の正式な表記は通常次のとおりです。

判断のための正式な表記 説明
タイプ タイプです(仮定の下で)。
タイプの用語です(仮定の下で)。
タイプタイプと等しい(仮定の下で)。
条項どちらもタイプですと等しい(仮定の下で)。

(注:用語の平等の判断は、「判断の平等」というフレーズの由来です。)

判決は、すべての用語にタイプがあることを強制します。タイプは、用語に適用できるルールを制限します。

ルール

型理論のルールは、他の判断の存在に基づいて、どのような判断を下すことができるかを示しています。ルールは水平線を使用して表され、必要な入力判断は線の上にあり、結果の判断は線の下にあります。ラムダ項を作成するためのルールは次のとおりです。

ラムダ項を作成するために必要な判断は、境界線を超えています。この場合、必要な判断は1つだけです。あるタイプ「A」のある用語「a」と他のいくつかの仮定があると仮定すると、あるタイプ「B」のある用語「b」があるということです。"。 (ノート: "「 "a"、 "A"、 "b"、および "B"はすべて、ルール内のメタ変数です。)結果の判断は、境界線を下回ります。このルールの結果の判断は、新しいラムダ項のタイプが "A他の仮定の下でのB "

ルールは構文であり、書き換えることで機能します。したがって、「"、" a "、" A "などは、実際には、単一の記号だけでなく、多くの関数アプリケーションを含む複雑な用語で構成されている場合があります。

型理論で特定の判断を生成するには、それを生成するためのルールが必要です。次に、そのルールに必要なすべての入力を生成するルールが必要です。そして、それらのルールのすべての入力のルール。適用されたルールはプルーフツリーを形成します。これは通常、ゲンツェンスタイルで描かれ[4]、ターゲットの判断(ルート)が下部にあり、入力(リーフ)を必要としないルールが上部にあります。Natural_deduction#Proofs_and_type_theoryを参照してください。)入力を必要としないルールの例は、タイプ「nat」の用語「0」があることを示すルールです。

型理論には通常、次のような規則があります。

  • コンテキストを作成する
  • コンテキストに仮定を追加します(「弱体化」)
  • 仮定を再配置する
  • 仮定を使用して変数を作成します
  • 判断の平等のための反射性、対称性、推移性を定義する
  • ラムダ項の適用の置換を定義する
  • 平等、置換などのすべての相互作用。
  • 宇宙を定義する

また、「ルール別」タイプごとに、4種類のルールがあります

  • 「タイプ形成」ルールは、タイプを作成する方法を示します
  • 「用語紹介」ルールは、「ペア」や「S」などの正規用語とコンストラクター関数を定義します。
  • 「用語除去」ルールは、「第1」、「第2」、「R」などの他の機能を定義します。
  • 「計算」ルールは、タイプ固有の関数を使用して計算を実行する方法を指定します。

ルールの例:

型理論の性質

用語は通常、単一のタイプに属します。ただし、「サブタイピング」を定義する集合論があります。

計算は、ルールを繰り返し適用することによって行われます。多くの型理論は強く正規化されています。つまり、ルールを適用する順序は常に同じ結果になります。ただし、そうでないものもあります。正規化型理論では、一方向の計算規則は「削減規則」と呼ばれ、規則を適用すると用語が「削減」されます。ルールが一方向でない場合、それは「変換ルール」と呼ばれます。

タイプのいくつかの組み合わせは、他のタイプの組み合わせと同等です。関数が「べき乗」と見なされる場合、型の組み合わせは代数単位元と同様に記述できます。[5] したがって、

公理

ほとんどの型理論には公理がありませんこれは、型理論が推論規則によって定義されているためです。(上記の「ルール」を参照してください)。これは、集合論に精通している人々にとって混乱の原因です。集合論では、論理(一階述語論理など)の推論規則と集合に関する公理の両方によって理論が定義されます。

時々、型理論はいくつかの公理を追加します。公理は、推論規則を使用して導出せずに受け入れられる判断です。これらは、ルールを介してクリーンに追加できないプロパティを確保するために追加されることがよくあります。

公理は、それらの用語を計算する方法なしに用語を導入する場合、問題を引き起こす可能性があります。つまり、公理は型理論の正規化特性に干渉する可能性があります。[6]

一般的に遭遇する公理は次のとおりです。

  • 「AxiomK」は「アイデンティティ証明の一意性」を保証します。つまり、アイデンティティタイプのすべての項は再帰性に等しいということです。[7]
  • 「UnivalentAxiom」は、型の同等性は型の同等性であると考えています。この性質の研究は、公理を必要とせずに性質が成り立つ立方型理論につながりました。[8]
  • 「排中律」は、直観主義論理ではなく、古典論理を求めるユーザーを満足させるために追加されることがよくあります。

ほとんどの型理論では推論規則から導き出すことができるため、選択公理を型理論に追加する必要はありません。これは、値が存在することを証明するには値を計算する方法が必要な型理論の建設的な性質によるものです。選択公理は、型理論の関数が計算可能でなければならず、構文駆動型であるため、型の用語の数が数えられなければならないため、ほとんどの集合論よりも型理論では強力ではありません。Axiom_of_choice#In_constructive_mathematicsを参照してください。)

決定問題

型理論は、当然、住性の決定問題と関連してます。[9]

住性

住性の決定問題(略し) は:

与えられたタイプの環境とタイプ、用語が存在するかどうかを判断しますタイプを割り当てることができますタイプ環境で

ジラールのパラドックスは、住性がカリー・ハワード対応の型システムの一貫性と強く関連していることを示しています。健全であるためには、そのようなシステムは無人のタイプを持たなければなりません。

用語とタイプの反対は、実装仕様の1つと見なすこともできますプログラム合成(の計算上の対応物)によって、住性(以下を参照)を使用して、型情報の形式で与えられた仕様からプログラム(のすべてまたは一部)を構築できます。[10]

型推論

型理論で動作する多くのプログラム(たとえば、対話型定理証明者)も型推論を行います。これにより、ユーザーによるアクションを減らして、ユーザーが意図するルールを選択できます。

研究分野

ホモトピー型理論は、主に等式型の取り扱いによって直観主義型理論とは異なります。最近、正規化を伴うホモトピー型理論である「キュービカル型理論」が提案されています。

型理論の解釈

型理論は数学の他の分野と関係があります。基礎としての型理論の支持者は、しばしばこれらの接続をその使用の正当化として言及します。

タイプは命題です。用語は証明です

基礎として使用される場合、特定のタイプは命題(証明できるステートメント)として解釈され、タイプの用語はその命題の証明です。したがって、タイプ「Πx:nat .x + 1 = 1 + x」は、タイプ「nat」の任意の「x」に対して、「x +1」と「1 + x」が等しいことを表します。そして、そのタイプの用語はその証拠を表しています。

カリーハワード対応

カリーハワード対応は、論理とプログラミング言語の間で観察された類似性です。論理における含意、「AB "は、タイプ" A "からタイプ" B "の関数に似ています。さまざまなロジックで、ルールはプログラミング言語のタイプの式に似ています。ルールの適用はプログラミングのプログラムに似ているため、類似性はさらに高まります。したがって、対応は「プログラムとしての証明」として要約されることがよくあります。

「すべての」および「存在する」という論理演算子により、PerMartin-Löfは依存型理論を発明しました。

直観主義論理

一部の型が命題として解釈される場合、それらを接続して型からロジックを作成するために使用できる一連の一般的な型があります。ただし、その論理は古典論理ではなく、直観主義論理です。つまり、排中律二重否定もありません。

型と論理命題には自然な関係があります。「A」が命題を表す型である場合、「型」の関数を作成できるA」は、Aに証明があり、関数「A」を作成できることを示します。「Aには証拠がないことを示します。つまり、居住可能なタイプは証明され、居住不可能なタイプは反証されます。

警告:この解釈は多くの混乱を招く可能性があります。型理論には、ブール論理のように機能する「bool」型の「true」と「false」という用語があり、同時に型があります。 命題の直観主義論理の一部として、「真」(証明可能)と「偽」(反証)を表すこと。

この直感的な解釈の下で、論理演算子として機能する一般的なタイプがあります。

ロジック名 論理表記 タイプ表記 タイプ名
ユニット型
誤り 空のタイプ
いいえ タイプを空にする関数
含意 関数
製品型
または 合計タイプ
すべてのために Πa:A。P(a) 依存関数
存在する Σa:A。P(a) 依存製品タイプ

しかし、この解釈の下では、排中律の法則はありません。つまり、タイプΠAの用語はありません。A +(A)。

同様に、二重否定はありません。タイプΠAの用語はありません。((A)。)。A.(注:直観主義論理は許可しますタイプの用語があります(((A)。)。)。(A)。)

したがって、型の論理は直観主義論理です。型理論は、 Brouwer–Heyting–Kolmogorov解釈の実装としてよく引用されます。

規則または仮定により、排中律と二重否定の法則を型理論に含めることができます。ただし、項は正規の項まで計算されない場合があり、2つの項が互いに判断的に等しいかどうかを判断する機能に干渉します。

構成数学

ペール・マルティン=レーフは、構成主義数学の基礎として彼の直観的型理論を提案しました構成主義の数学は、「存在するプロパティP()」、特定の必要がありますそしてそれが特性「P」を持っているという証拠。型理論では、存在は依存する製品タイプを使用して達成され、その証明には、そのタイプの用語が必要です。期間中、 "最初"を生成しますと「2番目"はP(の証明を生成します)。

非構成的証明の例は、「矛盾による証明」です。最初のステップは、存在せず、矛盾して反駁している。そのステップからの結論は、「そうではない最後のステップは、二重否定によって、次のように結論付けます。存在します。明確にするために、構成主義の数学はまだ「矛盾による反論」を可能にします。「そうではないことを証明することができます存在しません」。しかし、構成主義の数学では、二重否定を削除する最後のステップで次のように結論付けることはできません。存在します。[11]

構成主義数学は、 Brouwer-Heyting-Kolmogorovの解釈によって証明されるように、しばしば直感的な論理を使用してきました

基礎として提案された型理論のほとんどは建設的です。これには、証明アシスタントが使用するもののほとんどが含まれます。

ルールまたは仮定によって、型理論に非構成的特徴を追加することが可能です。これらには、現在の継続を使用した呼び出しなどの継続の演算子が含まれますただし、これらの演算子は、カノニシティパラメトリシティなどの望ましいプロパティを壊す傾向があります

圏論

圏論の最初の動機は基礎主義からはほど遠いものでしたが、2つの分野は深いつながりを持っていることが判明しました。ジョン・レーン・ベルが書いているように、「実際、カテゴリー自体特定の種類の型理論と見なすことができます。この事実だけでも、型理論は集合論よりも圏論とはるかに密接に関連していることを示しています。」簡単に言えば、カテゴリは、そのオブジェクトを型(またはソート)と見なすことによって型理論と見なすことができます。つまり、「大まかに言えば、カテゴリは、その構文の一部である型理論と見なすことができます」。このようにして、いくつかの重要な結果が得られます。[12]

それ以来、内部言語として知られる相互作用は活発研究の対象となっています。たとえば、ジェイコブス(1999)のモノグラフを参照してください。

ホモトピー型理論は、型理論と圏論を組み合わせようとします。平等、特にタイプ間の平等に焦点を当てています。

型理論のリスト

メジャー

マイナー

アクティブリサーチ

アプリケーション

数学的基礎

Automathと呼ばれる最初のコンピューター証明アシスタントは、型理論を使用してコンピューター上で数学をエンコードしました。Martin-Löfは、数学の新しい基礎として機能するようにすべての数学をエンコードする直感的な型理論を特別に開発しました。ホモトピー型理論を用いた数学的基礎の研究が進行中です。

圏論で働く数学者は、ツェルメロ・フレンケル集合論の広く受け入れられている基礎を扱うのにすでに苦労していましたこれは、集合の圏のローヴェアの初等理論(ETCS)などの提案につながりました。[13]ホモトピー型理論は、型理論を使用してこの行に続きます。研究者は、依存型(特にアイデンティティ型)と代数トポロジー(特にホモトピー)の間の関係を調査しています。

証明アシスタント

型理論に関する現在の研究の多くは、証明チェッカー、対話型証明アシスタント、および自動定理証明者によって推進されています。これらのシステムのほとんどは、型理論とプログラミング言語の密接な関係を考えると、証明をエンコードするための数学的基礎として型理論を使用しますが、これは驚くべきことではありません。

多くの型理論がLEGOIsabelleによってサポートされています。Isabelleは、 ZFCなどの型理論以外の基礎もサポートしています。Mizarは、集合論のみをサポートする証明システムの例です。

プログラミング言語

型理論と型システムの分野の間には、広範な重複と相互作用があります。型システムは、バグを特定するために設計されたプログラミング言語機能です。コンパイラのセマンティック分析フェーズでの型チェックアルゴリズムなどの静的プログラム分析は、型理論と関係があります。

代表的な例は、型システムにUTT(Luoの依存型の統一理論)を使用するプログラミング言語であるAgdaです。プログラミング言語MLは、型理論を操作するために開発され(LCFを参照)、独自の型システムはそれらの影響を強く受けていました。

言語学

型理論は、自然言語の意味論、特にモンタギュー文法とその子孫の形式理論でも広く使用されています。特に、範疇文法プレグループ文法は、型構築子を広く使用して、単語の型(名詞動詞など) を定義します。

最も一般的な構造は基本的なタイプを取りますそれぞれ、個人と真理値に対して、次のように再帰的に型のセットを定義します。

  • もしもタイプです、そしてそうです;
  • 基本型以外は何もありません。前の節でそれらから構築できるのは型です。

複合型タイプのエンティティからの関数のタイプですタイプのエンティティにしたがって、次のようなタイプがありますこれは、エンティティから真理値までの関数のセットの要素、つまりエンティティのセットのインジケーター関数として解釈されます。タイプの式は、エンティティのセットから真理値への関数、つまり(aのインジケーター関数)セットのセットです。この後者のタイプは、標準的に、誰もがそうであるように、自然言語の数量詞のタイプであると見なされますMontague 1973Barwise and Cooper1981

社会科学

グレゴリー・ベイトソンは、論理型の理論を社会科学に導入しました。彼のダブルバインド論理レベルの概念は、ラッセルの型理論に基づいています。

も参照してください

外部リンク

紹介資料

Advanced Material

  • ロバートL.コンスタブル(編)。「計算型理論」スカラーペディア
  • TYPESフォーラム—コンピュータサイエンスの型理論に焦点を当てたモデレートされた電子メールフォーラムで、1987年から運営されています。
  • Nuprl Book:「型理論入門」 。
  • タイプ2005〜2008年のサマースクールの プロジェクト講義ノート
  • オレゴンプログラミング言語サマースクール、多くの講義といくつかのメモ。
  • アンドレイ・バウアーのブログ

さらに読む

参考文献

  1. ^ スタンフォード哲学百科事典 (2020年10月12日月曜日改訂)ラッセルのパラドックス3.パラドックスへの初期の対応
  2. ^ 教会、アロンゾ(1940)。「型の単純な理論の定式化」。シンボリックロジックのジャーナル5(2):56–68。土井10.2307 / 2266170JSTOR2266170_ 
  3. ^ バウアー、アンドレイ。「判決とは正確には何ですか?」mathoverflow 2021年12月29日取得
  4. ^ スミス、ピーター。「証明システムの種類」(PDF)logicmatters.net 2021年12月29日取得
  5. ^ ミレフスキー、バルトス。「数学によるプログラミング(型理論の探求)」YouTube
  6. ^ 「公理と計算」リーンで証明する定理2022年1月21日取得
  7. ^ 「公理K」nLab
  8. ^ コーエン、シリル; コカンド、ティエリー; フーバー、サイモン; Mörtberg、Anders(2016)。「立方型理論:一価公理の建設的な解釈」(PDF)非常に重要なトピックに関する第42回会議土井10.4230 /LIPIcs.CVIT.2016.23
  9. ^ ヘンクバレンドレッグ; ウィルデッカーズ; リチャードスタットマン(2013年6月20日)。タイプのラムダ計算ケンブリッジ大学出版局。p。66. ISBN 978-0-521-76614-2
  10. ^ ハイネマン、ジョージT。; ベッサイ、1月; Düdder、Boris; Rehof、Jakob(2016)。「モジュラーシンセシスへの長く曲がりくねった道」。正式な方法、検証および妥当性確認のアプリケーションの活用:基本的な手法ISoLA2016。コンピュータサイエンスの講義ノート。9952.スプリンガー。pp。303–317。土井10.1007 / 978-3-319-47166-2_21
  11. ^ 「矛盾による証明」nlab 2021年12月29日取得
  12. ^ ベル、ジョンL.(2012)。「タイプ、セット、およびカテゴリー」(PDF)カナモリーでは、アキヒロ(編)。20世紀のセットと拡張論理学の歴史のハンドブック。6.エルゼビア。ISBN  978-0-08-093066-4
  13. ^ nLabETCS