stlc の設計

設計目標

stlc は共有基盤上の小さく完全な型付き計算体系の実例である：名前付き構文、代入、書き換え、型なし簡約器を再利用し、型によって可能になるもの、すなわち決定可能な型検査器と、ステップ上限を必要とせず標準形（β 正規かつ η 長形式）を返す正規化器を加える。これは type_theory 上に構築されるより豊かな型付きコアの手本である。

数学的背景

型と項

\tau, \sigma \;::=\; b \;\mid\; \mathsf{Unit} \;\mid\; \sigma \to \tau, \qquad t \;::=\; () \;\mid\; c \;\mid\; x \;\mid\; \lambda x.\,t \;\mid\; t\,u_1 \cdots u_n .

基底型 $b$ は解釈されない名前である。ラムダは型注釈をもたない（Curry 流）。シグネチャ $\Sigma$ は定数 $c$ の型を、文脈 $\Gamma$ は自由変数の型を与える。いずれにおいても、ある名前に対する後のエントリは前のエントリを隠し、 $\Gamma, x{:}\sigma$ と書く。

宣言的型付け

判断 $\Sigma; \Gamma \vdash t : \tau$ は標準的な規則で与えられる（ $\Sigma$ は暗黙とする）：

\frac{}{\Gamma \vdash () : \mathsf{Unit}} \qquad \frac{\Sigma(c) = \tau}{\Gamma \vdash c : \tau} \qquad \frac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau} \qquad \frac{\Gamma, x{:}\sigma \vdash t : \tau}{\Gamma \vdash \lambda x.\,t : \sigma \to \tau} \qquad \frac{\Gamma \vdash f : \sigma \to \tau \qquad \Gamma \vdash a : \sigma}{\Gamma \vdash f\,a : \tau}

項の等しさは $\beta\eta$ 変換であり、 $(\lambda x.\,b)\,a =_\beta b[x := a]$ および $x \notin \mathrm{FV}(f)$ のとき $\lambda x.\,f\,x =_\eta f$ で、いずれも型の付くインスタンスに対してである。

古典的な結果

主部簡約。 $\Gamma \vdash t : \tau$ かつ $t \to_{\beta\eta} u$ ならば $\Gamma \vdash u : \tau$ である。
強正規化。 型の付く項のすべての簡約列は有限である（Tait の計算可能性述語の方法）。¹1 W. W. Tait、“Intensional interpretations of functionals of finite type I”、Journal of Symbolic Logic 32、1967。
標準形。 型の付くすべての項は、下で定義する β 正規かつ η 長形式の唯一の項と $\beta\eta$ 等価である。

設計上の決定

双方向型検査

問題。 ラムダに注釈がないと $\lambda x.\,x$ の型は定まらず、完全な型推論（単一化）はこの計算体系に必要な範囲を超える。

選択。 相互再帰する二つの判断：推論 $\Gamma \vdash t \Rightarrow \tau$ （infer）と検査 $\Gamma \vdash t \Leftarrow \tau$ （check）。情報は期待される型からラムダへ流れ込み、変数や定数から適用へと流れ出す。²2 J. Dunfield と N. Krishnaswami、“Bidirectional typing”、ACM Computing Surveys 54(5)、2021。実装された規則は次のとおりである

\frac{}{\Gamma \vdash () \Rightarrow \mathsf{Unit}} \qquad \frac{\Sigma(c) = \tau}{\Gamma \vdash c \Rightarrow \tau} \qquad \frac{\Gamma(x) = \tau}{\Gamma \vdash x \Rightarrow \tau}

\textsc{App}\; \frac{\Gamma \vdash h \Rightarrow \tau_1 \to \cdots \to \tau_n \to \tau \qquad \Gamma \vdash a_i \Leftarrow \tau_i \ \ (1 \le i \le n)} {\Gamma \vdash h\,a_1 \cdots a_n \Rightarrow \tau} \quad (h \text{ not a } \lambda,\ n \ge 1)

\textsc{Redex}\; \frac{\Gamma \vdash a_1 \Rightarrow \sigma \qquad \Gamma, x{:}\sigma \vdash b\,a_2 \cdots a_n \Rightarrow \tau} {\Gamma \vdash (\lambda x.\,b)\,a_1\,a_2 \cdots a_n \Rightarrow \tau} \qquad \textsc{Lam}\; \frac{\Gamma, x{:}\sigma \vdash b \Leftarrow \tau}{\Gamma \vdash \lambda x.\,b \Leftarrow \sigma \to \tau} \qquad \textsc{Sub}\; \frac{\Gamma \vdash t \Rightarrow \tau' \qquad \tau' = \tau}{\Gamma \vdash t \Leftarrow \tau}

