システムF

システムF（多相ラムダ計算または二階ラムダ計算とも呼ばれる）は、単純な型付きラムダ計算に、型に対する普遍量化のメカニズムを導入した型付きラムダ計算である。システムFはプログラミング言語におけるパラメトリック多相性を形式化し、 HaskellやMLなどの言語の理論的基盤を形成している。これは、論理学者のジャン＝イヴ・ジラール（1972年）とコンピュータ科学者のジョン・C・レイノルズによってそれぞれ独立に発見された。

単純な型付きラムダ計算では、変数は項の範囲をカバーし、それらのバインダーも存在しますが、System F ではさらに変数は型の範囲をカバーし、それらのバインダーも存在します。例えば、恒等関数がA → Aの形式の任意の型を持つことができるという事実は、System F では次の文として形式化されます。

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

どこ${\displaystyle \alpha }$は型変数です。大文字${\displaystyle \Lambda }$は、小文字の とは対照的に、型レベルの関数を表すために伝統的に使用されます。${\displaystyle \lambda }$値レベルの関数に使用されます。（上付き文字${\displaystyle \alpha }$これは、束縛変数xが型であることを意味します。${\displaystyle \alpha }$（コロンの後の式は、その前のラムダ式の型です。）

項書き換えシステムとして、System F は強力な正規化機能を備えています。ただし、System F における型推論（明示的な型注釈なし）は決定不能です。Curry –Howard の同型性の下では、System Fは二階直観主義命題論理に対応します。System F は、依存型を持つものを含む、さらに表現力豊かな型付きラムダ計算とともに、ラムダキューブの一部と見なすことができます。

ジラールによれば、システムFの「F」は偶然選ばれたものだという。^{[ 1 ]}

System F の型付け規則は、単純な型付きラムダ計算の規則に以下の規則を追加したものです。

どこ${\displaystyle \sigma ,\tau }$種類は、${\displaystyle \alpha }$は型変数であり、${\displaystyle \alpha ~{\text{type}}}$文脈上、${\displaystyle \alpha }$拘束されている。第一の規則は適用規則であり、第二の規則は抽象化規則である。^{[ 2 ] [ 3 ]}

の$\displaystyle {\mathsf {ブール値}}}$型は次のように定義されます。 ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$、 どこ${\displaystyle \alpha }$これは型変数です。つまり、次のようになります。$\displaystyle {\mathsf {ブール値}}}$は、型αと 2 つの型αの式を入力として受け取り、型αの式を出力するすべての関数の型です( を考慮すると、${\displaystyle \to }$右結合である。）

ブール値に関する以下の2つの定義${\displaystyle \mathbf {T} }$そして${\displaystyle \mathbf {F} }$チャーチブールの定義を拡張して使用される。

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

（上記の 2 つの関数は、2 つではなく 3 つの引数を必要とすることに注意してください。後者2つ はラムダ式である必要がありますが、最初の引数は型である必要があります。この事実は、これらの式の型が次のようになっているという事実に反映されています。）${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$; αを束縛する全称量化子は、ラムダ式自体の α を束縛するΛに対応します。また、次の点にも注意してください。$\displaystyle {\mathsf {ブール値}}}$は、${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$しかし、それはシステムF自体のシンボルではなく、「メタシンボル」である。同様に、${\displaystyle \mathbf {T} }$そして${\displaystyle \mathbf {F} }$これらはまた、System Fの「アセンブリ」（ブルバキの意味で）の便利な略記法である「メタシンボル」でもある。そうでなければ、もしそのような関数に（System F内で）名前を付けることができたなら、関数を匿名で定義できるラムダ表現装置や、その制約を回避するための固定小数点コンビネータは不要になるだろう。

そして、この2つで${\displaystyle \lambda }$-用語では、いくつかの論理演算子（型）を定義できます${\displaystyle {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}}$):

${\displaystyle {\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {ブール値}}\lambda y^{\mathsf {ブール値}}{.}x\,{\mathsf {ブール値}}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {ブール値}}\lambda y^{\mathsf {ブール値}}{.}x\,{\mathsf {ブール値}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {ブール値}}{.}x\,{\mathsf {ブール値}}\,\mathbf {F} \,\mathbf {T} \end{aligned}}}$

上記の定義では、$\displaystyle {\mathsf {ブール値}}}$は型引数です${\displaystyle x}$に与えられる他の 2 つのパラメータを指定します${\displaystyle x}$の型$\displaystyle {\mathsf {ブール値}}}$Church エンコーディングと同様に、生の値をそのまま使用できるため、IFTHENELSE関数は必要ありません。$\displaystyle {\mathsf {ブール値}}}$決定関数として型付けされた項。ただし、要求された場合は：

${\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

それでいいです。述語は、$\displaystyle {\mathsf {ブール値}}}$-型の値。最も基本的な述語はISZEROで、これは${\displaystyle \mathbf {T} }$引数が教会数0である場合に限り、

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

さらに、存在量化子（および存在型）は、システム F で次のように実装できます。^{[ 4 ] [ 5 ]}

${\displaystyle \exists X.A=\forall Y.(\forall X.A\rightarrow Y)\rightarrow Y}$

