「型付きラムダ計算」の版間の差分

削除された内容追加された内容

インライン

2023年8月7日 (月) 06:18時点における最新版

型付きラムダ計算（かたつきラムダけいさん、英: typed lambda calculus）とは、無名の関数の抽象表現にラムダ ( $\lambda$ ) というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。

ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。

様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型 $\sigma \to \tau$ から成る。System T はこれを拡張し、自然数型と高階原始再帰を加えたものである。この系ではペアノ算術において全ての再帰する可能性のある関数が定義可能である。System F は、全ての型に対して全称量化を施すことでポリモーフィズムを実現している。これを論理学的に見れば、二階述語論理に属する全ての関数を記述できることを意味する。依存型のあるラムダ計算は直観主義的型理論の基盤であり、calculus of constructions や logical framework (LF) の基盤である。Berardi の成果に基づき Barendregt が提案したラムダ・キューブは、純粋な型付きラムダ計算（単純型付きラムダ計算、System F、LF、calculus of constructions など）の関係を体系化したものである。

一部の型付きラムダ計算には「サブタイピング」の概念が導入されている。すなわち、 $A$ が $B$ のサブタイプ（下位型）であるとき、 $A$ 型の項は必ず $B$ 型の項でもある。サブタイピングのある型付きラムダ計算としては、単純型付きラムダ計算に conjunctive type を加えたものと System F-sub（英語版） (F_<:) が挙げられる。

以上の体系はすべて（型のないラムダ計算以外）、「強く正規化 (strongly normalizing)」する。すなわち、全ての計算は停止する。結果としてそれらは論理として一貫しており、uninhabited types がある。しかし、強く正規化しない型付きラムダ計算も存在する。全ての型の型 (Type : Type) を持つ依存型付きラムダ計算は Girard's paradox により正規化しない。この系は最も単純な純粋型システムでもあり、ラムダ・キューブを一般化した形式手法である。明示的な再帰コンビネータを持つ系（Gordon Plotkin の PCF など）も正規化しないが、論理体系として解釈されることを意図していない。実際、PCF (Programming language for Computable Functions) は型付き関数型プログラミング言語であり、型はプログラムが正しく動作することを保証する目的で使われているが、必ずしも停止を保証しない。

型付きラムダ計算はプログラミング言語の新たな型システムの設計で重要な役割を演じている。型付け可能性は一般にプログラミングの好ましい属性を捉え、例えば、プログラムがメモリアクセス違反を起こさないようにするといったことが考えられる。

プログラミングにおいて、強い型付けのプログラミング言語のルーチン（関数、プロシージャ、メソッド）は、型付きラムダ計算と密接に関連している。Eiffelには "inline agent" の記法があり、型付きラムダ式を直接定義して操作できる。例えば、agent (p: PERSON): STRING do Result := p.spouse.name end という式があるとき、これはある人 (person) の配偶者 (spouse) の名前を返す関数を表したオブジェクトを記述している。

参考文献

Henk Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, Volume II, Oxford University Press.

@@ 1行目: / 1行目: @@
-'''型付きラムダ計算'''（{{lang-en-short|typed lambda calculus}}）とは、無名の関数の抽象表現にラムダ (<math>\lambda</math>) というシンボルを用いる型付き[[形式手法]]である。型付きラムダ計算は基礎的な[[プログラミング言語]]でもあり、[[ML (プログラミング言語)|ML]]や[[Haskell]]などの型付き[[関数型言語]]の基盤であり、さらには型付き[[命令型プログラミング]]言語の間接的な基盤とも言える。また、[[カリー・ハワード同型対応]]によって[[数理論理学]]と[[証明論]]とも密接に関連しており、[[圏論]]のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算は[[デカルト閉圏]] (CCC) の言語である。
+'''型付きラムダ計算'''（かたつきラムダけいさん、{{lang-en-short|typed lambda calculus}}）とは、無名の関数の抽象表現にラムダ (<math>\lambda</math>) というシンボルを用いる型付き[[形式手法]]である。型付きラムダ計算は基礎的な[[プログラミング言語]]でもあり、[[ML (プログラミング言語)|ML]]や[[Haskell]]などの型付き[[関数型言語]]の基盤であり、さらには型付き[[命令型プログラミング]]言語の間接的な基盤とも言える。また、[[カリー・ハワード同型対応]]によって[[数理論理学]]と[[証明論]]とも密接に関連しており、[[圏論]]のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算は[[デカルト閉圏]] (CCC) の言語である。
 ある観点から見れば、型付きラムダ計算は型を持たない[[ラムダ計算]]を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。