$\textsc{App}$ ではまずスパインを平坦化するので、入れ子の Apply ノードは一つの適用 $h\,a_1 \cdots a_n$ になる。 $h$ の矢印の数が引数より少なければ結果は ExpectedFunction である。 $n = 1$ の $\textsc{Redex}$ では、第 2 前提は $\Gamma, x{:}\sigma \vdash b \Rightarrow \tau$ である。 $\textsc{Sub}$ は、矢印型に対して検査されるラムダを除くすべての項に適用される。推論位置にあるラムダは CannotInferLambda で失敗する。 $\textsc{Sub}$ における型の等しさは構文的であり、単純型に対しては厳密である。

追加の $\textsc{Redex}$ 規則が必要な理由。 素朴な双方向型付けでは、ヘッドがラムダであるため $(\lambda x.\,b)\,a$ を推論できない。この規則は簡約基を $\mathsf{let}\ x = a\ \mathsf{in}\ b$ のように扱う：引数の型を推論し、それを仮引数に与える。これにより、 $(\lambda x.\,x)\,()$ のような代入スタイルのプログラミングで生じる項を、注釈なしで検査できるようになる。

検査器の健全性

定理。 check(Σ, Γ, t, τ) が成功すれば $\Gamma \vdash t : \tau$ であり、infer(Σ, Γ, t) が $\tau$ を返せば $\Gamma \vdash t : \tau$ である。ただし $\textsc{Redex}$ のすべての使用が $x \notin \mathrm{FV}(a_2, \dots, a_n)$ を満たすものとする。

証明の概略。 アルゴリズム的導出に関する帰納法による。 $\textsc{Lam}$ と公理は対応する宣言的規則に写る。 $\textsc{Sub}$ は自明である。 $\textsc{App}$ は宣言的な適用規則を $n$ 回使うことである。 $\textsc{Redex}$ については第 2 前提を反転する： $\Gamma, x{:}\sigma \vdash b \Rightarrow \tau_2 \to \cdots \to \tau_n \to \tau$ かつ $i \ge 2$ について $\Gamma, x{:}\sigma \vdash a_i : \tau_i$ である。このとき

\begin{aligned} &\Gamma \vdash \lambda x.\,b : \sigma \to \tau_2 \to \cdots \to \tau && \text{abstraction} \\ &\Gamma \vdash (\lambda x.\,b)\,a_1 : \tau_2 \to \cdots \to \tau && \text{application, } \Gamma \vdash a_1 : \sigma \\ &\Gamma \vdash a_i : \tau_i \ (i \ge 2) && \text{strengthening, needs } x \notin \mathrm{FV}(a_i) \\ &\Gamma \vdash (\lambda x.\,b)\,a_1 \cdots a_n : \tau && \text{application } (n - 1 \text{ times}). \end{aligned}

$\square$

強化のステップが副条件を使う箇所であり、実装はそれを強制しない： $\Gamma = x{:}B$ について、

(\lambda x.\,\lambda y.\,y)\;()\;x

は宣言的な型 $B$ をもつ（外側の $x$ は型 $B$ をもつ）が、infer は第 2 引数を $\Gamma, x{:}\mathsf{Unit}$ で型付けし Unit を返す。その後 normalize_eta_long は、その評価器が元の文脈で引数を検査するため、どちらの型でもこの項を拒否する。これは現在の実装の既知の問題であり（正しさのチェックリストに記録されている）、仮引数を残りの引数の自由変数と異なる名前に替えることで回避できる。

正規形に対する完全性。 $t$ が β 正規で $\Gamma \vdash t : \tau$ ならば、check(Σ, Γ, t, τ) は成功する。β 正規な項は、 $\textsc{Lam}$ が扱うラムダであるか、ヘッドが変数・定数・ $()$ であるスパインである。その型は $\Gamma$ または $\Sigma$ によって決まり、引数もまた正規形であるので、 $\textsc{App}$ と帰納法が適用できる。簡約基を含む項は、各簡約基の最初の引数が推論可能であれば受理される。 $(\lambda f.\,f\,())\,(\lambda y.\,y)$ は型が付くにもかかわらず CannotInferLambda で拒否される。

検査器は停止する。すべての再帰呼び出しは真に小さい項に対して行われる（ $\textsc{Redex}$ は $b\,a_2 \cdots a_n$ に対して再帰し、これは redex より小さい）。

役割の異なる二つの正規化器

normalize_checked は型を検査した後、utlc/lambda の型なし正規順序 βη 簡約器を再利用する。その価値は、トレースとステップ数を伴う参照意味論である点にある。ステップ数に上限があるのは型なし計算と共有しているためにすぎない。強正規化性により、上限が十分大きければ必ず NormalForm で終わる。その正規形は η 短形である。