システムFは、 Martin-Löfの型理論と同様に、再帰構造を自然な形で埋め込むことを可能にする。抽象構造（S ）はコンストラクタを用いて作成される。これらは次のように型付けされた関数である。

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$。

再帰性は、 S自体が型のいずれかの中に現れるときに現れる。${\displaystyle K_{i}}$これらのコンストラクタがm個ある場合、 Sの型を次のように定義できます。

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

例えば、自然数はコンストラクタを持つ帰納的データ型Nとして定義できる。

${\displaystyle {\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}}$

この構造に対応するシステムFタイプは ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$この種の用語は、教会数字のタイプ版で構成されており、最初の数個は以下のとおりです。

${\displaystyle {\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}}$

カリー化された引数の順序を逆にすると（つまり、${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$) の場合、 nのチャーチ数は、関数f を引数として受け取り、fのn^乗を返す関数です。つまり、チャーチ数は高階関数であり、1 つの引数を持つ関数fを受け取り、別の 1 つの引数を持つ関数を返します。

本稿で使用されている System F のバージョンは、明示的に型付けされた、つまり Church スタイルの計算体系です。λ 項に含まれる型情報により、型チェックは容易になります。Joe Wells (1994)は、明示的な型注釈のない、Curry スタイルの System F の変種では型チェックが決定不能であることを証明することで、「厄介な未解決問題」を解決しました。 ^{[ 6 ] [ 7 ]}

ウェルズの結果は、 System F の型推論が不可能であることを示唆しています。System F の制限である「Hindley–Milner」、または単に「HM」は、簡単な型推論アルゴリズムを持ち、Haskell 98やMLファミリーなどの多くの静的型付け関数型プログラミング言語で使用されています。時間の経過とともに、HM スタイルの型システムの制限が明らかになるにつれて、言語は型システムに対してより表現力豊かな論理へと着実に移行してきました。HaskellコンパイラであるGHC は、(2008 年現在) HM を超え、非構文型等価性で拡張された System F を使用しています。^{[ 8 ]} OCamlの型システムの HM 以外の機能にはGADTが含まれます。^{[ 9 ] [ 10 ]}

2階直観主義論理では、2階多相ラムダ計算 (F2) は Girard (1972) と Reynolds (1974) によって独立に発見されました。^{[ 11 ]} Girard は表現定理を証明しました。2階直観主義述語論理 (P2) では、自然数から自然数への関数で全射であることが証明できるものは、P2 から F2 への射影を形成します。^{[ 11 ]} Reynolds は抽象化定理を証明しました。F2 のすべての項は論理関係を満たし、その論理関係は P2 の論理関係に埋め込むことができます。^{[ 11 ]} Reynolds は、Girard 射影に続いて Reynolds 埋め込みを行うと恒等写像、すなわちGirard–Reynolds 同型写像が形成されることを証明しました。^{[ 11 ]}

システムFはバレンデレヒトのラムダキューブの第一軸に対応するが、システムFω _、すなわち高階多相ラムダ計算は、第一軸（多相）と第二軸（型演算子）を組み合わせたものであり、より複雑な異なるシステムである。

システム F _{ω は}、各システムで許容される種類に基づいて帰納的に定義されるシステムの族上で定義することができる。

• ${\displaystyle F_{n}}$許可の種類:
  • ${\displaystyle \star }$（種類の）そして
  • ${\displaystyle J\Rightarrow K}$どこ${\displaystyle J\in F_{n-1}}$そして${\displaystyle K\in F_{n}}$（型から型への関数の一種で、引数の型はより低い階数である）

極限では、システムを定義できます${\displaystyle F_{\omega }}$である

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

つまり、Fω_は、引数（および結果）の次数が任意の型であっても、型から型への関数を可能にするシステムである。

F _ωはこれらのマッピングの引数の順序に制限を設けませんが、これらのマッピングの引数のユニバースには制限を設けます。引数は値ではなく型でなければなりません。システム F _{ω は}値から型へのマッピング (依存型) を許可しませんが、値から値へのマッピング (${\displaystyle \lambda }$抽象化）、型から値へのマッピング（${\displaystyle \Lambda }$抽象化）、および型から型へのマッピング（${\displaystyle \lambda }$型レベルでの抽象化）。

System F _{< :} （「F-sub」と発音）は、サブタイピングを備えた System F の拡張です。System F _{< :は、1980 年代以降、}プログラミング言語理論において中心的な重要性を持ってきました。これは、 MLファミリーなどの関数型プログラミング言語の中核が、 System F _{< :}で表現できるパラメトリック多相性とレコードサブタイピングの両方をサポートしているためです。^{[ 12 ] [ 13 ]}

• 存在型​​― 普遍型の存在量化された対応物
• システムU
• ラムダキューブ

• ピアース、ベンジャミン（ 2002）。「V 多相性 第23章 普遍型、第25章 システムFのML実装」。『型とプログラミング言語』。MIT Press。pp. 339–362、381–388。ISBN  0-262-16209-1。

• フランク・ビナールによるシステムFの概要。
• System Fω _：現代コンパイラの主力システム（グレッグ・モリセット著）