Framework in lambda calculus
ラムダキューブ。矢印の方向が包含方向です。 数理論理学 と 型理論 において 、 λキューブ （ ラムダキューブとも表記される）は、 ヘンク・バレンドレト [1] によって導入された枠組みであり、 単純型付きλ計算 の一般化である 構成計算 の様々な次元を調査するものである。キューブの各次元は、項と型の間の新しい種類の依存関係に対応する。ここで「依存関係」とは、項または型が別の項または型 を束縛する 能力を指す 。λキューブの各次元は、以下のものに対応する。
x 軸 ( ): 項に依存できるタイプ。 依存タイプ に対応します。 → {\displaystyle \rightarrow } y軸（ ）： 多態性 に対応する、型に依存できる項 。 ↑ {\displaystyle \uparrow } z軸（ ）：他の型に依存できる型。（結合） 型演算子 に対応します。 ↗ {\displaystyle \nearrow } これら3つの次元を様々な方法で組み合わせることで、立方体の8つの頂点が生成され、それぞれが異なる種類の型付きシステムに対応します。λキューブは、 純粋型システム の概念に一般化できます。
システムの例
(λ→) 単純に型付けされたラムダ計算 λキューブに見られる最も単純なシステムは、 単純型ラムダ計算 （λ→とも呼ばれる）である。このシステムでは、抽象化を構築する唯一の方法は、 項を項に依存させる ことであり、その 型付け規則は以下 の通りである。
Γ , x : σ ⊢ t : τ Γ ⊢ λ x . t : σ → τ {\displaystyle {\frac {\Gamma ,x:\sigma \;\vdash \;t:\tau }{\Gamma \;\vdash \;\lambda x.t:\sigma \to \tau }}}
(λ2) システムF システムF （「2階型付きラムダ計算」からλ2とも呼ばれる） [2] には 、 で記述される別のタイプの抽象化があり、 次の規則に従って、 項が型 に依存できる ようにします。 Λ {\displaystyle \Lambda }
Γ ⊢ t : σ Γ ⊢ Λ α . t : Π α . σ if α does not occur free in Γ {\displaystyle {\frac {\Gamma \;\vdash \;t:\sigma }{\Gamma \;\vdash \;\Lambda \alpha .t:\Pi \alpha .\sigma }}\;{\text{ if }}\alpha {\text{ does not occur free in }}\Gamma }
a で始まる用語は 多態的 と呼ばれます。これは、 ML系言語 における多態的関数と同様に、異なる型に適用することで異なる関数が得られるためです 。例えば、多態的恒等式は Λ {\displaystyle \Lambda }
OCaml の 型は
つまり、任意の型の引数を取り 'a、その型の要素を返すことができます。この型はλ2において型 に対応します 。 Π α . α → α {\displaystyle \Pi \alpha .\alpha \to \alpha }
(λ ω ) システムF ω システムFでは、 他の型に依存する型 を提供するための構文が導入されています。これは 型コンストラクタ と呼ばれ、「型を 値 として持つ関数」を構築する方法を提供します 。 [3] このような型コンストラクタの例としては、 与えられた型のデータでラベル付けされた葉を持つ二分木の型があります。 ここで、「 」は非公式には「 は型である」という意味です。これは、型パラメータを 引数として取り、 型の値の型を返す 関数です 。具体的なプログラミングでは、この機能は、型コンストラクタをプリミティブとしてではなく、言語内で定義する機能に対応しています。前述の型コンストラクタは、OCamlにおけるラベル付けされた葉を持つ木の次の定義にほぼ対応しています ω _ {\displaystyle {\underline {\omega }}} A {\displaystyle A} T R E E := λ A : ∗ . Π B . ( A → B ) → ( B → B → B ) → B {\displaystyle {\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B} A : ∗ {\displaystyle A:*} A {\displaystyle A} A {\displaystyle A} T R E E {\displaystyle {\mathsf {TREE}}} A {\displaystyle A}
タイプ ' a tree = | ' a の 葉 | ' a tree の ノード * ' a tree この型コンストラクタは他の型に適用して新しい型を取得できます。例えば、整数のツリーの型を取得するには次のようにします。
システムF は単独で使用されることは通常ありませんが、型コンストラクタの独立した機能を分離するのに役立ちます。 [4] ω _ {\displaystyle {\underline {\omega }}}
(λP) ラムダP LF論理フレームワーク と密接に関連する λP システム（λΠとも呼ばれる）には、 いわゆる 依存型 があります。これらは 項に依存できる型 です。このシステムの重要な導入規則は、
Γ , x : A ⊢ B : ∗ Γ ⊢ ( Π x : A . B ) : ∗ {\displaystyle {\frac {\Gamma ,x:A\;\vdash \;B:*}{\Gamma \;\vdash \;(\Pi x:A.B):*}}}
ここで、 は 有効な型を表します。新しい型構築子は、 カリー＝ハワード同型性 を介して 全称量化子に対応し、システム λP 全体は、含意を結合子としてのみ 持つ一階述語論理 に対応します。具体的なプログラミングにおけるこれらの依存型の例としては、特定の長さのベクトルの型が挙げられます。長さは項であり、型はそれに依存します。 ∗ {\displaystyle *} Π {\displaystyle \Pi }
(λω) システムFω システムFωは 、システムFの構築子とシステムFの型構築子の 両方を組み合わせたものです 。
したがって、システムFωは 型に依存する項 と 型に依存する型の 両方を提供します Λ {\displaystyle \Lambda } ω _ {\displaystyle {\underline {\omega }}}
(λC) 構成の計算 構成計算（ 立方体 ではλC、あるいはλPωと表記される） [1] : 130 において、これら4つの特徴は共存し、型と項はどちらも型と項に依存できる。λ→ において項と型の間に存在する明確な境界は、普遍型を除くすべての型が それ自体型を持つ項であるため、ある程度消滅している。 ◻ {\displaystyle \square }
単純型付きラムダ計算に基づくすべてのシステムと同様に、キューブ内のすべてのシステムは2つのステップで与えられます。まず、生の項と β-縮約 の概念、次にそれらの項を型付けすることを可能にする型付け規則です
ソートの集合は と定義され 、ソートは文字 で表されます 。また、変数の集合も存在し 、文字 で表されます 。キューブの8つのシステムの生の項は、次の構文で与えられます。 S := { ∗ , ◻ } {\displaystyle S:=\{*,\square \}} s {\displaystyle s} V {\displaystyle V} x , y , … {\displaystyle x,y,\dots }
A := x ∣ s ∣ A A ∣ λ x : A . A ∣ Π x : A . A {\displaystyle A:=x\mid s\mid A~A\mid \lambda x:A.A\mid \Pi x:A.A}
および が で 自由に発生しない 場合 を示します 。 A → B {\displaystyle A\to B} Π x : A . B {\displaystyle \Pi x:A.B} x {\displaystyle x} B {\displaystyle B}
環境は、型付きシステムでは通常、次のように与えられる。 Γ := ∅ ∣ Γ , x : A {\displaystyle \Gamma :=\emptyset \mid \Gamma ,x:A}
β-還元の概念は、立方体内のすべての系に共通です。これは 規則によって表され、与えられます。 その 反射的推移的閉包 は と表されます 。 → β {\displaystyle \to _{\beta }} ( λ x : A . B ) C → β B [ C / x ] {\displaystyle {\frac {}{(\lambda x:A.B)~C\to _{\beta }B[C/x]}}} B → β B ′ λ x : A . B → β λ x : A . B ′ {\displaystyle {\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}} A → β A ′ λ x : A . B → β λ x : A ′ . B {\displaystyle {\frac {A\to _{\beta }A'}{\lambda x:A.B\to _{\beta }\lambda x:A'.B}}} B → β B ′ Π x : A . B → β Π x : A . B ′ {\displaystyle {\frac {B\to _{\beta }B'}{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}} A → β A ′ Π x : A . B → β Π x : A ′ . B {\displaystyle {\frac {A\to _{\beta }A'}{\Pi x:A.B\to _{\beta }\Pi x:A'.B}}} = β {\displaystyle =_{\beta }}
次の型指定ルールもキューブ内のすべてのシステムに共通です。 ⊢ ∗ : ◻ (Axiom) {\displaystyle {\frac {}{\vdash *:\square }}\quad {\text{(Axiom)}}} Γ ⊢ A : s Γ , x : A ⊢ x : A x ∉ Γ (Start) {\displaystyle {\frac {\Gamma \vdash A:s}{\Gamma ,x:A\vdash x:A}}x\not \in \Gamma \quad {\text{(Start)}}} Γ ⊢ A : B Γ ⊢ C : s Γ , x : C ⊢ A : B x ∉ Γ (Weakening) {\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}x\not \in \Gamma \quad {\text{(Weakening)}}} Γ ⊢ C : Π x : A . B Γ ⊢ D : A Γ ⊢ C D : B [ D / x ] (Application) {\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash D:A}{\Gamma \vdash CD:B[D/x]}}\quad {\text{(Application)}}} Γ ⊢ A : B B = β B ′ Γ ⊢ B ′ : s Γ ⊢ A : B ′ (Conversion) {\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(Conversion)}}}
システム間の違いは、 次の 2 つの型付け規則で許可されるソートのペアにあります。 ( s 1 , s 2 ) {\textstyle (s_{1},s_{2})} Γ ⊢ A : s 1 Γ , x : A ⊢ B : s 2 Γ ⊢ Π x : A . B : s 2 (Product) {\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \Pi x:A.B:s_{2}}}\quad {\text{(Product)}}} Γ ⊢ A : s 1 Γ , x : A ⊢ B : s 2 Γ , x : A ⊢ C : B Γ ⊢ λ x : A . C : Π x : A . B (Abstraction) {\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad \Gamma ,x:A\vdash C:B}{\Gamma \vdash \lambda x:A.C:\Pi x:A.B}}\quad {\text{(Abstraction)}}}
システムと ルールで許可されているペアの対応は次のとおりです。 ( s 1 , s 2 ) {\textstyle (s_{1},s_{2})}
( s 1 , s 2 ) {\displaystyle (s_{1},s_{2})} ( ∗ , ∗ ) {\displaystyle (*,*)} ( ∗ , ◻ ) {\displaystyle (*,\square )} ( ◻ , ∗ ) {\displaystyle (\square ,*)} ( ◻ , ◻ ) {\displaystyle (\square ,\square )} λ→ λP λ2 λω λP2 λP ω λω λC
立方体の各方向は 1 つのペア ( すべてのシステムで共有されるペアを除く) に対応し、各ペアは用語とタイプ間の依存関係の 1 つの可能性に対応します。 ( ∗ , ∗ ) {\textstyle (*,*)}
( ∗ , ∗ ) {\textstyle (*,*)} 用語が用語に依存できるようにします。 ( ∗ , ◻ ) {\textstyle (*,\square )} 型が用語に依存できるようにします。 ( ◻ , ∗ ) {\textstyle (\square ,*)} 用語がタイプに依存できるようにします。 ( ◻ , ◻ ) {\textstyle (\square ,\square )} 型が型に依存できるようにします。
システム間の比較
λ→ 得られる典型的な導出は、 矢印のショートカットで または であり、これは通常の λ→ の （型 の）恒等式に非常に似ています。使用されるすべての型はコンテキスト内に出現する必要があることに注意してください 。 空のコンテキストで実行できる唯一の導出は であるためです α : ∗ ⊢ λ x : α . x : Π x : α . α {\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha } α : ∗ ⊢ λ x : α . x : α → α {\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\alpha \to \alpha } α {\textstyle \alpha } ⊢ ∗ : ◻ {\textstyle \vdash *:\square }
計算能力は非常に弱く、拡張多項式（条件演算子を伴う多項式）に相当する。 [5]
λ2 λ2では、そのような項は の ように得ることができます。 カリー・ハワード同型性を介して全称量化として 読むと、これは 爆発の原理 の証明と見ることができます。一般に、λ2はのような 非述語 型 、つまりそれ自身を含むすべての型にわたって量化される項を持つ可能性を追加します。 この多型性により、λ→では構成できなかった関数の構築も可能になります。より正確には、λ2で定義可能な関数は、2階 ペアノ算術 において証明可能全体となる関数です。 [6] 特に、すべての 原始再帰関数は 定義可能です ⊢ ( λ β : ∗ . λ x : ⊥ . x β ) : Π β : ∗ . ⊥ → β {\displaystyle \vdash (\lambda \beta :*.\lambda x:\bot .x\beta ):\Pi \beta :*.\bot \to \beta } ⊥ = Π α : ∗ . α {\textstyle \bot =\Pi \alpha :*.\alpha } Π {\textstyle \Pi } ⊥ {\textstyle \bot }
λP λPでは、項に依存する型を持つことができるということは、論理述語を表現できることを意味します。例えば、以下は導出可能です。 これは、カリー・ハワード同型性を介して、の証明に対応します 。 しかし、計算の観点から見ると、依存型を持つことは計算能力を向上させるのではなく、より正確な型特性を表現できる可能性を高めるだけです。 [7] α : ∗ , a 0 : α , p : α → ∗ , q : ∗ ⊢ λ z : ( Π x : α . p x → q ) . λ y : ( Π x : α . p x ) . ( z a 0 ) ( y a 0 ) : ( Π x : α . p x → q ) → ( Π x : α . p x ) → q {\displaystyle {\begin{array}{l}\alpha :*,a_{0}:\alpha ,p:\alpha \to *,q:*\vdash \\\quad \lambda z:(\Pi x:\alpha .px\to q).\\\quad \lambda y:(\Pi x:\alpha .px).\\\quad (za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to (\Pi x:\alpha .px)\to q\end{array}}} ( ∀ x : A , P x → Q ) → ( ∀ x : A , P x ) → Q {\displaystyle (\forall x:A,Px\to Q)\to (\forall x:A,Px)\to Q}
変換規則は、依存型を扱う際に非常に重要になります。なぜなら、この規則によって、型内の項に対して計算を実行できるようになるからです。例えば、 と がある場合、 と 型付けできるようにする には 、変換規則 [a] を適用して を得る必要があります。 Γ ⊢ A : P ( ( λ x . x ) y ) {\displaystyle \Gamma \vdash A:P((\lambda x.x)y)} Γ ⊢ B : Π x : P ( y ) . C {\displaystyle \Gamma \vdash B:\Pi x:P(y).C} Γ ⊢ A : P ( y ) {\displaystyle \Gamma \vdash A:P(y)} Γ ⊢ B A : C {\displaystyle \Gamma \vdash BA:C}
λω λωでは、次の演算子 が定義可能です 。導出は λ2ですでに得られますが、多型性は 規則 も存在する
場合にのみ定義できます A N D := λ α : ∗ . λ β : ∗ . Π γ : ∗ . ( α → β → γ ) → γ {\displaystyle AND:=\lambda \alpha :*.\lambda \beta :*.\Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma } ⊢ A N D : ∗ → ∗ → ∗ {\displaystyle \vdash AND:*\to *\to *} α : ∗ , β : ∗ ⊢ Π γ : ∗ . ( α → β → γ ) → γ : ∗ {\displaystyle \alpha :*,\beta :*\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*} A N D {\textstyle AND} ( ◻ , ∗ ) {\textstyle (\square ,*)}
コンピューティングの観点から見ると、λωは非常に強力であり、プログラミング言語の基礎として考えられてきました。 [10]
λC 構成計算はλPの述語表現力とλωの計算力の両方を備えているため、λCはλPωとも呼ばれます。 [1] : 130 つまり、論理面でも計算面でも非常に強力です
他のシステムとの関係 オートマトン システムは 、論理的な観点からはλ2に類似しています。ML 系言語は 、型付けの観点から見ると、λ→とλ2の中間に位置します。ML系言語は、限られた種類の多相型、つまり冠頭 正規形（prenex normal form） の型を許容するからです。しかし、再帰演算子を備えているため、計算能力はλ2よりも優れています。 [7] Coqシステムは、λCの拡張に基づいており、型付け不可能な型を1つだけではなく 、線形階層構造を持つユニバースと、帰納的型を構築する機能を備えています。 ◻ {\textstyle \square }
純粋型システムは 、任意のソート、公理、積、抽象化規則を持つキューブの一般化と見ることができます。逆に、ラムダキューブのシステムは、2つのソート 、唯一の公理、そして となる 規則を持つ純粋型システムとして表現できます 。 [1] { ∗ , ◻ } {\displaystyle \{*,\square \}} { ∗ , ◻ } {\textstyle \{*,\square \}} R {\textstyle R} { ( ∗ , ∗ , ∗ ) } ⊆ R ⊆ { ( ∗ , ∗ , ∗ ) , ( ∗ , ◻ , ◻ ) , ( ◻ , ∗ , ∗ ) , ( ◻ , ◻ , ◻ ) } {\displaystyle \{(*,*,*)\}\subseteq R\subseteq \{(*,*,*),(*,\square ,\square ),(\square ,*,*),(\square ,\square ,\square )\}}
カリー・ハワード同型性により、ラムダキューブ内のシステムと論理システムの間には1対1の対応関係がある 。 [1]
すべての論理は含意的です（つまり、接続詞はとのみです ） 。しかし、二階以上の論理では、 またはなどの他の接続詞を 非 述語的 に定義することができます。弱高階論理では、高階述語には変数がありますが、それらに対する量化はできません → {\textstyle \to } ∀ {\textstyle \forall } ∧ {\displaystyle \wedge } ¬ {\displaystyle \neg }
共通の性質 立方体内のすべてのシステムは
チャーチ ＝ロッサーの性質 ： かつ のとき 、かつ と なるようなもの が 存在する M → β N {\displaystyle M\to _{\beta }N} M → β N ′ {\displaystyle M\to _{\beta }N'} N ″ {\displaystyle N''} N → β ∗ N ″ {\displaystyle N\to _{\beta }^{*}N''} N ′ → β ∗ N ″ {\displaystyle N'\to _{\beta }^{*}N''} 主語 削減プロパティ : if and then ; Γ ⊢ M : T {\displaystyle \Gamma \vdash M:T} M → β M ′ {\displaystyle M\to _{\beta }M'} Γ ⊢ M ′ : T {\displaystyle \Gamma \vdash M':T} 型の一意性: if と then 。 Γ ⊢ A : B {\displaystyle \Gamma \vdash A:B} Γ ⊢ A : B ′ {\displaystyle \Gamma \vdash A:B'} B = β B ′ {\displaystyle B=_{\beta }B'} これらはすべてジェネリック純粋型システムで証明できます。 [11]
キューブのシステムにおいて適切に型付けされた項はどれも強く正規化されるが [1] 、この性質はすべての純粋型システムに共通するわけではない。キューブ内のシステムはチューリング完全ではない。 [7]
サブタイピング しかし、サブタイピングは キューブでは表現されません。 高階限定量化と呼ばれる、サブタイピングと多態性を組み合わせたシステムは実用上興味深いものであり、さらに限定型演算子へと一般化できます。 純粋に関数的なオブジェクトの定義を可能にするためのさらなる拡張。これらのシステムは、ラムダキューブの論文が発表された後に、一般的に開発されました。 [12] F <: ω {\displaystyle F_{<:}^{\omega }} F <: ω {\displaystyle F_{<:}^{\omega }}
立方体のアイデアは、数学者 ヘンク・バレンドレト（1991）によるものです。 純粋型システム の枠組みは、 ラムダ立方体を一般化します。つまり、立方体のすべての角、そして他の多くのシステムを、この一般的な枠組みのインスタンスとして表現できるということです。 [13] この枠組みはラムダ立方体より数年前に生まれました。バレンドレトは1991年の論文で、この枠組みにおける立方体の角も定義しています。
参照 オリヴィエ・リドゥーは、 『研究指導要領』 [14] の中で 、ラムダ立方体の切り抜きテンプレートと、8つの頂点を面に置き換えた正八面体としての立方体の双対表現、および12の辺を面に置き換えた正十二面体としての双対表現を示しています 論理的立方体 論理的六角形 反対の正方形 反対の三角形
注記 ^ abcdef Barendregt, Henk (1991). 「一般化型システム入門」. Journal of Functional Programming . 1 (2): 125–154 . doi :10.1017/s0956796800020025. hdl : 2066/17240 . ISSN 0956-7968. S2CID 44757552 ^ Nederpelt, Rob; Geuvers, Herman (2014). 型理論と形式的証明. Cambridge University Press. p. 69. ISBN 9781107036505 。 ^ Nederpelt & Geuvers 2014, p. 85 ^ Nederpelt & Geuvers 2014、p. 100 ^ シュヴィヒテンベルク、ヘルムート (1975)。 「Definierbare Funktionen imλ-Kalkül mit Typen」。 Archiv für Mathematische Logik und Grundlagenforschung (ドイツ語)。 17 ( 3–4 ): 113–114 . 土井 :10.1007/bf02276799。 ISSN 0933-5846。 S2CID 11598130。 ^ ジャン＝イヴ・ジラール、イヴ・ラフォン、ポール・テイラー (1989). 『証明と型 』 ケンブリッジ理論計算機科学論文集. 第7巻. ケンブリッジ大学出版局. ISBN 9780521371810 。 ^ abc Ridoux, Olivier (1998). Lambda-Prolog de A à Z … ou presque (PDF) . [sn] OCLC 494473554 ^ Angiuli, Carlo; Gratzer, Daniel (2024). 「2.1.3 型付け規則の型検査は誰が行うのか？ および 2.2 依存型理論の構文に向けて」. 依存型理論の原理 (PDF) . インディアナ大学およびオーフス大学. 2024年 9月7日 閲覧 。 ^ Favier, Naïm (2023年8月17日). 「ラムダキューブの変換推論規則において、なぜ Γ ⊢ B′:s が必要なのか？」 Computer Science Stack Exchange . 2024年 9月7日 閲覧 。 ^ ピアス, ベンジャミン; ディーツェン, スコット; ミハイロフ, スピロ (1989). 高階型付きラムダ計算におけるプログラミング . カーネギーメロン大学コンピュータサイエンス学部. OCLC 20442222. CMU-CS-89-111 ERGO-89-075. ^ Sørensen, Morten Heine; Urzyczyin, Pawel (2006). 「純粋型システムとλキューブ」. Curry-Howard同型性に関する講義 . Elsevier. pp. 343– 359. doi :10.1016/s0049-237x(06)80015-7. ISBN 9780444520777 。 ^ ピアス、ベンジャミン (2002). 型とプログラミング言語 . MIT Press. pp. 467– 490. ISBN 978-0262162098 OCLC 300712077 ^ ピアス 2002, 466ページ ^ リドゥー 1998、70ページ ^ 変換規則の仮定は 便宜上のものであり、代わりにメタ定理を証明することもできる 。 [8] [9] Γ ⊢ B ′ : s {\displaystyle \Gamma \vdash B':s} Γ ⊢ A : B ∧ B = β B ′ ⇒ Γ ⊢ B ′ : s {\displaystyle \Gamma \vdash A:B\land B=_{\beta }B'\Rightarrow \Gamma \vdash B':s}
さらに読む ペイトン・ジョーンズ、サイモン、マイヤー、エリック (1997).「Henk: 型付き中間言語」 (PDF) . Microsoft . Henkは 、表現力豊かな型付きラムダ計算のファミリーであるラムダキューブに直接基づいています
外部リンク ロジャー・ビショップ・ジョーンズ著『 純粋型システム の文脈におけるバレンドレヒトのラムダキューブ』 
![{\displaystyle {\frac {}{(\lambda x:AB)~C\to _{\beta }B[C/x]}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/43b3d114323724967ee6d4e99bfc60a24be40384)
![{\displaystyle {\frac {\Gamma \vdash C:\Pi x:AB\quad \Gamma \vdash D:A}{\Gamma \vdash CD:B[D/x]}}\quad {\text{(応用)}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/35cee7b01b02ea0e01c97ac2fee5f00844c15740)