normalize_eta_long は型付きの評価による正規化（normalization by evaluation）である。上限を必要とせず、 $\beta\eta$ 同値類の標準的な代表元を返すので、二つの well-typed な項が $\beta\eta$ 等しいのは、それらの η 長正規形が α同値であるとき、かつそのときに限る。すなわちこの正規化器は変換可能性を決定する。

β正規・η長形式

正規形 $\mathit{Nf}^\tau$ と中立項 $\mathit{Ne}$ は型ごとに定義される。

\begin{aligned} \mathit{Nf}^{\sigma \to \tau} &::= \lambda x.\,\mathit{Nf}^{\tau}, & \mathit{Nf}^{b} &::= \mathit{Ne}, & \mathit{Nf}^{\mathsf{Unit}} &::= () \mid \mathit{Ne}, \\ \mathit{Ne} &::= x \mid c \mid \mathit{Ne}\;\mathit{Nf}^{\sigma} . \end{aligned}

矢印型の項はすべてラムダであり（η 長）、すべての適用は頭部に変数または定数を持つ（β 正規）。 $\mathsf{Unit}$ 型の中立項はそのまま残される。unit 型の η 法則（すべての $t : \mathsf{Unit}$ について $t = ()$ ）は実装されていないため、 $f : \mathsf{Unit} \to \mathsf{Unit}$ と $u : \mathsf{Unit}$ に対して項 $f\,u$ と $f\,()$ は異なる正規形を持つ。

型付きの評価による正規化

意味領域は各型を次のように解釈する。

V_b = \mathit{Ne}_V, \qquad V_{\mathsf{Unit}} = \{()\} + \mathit{Ne}_V, \qquad V_{\sigma \to \tau} = \mathit{Clo}_{\sigma \to \tau} + \mathit{Ne}_V,

ここでクロージャはラムダ本体をその環境と型とともに保持し、意味的な中立項は自由変数、定数、または中立項を値に適用したもの（その値の型も併せて保持する）である。評価 $\llbracket t \rrbracket\rho$ は変数を環境を通じて写し、ラムダをクロージャに、定数を中立項に写し、クロージャはその本体を評価することで適用する（値呼び。型付き項の評価は停止するので安全である）。反映 $\uparrow^\tau$ は中立項を値として埋め込む。ここでは中立項上の恒等写像である。η展開はすべて具象化（reification）まで遅延されるからである。具象化 $\downarrow^\tau : V_\tau \to \mathit{Nf}^\tau$ は次のとおりである。

\begin{aligned} \downarrow^{\sigma \to \tau} f &= \lambda x.\; \downarrow^{\tau}\big(f \cdot \uparrow^{\sigma} x\big) \qquad x \text{ fresh}, \\ \downarrow^{b} n &= \mathrm{quote}(n), \qquad \downarrow^{\mathsf{Unit}} () = (), \qquad \downarrow^{\mathsf{Unit}} n = \mathrm{quote}(n), \\ \mathrm{quote}(x) &= x, \quad \mathrm{quote}(c) = c, \quad \mathrm{quote}(n \cdot^{\sigma} v) = \mathrm{quote}(n)\;\downarrow^{\sigma} v, \end{aligned}

そして $\Gamma \vdash t : \tau$ の正規形は $\downarrow^\tau \llbracket t \rrbracket \rho_\Gamma$ である。ここで $\rho_\Gamma$ は各 $x{:}\sigma \in \Gamma$ を $\uparrow^\sigma x$ に写す。矢印型での具象化は値を新しい変数に適用し、これが η展開を行う。中立な適用は引数の定義域の型を記録しておき、後でその引数を正しい型で具象化できるようにする。³3 U. Berger and H. Schwichtenberg, “An inverse of the evaluation functional for typed λ-calculus”, LICS 1991. 型主導の提示は A. Abel, Normalization by Evaluation: Dependent Types and Impredicativity, habilitation thesis, 2013 に従う。

正しさ（証明の概略）。 項と値の間の Kripke 論理関係 $t \mathrel{R_\tau} d$ を、文脈の拡張について単調なものとして定義する。

\begin{aligned} t \mathrel{R_b} n &\iff t =_{\beta\eta} \mathrm{quote}(n), \\ t \mathrel{R_{\mathsf{Unit}}} d &\iff t =_{\beta\eta} \downarrow^{\mathsf{Unit}} d, \\ t \mathrel{R_{\sigma \to \tau}} f &\iff \forall\, \Gamma' \supseteq \Gamma,\ s \mathrel{R_\sigma} e \implies t\,s \mathrel{R_\tau} f \cdot e . \end{aligned}