-様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型 <math>\sigma\to\tau</math> から成る。System T はこれを拡張し、自然数型と高階原始再帰を加えたものである。この系では[[ペアノの公理|ペアノ算術]]において全ての再帰する可能性のある関数が定義可能である。System F は、全ての型に対して[[全称記号|全称量化]]を施すことで[[ポリモーフィズム]]を実現している。これを論理学的に見れば、[[二階述語論理]]に属する全ての関数を記述できることを意味する。[[依存型]]のあるラムダ計算は[[直観主義的型理論]]の基盤であり、[[:en:calculus of constructions|calculus of constructions]] や [[:en:LF (logical framework)|logical framework]] (LF) の基盤である。Berardi の成果に基づき Barendregt が提案した[[ラムダ・キューブ]]は、純粋な型付きラムダ計算（単純型付きラムダ計算、System F、LF、calculus of constructions など）の関係を体系化したものである。
+様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型 <math>\sigma\to\tau</math> から成る。[[System T]] はこれを拡張し、自然数型と高階原始再帰を加えたものである。この系では[[ペアノの公理|ペアノ算術]]において全ての再帰する可能性のある関数が定義可能である。[[System F]] は、全ての型に対して[[全称記号|全称量化]]を施すことで[[ポリモーフィズム]]を実現している。これを論理学的に見れば、[[二階述語論理]]に属する全ての関数を記述できることを意味する。[[依存型]]のあるラムダ計算は[[直観主義的型理論]]の基盤であり、[[:en:calculus of constructions|calculus of constructions]] や [[:en:LF (logical framework)|logical framework]] (LF) の基盤である。Berardi の成果に基づき Barendregt が提案した[[ラムダ・キューブ]]は、純粋な型付きラムダ計算（単純型付きラムダ計算、System F、LF、calculus of constructions など）の関係を体系化したものである。
-一部の型付きラムダ計算には「[[派生型]]」の記法が導入されている。すなわち、<math>A</math> が <math>B</math> の派生型であるとき、型が <math>A</math> である全ての項は型が <math>B</math> でもある。派生型のある型付きラムダ計算は単に普通の型付きラムダ計算に結合型 (conjunctive type) と <math>F^\leq</math> (F-sub) を加えたものである。
+一部の型付きラムダ計算には「[[サブタイピング (計算機科学)|サブタイピング]]」の概念が導入されている。すなわち、<math>A</math> が <math>B</math> のサブタイプ（下位型）であるとき、<math>A</math>型の項は必ず<math>B</math>型の項でもある。サブタイピングのある型付きラムダ計算としては、単純型付きラムダ計算に conjunctive type <!-- 結合型 ←この訳で合ってる? 積型 ? -->を加えたものと {{仮リンク|System F-sub|en|System F-sub}} (F<sub><:</sub>) が挙げられる。
 以上の体系はすべて（型のないラムダ計算以外）、「強く正規化 (strongly normalizing)」する。すなわち、全ての計算は停止する。結果としてそれらは論理として一貫しており、uninhabited types がある。しかし、強く正規化しない型付きラムダ計算も存在する。全ての型の型 (Type : Type) を持つ依存型付きラムダ計算は Girard's paradox により正規化しない。この系は最も単純な[[純粋型システム]]でもあり、ラムダ・キューブを一般化した形式手法である。明示的な再帰コンビネータを持つ系（Gordon Plotkin の PCF など）も正規化しないが、論理体系として解釈されることを意図していない。実際、PCF ([[:en:Programming_language_for_Computable_Functions|Programming language for Computable Functions]]) は型付き関数型プログラミング言語であり、型はプログラムが正しく動作することを保証する目的で使われているが、必ずしも停止を保証しない。