$\tau$ に関する帰納法で二つの補題を同時に証明する。反映（ $t =_{\beta\eta} \mathrm{quote}(n)$ ならば $t \mathrel{R_\tau} \uparrow^\tau n$ ）と具象化（ $t \mathrel{R_\tau} d$ ならば $t =_{\beta\eta} \downarrow^\tau d$ ）である。具象化の矢印型の場合が η ステップである。

t \;=_\eta\; \lambda x.\,t\,x \;=_{\beta\eta}\; \lambda x.\,\downarrow^\tau (f \cdot \uparrow^\sigma x) \;=\; \downarrow^{\sigma \to \tau} f ,

ここでは $x \mathrel{R_\sigma} \uparrow^\sigma x$ （反映）と $R_{\sigma \to \tau}$ の定義を用いる。基本補題は、 $\Gamma \vdash t : \tau$ かつ $\gamma \mathrel{R_\Gamma} \rho$ ならば $t[\gamma] \mathrel{R_\tau} \llbracket t \rrbracket \rho$ であることを主張する。これは型導出に関する帰納法で証明され、ラムダの場合には β簡約が $=_{\beta\eta}$ に含まれることを用いる。 $\gamma$ を恒等代入とし $\rho_\Gamma$ を取ると（両者は反映によって関係づけられる）、具象化により $t =_{\beta\eta} \mathrm{nf}(t)$ （健全性）が得られる。評価は $\beta\eta$ 等しい項を同一視する（β はモデルにおける関数適用であり、η は具象化が常に展開するので成り立つ）ため、等しい項は等しい正規形を持つ（完全性）。同じ関係を計算可能性述語として読めば、well-typed な項上で評価が停止することが示され、これが燃料（fuel）を必要としない理由である。

読み戻しにおける新しい名前

読み戻しは fresh_name("x", used) によって束縛子の名前を生成する。ここで used は入力項と文脈のすべての名前、クロージャ環境内の名前、そして経路上ですでに導入された名前を含む。したがって生成された名前は同じ経路上で互いに異なり、入力のすべての名前とも異なるので、中立変数が後から導入される束縛子に捕獲されることはない。

正しさ / 不変条件

check と infer は停止する。成功した場合、その項は報告された型で宣言的に型付け可能である。ただし $\textsc{Redex}$ の付帯条件に従う（上述の既知の問題を参照）。
check は well-typed な β 正規項をすべて受理する。
既知の問題を除き、normalize_eta_long はちょうど check が受理する項に対して Ok を返す。その結果は $\mathit{Nf}^\tau$ に属し、入力と $\beta\eta$ 等しく、 $\beta\eta$ 等しい入力に対しては（ $=_\alpha$ を除いて）同じである。
型の誤った入力に対して、normalize_checked は簡約を行う前に Err を返す。
NormalizationError は内部不変条件の違反を示し、検査済みの入力に対しては生じない。

src/stlc/stlc_test.mbt のテストは、型付けと拒否、シャドーイング、開いた変数および定数の η展開（入れ子の矢印型や高階の引数を含む）、そして小さな項における二つの正規化器の一致を扱う。

却下した代替案

Church 流の注釈付きラムダ。 注釈があれば型推論は完全になるが、共有の Term 構文を変えてしまう。双方向型検査器は項を注釈なしのまま保つ。
Hindley–Milner 型推論。 単一化により注釈なしラムダの型を推論できるが、多相性と型変数はこの計算の範囲外である。
型付き NbE の燃料。 強正規化性により不要である。型なしの utlc/nbe が燃料を保持するのは、それが必要だからである。
unit 型の η。 $\mathsf{Unit}$ 型のすべての中立項を $()$ として具象化すれば実装できるが、中立項を観測可能に保つため行っていない。決定される等価性は矢印型に対する $\beta\eta$ のみである。

境界

型は $b$ 、 $\mathsf{Unit}$ 、矢印型のみである。直積、直和、多相性、依存型はない。
unit 型の η はない。正規形が η 長であるのは矢印型についてのみである。
定数は不透明である。δ 規則はない。
$\textsc{Redex}$ 規則は、そのパラメータを後続の引数と衝突しないよう名前替えしない（既知の問題）。
normalize_checked は型なし簡約器を再利用するため、ステップ数の上限に縛られる。

W. W. Tait、“Intensional interpretations of functionals of finite type I”、Journal of Symbolic Logic 32、1967。 ↩
J. Dunfield と N. Krishnaswami、“Bidirectional typing”、ACM Computing Surveys 54(5)、2021。 ↩
U. Berger and H. Schwichtenberg, “An inverse of the evaluation functional for typed λ-calculus”, LICS 1991. 型主導の提示は A. Abel, Normalization by Evaluation: Dependent Types and Impredicativity, habilitation thesis, 2013 に従う。 ↩