# プログラミング言語論：機械語から型システムとパラダイムまで > 機械語・アセンブリ・高級言語の階層を RISC-V の実際の命令符号化から確認し、小さな言語の操作的意味論のうえで進行定理と保存定理を証明したうえで、静的型付けと動的型付け、関数型とオブジェクト指向の設計原理を比較します。 > https://rikai.mugen-giken.com/computer-science/cs-basics/programming-language-theory ## 0. この記事の要点 - CPU が実行できるのは固定長のビット列（機械語）だけです。アセンブリ言語はそのビット列に人間が読める名前を付けただけのもので、高級言語との間には「意味を保つ翻訳」という質的な断絶があります。 - コンパイラとインタプリタの違いは、言語の性質ではなく実装戦略の違いです。同じ言語に両方の処理系を作れます。区別が本質的に効くのは、エラーを実行前に見つけるか実行時に見つけるかという点です。 - 型システムの価値は「進行定理」と「保存定理」の 2 本に集約されます。この 2 つから、型の付いたプログラムは実行の途中で行き詰まらないという保証（型健全性）が従います。 - 静的型検査は健全である限り必ず不完全です。これは実装の未熟さではなく、停止性問題の決定不能性から導かれる原理的な限界です。 - 関数型プログラミングの中心概念は参照透過性であり、これは「同じ式は何度評価しても同じ値になる」という定理を成立させます。オブジェクト指向の中心概念は動的ディスパッチと部分型であり、関数型の部分型規則は引数について反変になります。 ## 1. 動機：なぜ「言語」が必要なのか [コンピュータアーキテクチャと CPU の構造](/computer-science/cs-basics/computer-architecture) の で見たとおり、CPU が理解するのは 32 ビットや 64 ビットのビット列だけです。1940 年代の計算機は、実際にこのビット列を人間が紙に書き、スイッチやパンチカードで入力していました。 この作業は 2 つの意味で耐えがたいものでした。第 1 に、間違えます。1 ビット違えば別の命令になり、しかも大抵の場合それも「有効な」命令なので、計算機は何事もなかったかのように誤った計算を続けます。第 2 に、書き換えられません。プログラムの真ん中に命令を 1 つ挿入すると、それ以降のすべての分岐先アドレスがずれます。 そこで生まれた発想が「記号で書いて、機械に翻訳させる」ことでした。ここには 1 つの飛躍があります。翻訳をするのもまたプログラムだ、という自己言及です。1952 年に Grace Hopper が A-0 システムを、1957 年に IBM の John Backus のチームが FORTRAN のコンパイラを完成させたとき、多くの技術者は「機械が生成したコードが人間の手書きに勝てるはずがない」と考えていました。今日、その懐疑は完全に覆っています。 しかし翻訳を機械に任せた瞬間、新しい問いが生まれます。**翻訳が正しいとは、どういうことか**。これに答えるには、まず「プログラムの意味」を数学的に定義しなければなりません。この記事はその定義から始めて、型システムとパラダイムの設計原理までを見ていきます。 ## 2. 抽象度の階段：機械語とアセンブリ言語 ### 2.1. 機械語は命令の符号化である RISC-V の 32 ビット命令 `addi`（即値加算）を例に取ります。どの命令名がどのビット並びに対応するかを定める規約が の命令セットアーキテクチャです。この命令は I 形式と呼ばれる並びを持ち、上位から順に 12 ビットの即値、5 ビットのソースレジスタ番号 `rs1`、3 ビットの `funct3`、5 ビットのデスティネーションレジスタ番号 `rd`、7 ビットのオペコードが並びます。 「レジスタ `a0` の値に 1 を足して `a0` に戻す」という命令を符号化します。RISC-V では `a0` はレジスタ番号 10、すなわち 2 進で `01010` です。`addi` のオペコードは `0010011`、`funct3` は `000` です。即値 1 は 12 ビットで `000000000001` です。 これを上位から連結します。 ```text 000000000001 01010 000 01010 0010011 即値=1 rs1=10 funct3 rd=10 opcode ``` 区切りを外して 4 ビットずつ切り直すと `0000 0000 0001 0101 0000 0101 0001 0011`、16 進で **0x00150513** です。同じ手順で `add a0, a0, a1`（R 形式。R 形式の符号化は でも計算しています）は 0x00B50533、関数からの復帰命令 `ret`（実体は `jalr x0, 0(x1)`）は 0x00008067 になります。 つまり `addi a0, a0, 1` というアセンブリの 1 行は、0x00150513 という 32 ビット整数に**1 対 1 で対応する**別表記にすぎません。 この対応が 1 対 1 であることが決定的です。アセンブラの仕事は、命令名をオペコードの表で引き、レジスタ名を番号に直し、ラベルをアドレスに解決してビットを詰めることだけです。**新しい概念を導入しません**。 ### 2.2. 高級言語は何を追加したのか 一方、C 言語の 1 行はしばしば複数の命令に展開されます。 ```c int add1(int x) { return x + 1; } ``` これを RISC-V 向けに最適化付きでコンパイルすると、次の 2 命令になります。 ```text add1: addi a0, a0, 1 # 0x00150513 ret # 0x00008067 ``` ここで起きていることは、単なる記号の置換ではありません。「引数 `x` は第 1 引数レジスタ `a0` に入っている」「返り値も `a0` に置く」という**呼び出し規約**の知識、「`int` は 32 ビット 2 の補数である」という**型と表現の対応**、そして「局所変数はレジスタに割り付けてよい」という**最適化の判断**が使われています。高級言語が追加したのは、こうした決定を人間の手から取り上げる抽象化です。
B["中間表現 (構文木・IR)"] B --> C["アセンブリ言語 (addi a0, a0, 1)"] C --> D["機械語 (0x00150513)"] D --> E["CPU が実行"] B -.意味を保つ翻訳.-> C`} />
## 3. コンパイラとインタプリタ 言語 $S$（原始言語）、言語 $T$（目的言語）、言語 $I$（実装言語）を考えます。 **コンパイラ**とは、$I$ で書かれたプログラム $C$ であって、$S$ のプログラム $p$ を入力すると $T$ のプログラム $C(p)$ を出力し、任意の入力 $d$ について $p$ を $d$ に適用した結果と $C(p)$ を $d$ に適用した結果が一致するものをいいます。 **インタプリタ**とは、$I$ で書かれたプログラム $J$ であって、$S$ のプログラム $p$ と入力 $d$ の組を受け取り、$p$ を $d$ に適用した結果を直接出力するものをいいます。 この定義から読み取ってほしいのは、**コンパイラかインタプリタかは言語の属性ではない**ということです。どちらも「$p$ の意味を実現する」という同じ目標を、出力の形を変えて達成しているだけです。実際、C にはインタプリタ（Cling など）があり、Python には機械語を生成する処理系（PyPy の JIT）があります。「Python はインタプリタ言語である」という言い方は、正確には「Python の主要な実装 CPython がバイトコードインタプリタである」という意味です。 | 観点 | コンパイル方式 | インタプリタ方式 | |---|---|---| | 誤りの発見時期 | 翻訳時（実行前）に構文・型の誤りを検出 | 該当行に到達したときに検出 | | 実行速度 | 最適化を翻訳時に済ませられるため速い | 命令ごとの解釈オーバーヘッドが載る | | 起動の速さ | 翻訳の時間が先に必要 | すぐ動く | | 移植性 | 目的機械ごとに翻訳し直す | インタプリタさえあれば同じコードが動く | | 実行時情報の活用 | 静的にわかる範囲に限られる | 実際に通った経路に基づく最適化ができる | 最後の行が JIT（実行時コンパイル）の存在理由です。「この呼び出し箇所には過去 1 万回すべて同じ型のオブジェクトが来た」という事実は静的にはわからず、実行時にしか観測できません。JIT はこの観測に賭けて特化コードを生成し、賭けが外れたら解釈実行へ戻ります。コンパイルとインタプリタは対立ではなく、情報が使える時点の違いだと捉えるのが正確です。 ## 4. プログラムの意味を厳密に述べる 「翻訳が意味を保つ」と言うためには意味の定義が要ります。ここでは最も広く使われる**操作的意味論**、すなわち「1 ステップずつどう書き換わるか」で意味を与える方法を、極小の言語で実演します。 項 $t$ を次の文法で定める。 $$ t ::= \mathtt{true} \mid \mathtt{false} \mid \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t \mid \mathtt{0} \mid \mathtt{succ}\ t \mid \mathtt{pred}\ t \mid \mathtt{iszero}\ t $$ **数値** $nv$ と**値** $v$ を次で定める。 $$ nv ::= \mathtt{0} \mid \mathtt{succ}\ nv, \qquad v ::= \mathtt{true} \mid \mathtt{false} \mid nv $$ **1 ステップ簡約関係** $t \to t'$ を、次の規則で生成される最小の関係とする。 $$ \begin{aligned} &\text{(E-IfTrue)} && \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_2 \\ &\text{(E-IfFalse)} && \mathtt{if}\ \mathtt{false}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_3 \\ &\text{(E-If)} && \frac{t_1 \to t_1'}{\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to \mathtt{if}\ t_1'\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3} \\ &\text{(E-Succ)} && \frac{t \to t'}{\mathtt{succ}\ t \to \mathtt{succ}\ t'} \\ &\text{(E-PredZero)} && \mathtt{pred}\ \mathtt{0} \to \mathtt{0} \\ &\text{(E-PredSucc)} && \mathtt{pred}\ (\mathtt{succ}\ nv) \to nv \\ &\text{(E-Pred)} && \frac{t \to t'}{\mathtt{pred}\ t \to \mathtt{pred}\ t'} \\ &\text{(E-IszeroZero)} && \mathtt{iszero}\ \mathtt{0} \to \mathtt{true} \\ &\text{(E-IszeroSucc)} && \mathtt{iszero}\ (\mathtt{succ}\ nv) \to \mathtt{false} \\ &\text{(E-Iszero)} && \frac{t \to t'}{\mathtt{iszero}\ t \to \mathtt{iszero}\ t'} \end{aligned} $$ どの規則も適用できない項を**正規形**という。値でない正規形を**行き詰まり項**（stuck term）という。 行き詰まりが、この形式化における「実行時エラー」の定義です。たとえば $\mathtt{pred}\ \mathtt{false}$ は、E-PredZero も E-PredSucc も形が合わず、E-Pred を使おうにも $\mathtt{false}$ が簡約できないため、どの規則も適用できません。しかも値でもありません。実機なら「Boolean に対して pred は使えません」という例外が飛ぶ場面です。 項 $\mathtt{if}\ (\mathtt{iszero}\ (\mathtt{pred}\ (\mathtt{succ}\ \mathtt{0})))\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0}$ を簡約します。使った規則を各行に添えます。 $$ \begin{aligned} &\ \mathtt{if}\ (\mathtt{iszero}\ (\mathtt{pred}\ (\mathtt{succ}\ \mathtt{0})))\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0} \\ \to&\ \mathtt{if}\ (\mathtt{iszero}\ \mathtt{0})\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0} && \text{E-If の前提を E-Iszero、その前提を E-PredSucc（} nv = \mathtt{0} \text{）で導出} \\ \to&\ \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0} && \text{E-If の前提を E-IszeroZero で導出} \\ \to&\ \mathtt{0} && \text{E-IfTrue} \end{aligned} $$ $\mathtt{0}$ は値なので、ここで停止します。注意すべきは、2 行目で「まず条件式を最後まで評価する」と決めているのは E-If ただ 1 つの規則だという点です。この規則がなければ、条件が未評価のまま分岐する意味論も書けてしまいます。意味論とは、こうした選択を明示的に固定する作業です。 この規則集合はそのまま実行できるプログラムに書き写せます。以下は言語 L の完全なインタプリタです。 ```python def is_numeric(t): if t == ("zero",): return True if t[0] == "succ": return is_numeric(t[1]) return False class Stuck(Exception): pass def step(t): """項 t を 1 ステップ簡約する。規則が適用できなければ Stuck を送出する。""" k = t[0] if k == "if": _, t1, t2, t3 = t if t1 == ("true",): return t2 # E-IfTrue if t1 == ("false",): return t3 # E-IfFalse return ("if", step(t1), t2, t3) # E-If if k == "succ": return ("succ", step(t[1])) # E-Succ if k == "pred": u = t[1] if u == ("zero",): return ("zero",) # E-PredZero if u[0] == "succ" and is_numeric(u): return u[1] # E-PredSucc return ("pred", step(u)) # E-Pred if k == "iszero": u = t[1] if u == ("zero",): return ("true",) # E-IszeroZero if u[0] == "succ" and is_numeric(u): return ("false",) # E-IszeroSucc return ("iszero", step(u)) # E-Iszero raise Stuck(t) def evaluate(t): while True: try: t = step(t) except Stuck: return t # 正規形に到達 term = ("if", ("iszero", ("pred", ("succ", ("zero",)))), ("zero",), ("succ", ("zero",))) print(evaluate(term)) # ('zero',) print(evaluate(("pred", ("false",)))) # ('pred', ('false',)) ← 行き詰まり ``` (1) $nv$ が数値ならば、$nv \to t'$ となる項 $t'$ は存在しない。 (2) $v$ が値ならば、$v \to t'$ となる項 $t'$ は存在しない。 (1) を $nv$ の構造に関する帰納法で示します。$nv = \mathtt{0}$ のとき、 の規則のうち左辺が $\mathtt{0}$ という形の項であるものは存在しません（E-PredZero の左辺は $\mathtt{pred}\ \mathtt{0}$ であって $\mathtt{0}$ ではありません）。よって簡約できません。 $nv = \mathtt{succ}\ nv_1$ のとき、左辺が $\mathtt{succ}$ で始まる規則は E-Succ だけです。E-Succ を使うには前提 $nv_1 \to t_1'$ が必要ですが、帰納法の仮定より $nv_1$ は簡約できないので、この前提は満たせません。よって $\mathtt{succ}\ nv_1$ も簡約できません。 (2) 値は $\mathtt{true}$、$\mathtt{false}$、数値のいずれかです。$\mathtt{true}$ と $\mathtt{false}$ を左辺に持つ規則は存在せず（E-IfTrue の左辺は $\mathtt{if}$ で始まる項です）、数値については (1) が示しています。 言語 L の任意の項 $t$ について、$t \to t'$ かつ $t \to t''$ ならば $t' = t''$ である。 $t \to t'$ の導出に関する帰納法で示します。$t$ の形で場合分けします。 $t = \mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3$ のとき。$t_1 = \mathtt{true}$ ならば適用できるのは E-IfTrue だけです。E-If を使うには前提 $t_1 \to t_1'$ が要りますが、 (2) より $\mathtt{true}$ は簡約できないので E-If は使えません。よって $t' = t'' = t_2$ です。$t_1 = \mathtt{false}$ も同様です。$t_1$ が $\mathtt{true}$ でも $\mathtt{false}$ でもなければ E-IfTrue も E-IfFalse も形が合わないので、両方の簡約は E-If によるもので、それぞれ $t_1 \to s_1$、$t_1 \to s_1'$ を前提とします。帰納法の仮定より $s_1 = s_1'$ となり、$t' = t''$ が従います。 $t = \mathtt{pred}\ t_1$ のとき。$t_1 = \mathtt{0}$ ならば E-PredZero のみが適用でき（E-Pred の前提 $\mathtt{0} \to \cdot$ は (1) により成立しない）、$t' = t'' = \mathtt{0}$ です。$t_1 = \mathtt{succ}\ nv$（$nv$ は数値）ならば E-PredSucc が適用でき、E-Pred は前提 $\mathtt{succ}\ nv \to \cdot$ を要求しますが (1) よりこれは成立しません。よって $t' = t'' = nv$ です。**ここで補題 (1) が本質的に効いています**。$t_1$ が $\mathtt{succ}\ u$ の形でも $u$ が数値でない場合は、E-PredSucc の形が合わないので両方 E-Pred であり、帰納法の仮定で決まります。$t_1$ がそれ以外の形のときも E-Pred のみです。 $t = \mathtt{iszero}\ t_1$ の場合は $\mathtt{pred}$ と完全に同じ議論です。$t = \mathtt{succ}\ t_1$ のときは E-Succ のみが適用でき、帰納法の仮定から従います。$t$ が値のときは より簡約できないので、仮定に反し、この場合は起こりません。 決定性は「同じプログラムは何度動かしても同じ結果になる」ことの形式的な内容です。並行実行や乱数を導入するとこの定理は成り立たなくなり、その瞬間にデバッグの難しさが跳ね上がります（並行実行のときに順序を制御して結果を定める仕組みについては を参照してください）。 ## 5. 型：静的型付けと動的型付け の直後で見たように、L には行き詰まる項があります。型システムとは、**実行する前に**、行き詰まる項の一部を排除する仕組みです。 型を $T ::= \mathtt{Bool} \mid \mathtt{Nat}$ とする。関係 $\vdash t : T$（項 $t$ は型 $T$ を持つ）を次の規則で生成される最小の関係とする。 $$ \begin{aligned} &\text{(T-True)} && \vdash \mathtt{true} : \mathtt{Bool} \qquad &&\text{(T-False)} && \vdash \mathtt{false} : \mathtt{Bool} \qquad &&\text{(T-Zero)} && \vdash \mathtt{0} : \mathtt{Nat} \\[4pt] &\text{(T-If)} && \frac{\vdash t_1 : \mathtt{Bool} \quad \vdash t_2 : T \quad \vdash t_3 : T}{\vdash \mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 : T} &&\text{(T-Succ)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{succ}\ t : \mathtt{Nat}} \\[4pt] &\text{(T-Pred)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{pred}\ t : \mathtt{Nat}} &&\text{(T-Iszero)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{iszero}\ t : \mathtt{Bool}} \end{aligned} $$ T-If が $t_2$ と $t_3$ に**同じ** $T$ を要求している点に注目してください。この 1 箇所が、後で見る型システムの不完全性の主要な原因になります。 (1) $v$ が値で $\vdash v : \mathtt{Bool}$ ならば、$v = \mathtt{true}$ または $v = \mathtt{false}$ である。 (2) $v$ が値で $\vdash v : \mathtt{Nat}$ ならば、$v$ は数値である。 (1) 値は $\mathtt{true}$、$\mathtt{false}$、数値のいずれかです。$v$ が数値だと仮定すると、$v = \mathtt{0}$ なら型を与える規則は T-Zero だけなので $\vdash v : \mathtt{Nat}$ しか導けず、$\vdash v : \mathtt{Bool}$ に矛盾します。$v = \mathtt{succ}\ nv$ なら型を与える規則は T-Succ だけで、やはり結論は $\mathtt{Nat}$ です。よって $v$ は数値ではなく、$\mathtt{true}$ か $\mathtt{false}$ です。 (2) 同様に、$v = \mathtt{true}$ なら T-True により $\mathtt{Bool}$ しか導けず、$v = \mathtt{false}$ でも T-False により $\mathtt{Bool}$ しか導けません。いずれも仮定 $\vdash v : \mathtt{Nat}$ に矛盾するので、$v$ は数値です。 $\vdash t : T$ なる項 $t$ は、値であるか、または $t \to t'$ となる項 $t'$ が存在する。すなわち、型の付いた項は行き詰まり項ではない。 $\vdash t : T$ の導出に関する帰納法で示します。 T-True、T-False、T-Zero が最後に使われた場合、$t$ はそれぞれ $\mathtt{true}$、$\mathtt{false}$、$\mathtt{0}$ であり、いずれも値です。 T-If の場合、$t = \mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3$ で $\vdash t_1 : \mathtt{Bool}$ です。帰納法の仮定より、$t_1$ は値であるか簡約できます。簡約できるなら E-If により $t$ 全体も簡約できます。$t_1$ が値なら、$\vdash t_1 : \mathtt{Bool}$ と (1) より $t_1$ は $\mathtt{true}$ か $\mathtt{false}$ であり、E-IfTrue または E-IfFalse が適用できます。 T-Succ の場合、$t = \mathtt{succ}\ t_1$ で $\vdash t_1 : \mathtt{Nat}$ です。帰納法の仮定より $t_1$ は値か簡約可能です。簡約可能なら E-Succ で $t$ も簡約できます。値なら (2) より $t_1$ は数値なので、$\mathtt{succ}\ t_1$ 自体が数値、すなわち値です。 T-Pred の場合、$t = \mathtt{pred}\ t_1$ で $\vdash t_1 : \mathtt{Nat}$ です。$t_1$ が簡約可能なら E-Pred を使います。$t_1$ が値なら (2) より数値であり、数値は $\mathtt{0}$ か $\mathtt{succ}\ nv$ の形です。前者は E-PredZero、後者は E-PredSucc が適用できます。**この 2 通りで数値を尽くしている**ことが要点で、$\mathtt{pred}\ \mathtt{false}$ のような場合は $\vdash \mathtt{false} : \mathtt{Nat}$ が導けないため、そもそもこの場合分けに現れません。 T-Iszero の場合も同じ構造で、E-IszeroZero と E-IszeroSucc が数値のすべての形を覆っています。 $\vdash t : T$ かつ $t \to t'$ ならば $\vdash t' : T$ である。すなわち、簡約は型を変えない。 $t \to t'$ の導出に関する帰納法で、規則ごとに確かめます。以下、型付け規則は形で一意に決まるので、$t$ の形から最後に使われた型付け規則を逆に読み取れます（反転補題）。 E-IfTrue：$t = \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_2$。$\vdash t : T$ の導出は T-If で終わるので、前提として $\vdash t_2 : T$ があります。よって $\vdash t' : T$ です。E-IfFalse も同様に $\vdash t_3 : T$ が前提にあります。 E-If：$t \to \mathtt{if}\ t_1'\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3$ で前提は $t_1 \to t_1'$。T-If の前提から $\vdash t_1 : \mathtt{Bool}$、$\vdash t_2 : T$、$\vdash t_3 : T$。帰納法の仮定より $\vdash t_1' : \mathtt{Bool}$。この 3 つに T-If を適用して $\vdash t' : T$ を得ます。 E-Succ：T-Succ より $T = \mathtt{Nat}$ かつ $\vdash t_1 : \mathtt{Nat}$。帰納法の仮定より $\vdash t_1' : \mathtt{Nat}$、T-Succ を適用して $\vdash \mathtt{succ}\ t_1' : \mathtt{Nat}$。 E-PredZero：$\mathtt{pred}\ \mathtt{0} \to \mathtt{0}$。T-Pred より $T = \mathtt{Nat}$ で、T-Zero より $\vdash \mathtt{0} : \mathtt{Nat}$ です。 E-PredSucc：$\mathtt{pred}\ (\mathtt{succ}\ nv) \to nv$。T-Pred より $T = \mathtt{Nat}$ かつ $\vdash \mathtt{succ}\ nv : \mathtt{Nat}$。これを導けるのは T-Succ だけなので、その前提として $\vdash nv : \mathtt{Nat}$ があります。 E-Pred：T-Pred の前提 $\vdash t_1 : \mathtt{Nat}$ に帰納法の仮定を適用し、T-Pred を再適用します。 E-IszeroZero：$\mathtt{iszero}\ \mathtt{0} \to \mathtt{true}$。T-Iszero より $T = \mathtt{Bool}$ で、T-True より $\vdash \mathtt{true} : \mathtt{Bool}$。E-IszeroSucc も同じく T-False を使います。 E-Iszero：T-Iszero の前提に帰納法の仮定を適用し、T-Iszero を再適用します。以上ですべての簡約規則を尽くしました。 $\vdash t : T$ ならば、$t$ から始まる任意の簡約列 $t \to t_1 \to \cdots \to t_n$ について $t_n$ は行き詰まり項ではない。すなわち、型の付いたプログラムは実行の途中で行き詰まらない。 $n$ に関する帰納法です。 を $n$ 回繰り返し適用すると $\vdash t_n : T$ が得られます。この $t_n$ に を適用すると、$t_n$ は値であるか、さらに簡約できるかのいずれかです。行き詰まり項とは「値でない正規形」でしたから、$t_n$ はそのどちらの条件も同時には満たせず、行き詰まり項ではありません。 「進行 + 保存 = 健全性」というこの 2 段構えは、Wright と Felleisen が 1994 年に定式化して以来、型システムを設計するときの標準的な証明義務になっています。新しい言語機能を足したら、この 2 つの定理を証明し直す。それが「型システムを設計する」ことの実質です。 ### 5.1. 静的型検査は必ず不完全である で保証されるのは片側だけです。型が付けば安全ですが、逆は成り立ちません。$\mathtt{if}\ \mathtt{true}\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{false}$ は E-IfTrue で $\mathtt{0}$ に簡約されて何の問題もなく終わりますが、T-If が枝の型の一致を要求するため型が付きません。これは L という玩具言語の欠陥でしょうか。違います。 $\mathcal{L}$ をチューリング完全なプログラミング言語とし、$P$ を「実行しても型エラーで停止しないプログラム」全体の集合とする。$C \subseteq \mathcal{L}$ が決定可能（あるプログラムが $C$ に属するか否かを必ず有限時間で判定できる）かつ健全（$C \subseteq P$）ならば、$C \subsetneq P$ である。すなわち、安全であるのに $C$ が受理しないプログラムが必ず存在する。 まず $P$ が決定不能であることを、停止性問題からの帰着で示します。チューリング機械 $M$ と入力 $w$ の組が与えられたとき、次のプログラム $p_{M,w}$ を機械的に構成します。 ```text p(M, w) の本体: M を w 上でシミュレートする # 停止しないかもしれない 1 + true を評価する # ここに到達すれば必ず型エラー ``` $\mathcal{L}$ はチューリング完全なので $M$ のシミュレータを $\mathcal{L}$ で書けます。このとき、$p_{M,w}$ が型エラーを起こすのは、シミュレーションが停止して 2 行目に到達したとき、かつそのときに限ります。よって $$ p_{M,w} \in P \iff M \text{ は } w \text{ 上で停止しない} $$ が成り立ちます。$P$ が決定可能だとすると、この対応によって停止性問題も決定可能になり、チューリングの結果に矛盾します。よって $P$ は決定不能です。 さて $C$ は決定可能、$P$ は決定不能なので $C \ne P$ です。仮定より $C \subseteq P$ ですから、$C \subsetneq P$ が従います。$P \setminus C$ の元が、安全なのに受理されないプログラムです。
すべてのプログラム 安全なプログラム（決定不能） 型検査を通る if true then 0 else false （安全だが型が付かない）
### 5.2. 静的と動的の比較 | 観点 | 静的型付け（Java, OCaml, Rust, TypeScript） | 動的型付け（Python, Ruby, JavaScript） | |---|---|---| | 誤りの検出 | 実行前。到達しない経路の誤りも見つかる | 実行時。そのコードを通るテストが必要 | | 拒否されるプログラム | 安全でも型が付かないものを拒否する | 拒否しない。動かして初めて分かる | | 実行性能 | 型が確定するので値の表現を最適化できる | 実行時に型タグを検査する分の負荷がある | | 保守性 | 型が機械検査される仕様書として働く | 仕様は文書とテストに依存する | | 記述の柔軟さ | 型を通すための記述が必要になることがある | 試作や探索的なコードを短く書ける | | リファクタリング | 型検査器が呼び出し側の修正漏れを指摘する | 漏れは実行して初めて露見する | 静的型付けの「型を書く手間」は、型推論でかなり削れます。関数 `twice`（引数 `f` を 2 回適用する）の型を、制約を集めて解く方法で求めます。 $$ \mathtt{twice} = \lambda f.\ \lambda x.\ f\ (f\ x) $$ $f$ の型を型変数 $\alpha$、$x$ の型を $\beta$ と置きます。 1. 内側の適用 $f\ x$ が型付くには、$f$ は $\beta$ を受け取る関数でなければなりません。結果の型を $\gamma$ と置くと、制約 $\alpha = \beta \to \gamma$ が出ます。 2. 外側の適用 $f\ (f\ x)$ では、$f$ は $\gamma$ を受け取ります。結果を $\delta$ と置くと、制約 $\alpha = \gamma \to \delta$ が出ます。 3. 2 つの制約から $\beta \to \gamma = \gamma \to \delta$。関数型の等式は引数どうし・結果どうしの等式に分解できるので、$\beta = \gamma$ かつ $\gamma = \delta$ を得ます。 4. したがって $\gamma = \delta = \beta$、$\alpha = \beta \to \beta$ です。 全体の型は $(\beta \to \beta) \to \beta \to \beta$ となり、$\beta$ に制約が残っていないので全称量化して $\forall \beta.\ (\beta \to \beta) \to \beta \to \beta$ が得られます。**型注釈を 1 つも書かずに、最も一般的な型が一意に決まりました**。この手続きが Hindley–Milner 型推論であり、OCaml や Haskell、そして Rust の局所的な型推論の基礎になっています。 ## 6. パラダイム：関数型とオブジェクト指向 ### 6.1. 関数型：参照透過性が定理を生む 関数型プログラミングの理論的な母体は 1930 年代の $\lambda$ 計算です。項は変数 $x$、抽象 $\lambda x.\ t$、適用 $t_1\ t_2$ の 3 つだけで、計算規則も $\beta$ 簡約 $(\lambda x.\ t)\ u \to t[x := u]$ の 1 つだけです。この極小の体系がチューリング機械と同じ計算能力を持ちます。 $\lambda$ 計算の項 $t$ について、$t \twoheadrightarrow t_1$ かつ $t \twoheadrightarrow t_2$（$\twoheadrightarrow$ は $\beta$ 簡約の反射推移閉包）ならば、$t_1 \twoheadrightarrow s$ かつ $t_2 \twoheadrightarrow s$ となる項 $s$ が存在する。 証明は Tait と Martin-Löf による平行簡約を使う方法が標準で、Barendregt の教科書の第 3 章に完全な形が載っています。ここでは主張の意味だけ押さえてください。 が「簡約の順序が 1 通りしかない」ことを言っていたのに対し、Church–Rosser は「順序は複数あってよいが、**結果は合流する**」ことを言っています。だから正規形は高々 1 つに定まり、式のどの部分から評価しても最終結果は変わりません。並列実行や遅延評価が意味を壊さない根拠がここにあります。 評価関係が決定的であり、式の評価結果が自由変数への束縛のみに依存し、評価が計算機の状態（変数の書き換え、入出力、時刻など）を変化させないとき、その言語は**参照透過**であるという。 参照透過な言語において、式 $e$ が環境 $\rho$ のもとで値 $v$ に評価されるとする。このとき、$e$ を含む式の中で $e$ の 2 度の出現をどちらも $v$ で置き換えても、全体の評価結果は変わらない。 $e$ の 1 度目の評価が値 $v$ を返したとします。 より評価は状態を変化させないので、1 度目の評価の前後で環境 $\rho$ は同一です。したがって 2 度目の評価も同じ環境 $\rho$ のもとで行われます。同じ環境・同じ式に対する評価は、決定性の仮定より同じ値を返します。よって 2 度目の結果も $v$ です。両方の出現がいずれも $v$ に等しい値へ評価される以上、それらを $v$ で置き換えても全体の値は変わりません。 この命題が、$e$ を 1 度だけ計算して使い回す最適化（共通部分式除去）を正当化します。**逆に、参照透過性がないとこの最適化は不正になります**。 次の Python コードで、`f() + f()` を「共通部分式」とみなして 1 回の呼び出しにまとめると結果が変わります。 ```python counter = 0 def f(): global counter counter += 1 return counter print(f() + f()) # 1 + 2 = 3 counter = 0 a = f() print(a + a) # 1 + 1 = 2 ``` 出力は 3 と 2 で一致しません。 の「評価が状態を変化させない」という仮定が破れているため、 の証明の第 1 段（環境が同一であること）が成立しないからです。関数型言語が副作用を型で隔離したり禁止したりするのは、禁欲のためではなく、この種の等式変形を安全に使うためです。 ### 6.2. オブジェクト指向：動的ディスパッチと部分型 オブジェクト指向の中心は継承ではなく、**呼ぶべきコードを実行時に受け手が決める**という動的ディスパッチです。その正体は、データと関数ポインタを束ねたレコードにすぎません。 ```python def make_circle(r): return {"area": lambda: 3.14159 * r * r, "name": lambda: "円"} def make_square(s): return {"area": lambda: s * s, "name": lambda: "正方形"} shapes = [make_circle(1.0), make_square(2.0)] for sh in shapes: print(sh["name"](), sh["area"]()) # 円 3.14159 / 正方形 4.0 ``` `sh["area"]` がどの関数を指すかは、`sh` の中身を見るまで決まりません。機械語のレベルでは、これは「関数ポインタをメモリから読んで、そのアドレスへ間接ジャンプする」という 2 命令に落ちます（C++ や Java の仮想関数表がまさにこの構造です）。分岐先が静的に決まらないため、[コンピュータアーキテクチャと CPU の構造](/computer-science/cs-basics/computer-architecture) で扱った分岐予測が効きにくく、これが仮想呼び出しのコストの正体です（予測が外れるとパイプラインの利得が失われます。 を参照）。 型の間の関係 $S \le T$（$S$ は $T$ の部分型）を、次の**包摂規則**が健全であるような関係として要求する。 $$ \frac{\Gamma \vdash t : S \qquad S \le T}{\Gamma \vdash t : T} $$ すなわち、$T$ が期待される場所には $S$ の値をそのまま置いてよい。 これが Liskov の置換原則の型理論版です。では関数型どうしの部分型関係はどうなるでしょうか。 関数型の部分型関係は $$ S_1 \to S_2 \le T_1 \to T_2 \quad\Longleftarrow\quad T_1 \le S_1 \ \text{かつ}\ S_2 \le T_2 $$ で与えられる。すなわち引数の位置では**反変**（向きが逆）、結果の位置では**共変**（向きが同じ）である。 $f$ を型 $S_1 \to S_2$ の関数とし、これを $T_1 \to T_2$ が期待される場所で使ったとします。 の要求は「その使い方で型エラーが起きない」ことです。 引数について。呼び出し側は $T_1 \to T_2$ だと信じているので、$T_1$ 型の任意の値を渡してきます。$f$ が受け取れるのは $S_1$ 型の値なので、$T_1$ 型の値がすべて $S_1$ 型として通用しなければなりません。これはまさに $T_1 \le S_1$ です。 結果について。$f$ は $S_2$ 型の値を返します。呼び出し側はそれを $T_2$ 型として扱うので、$S_2$ 型の値がすべて $T_2$ 型として通用する必要があります。これが $S_2 \le T_2$ です。 以上より、この 2 条件のもとで $f$ の使用は型エラーを起こしません。 Java は配列を共変にしています。すなわち `String` が `Object` の部分型なら `String[]` も `Object[]` の部分型として扱われます。 の観点で言えば、配列への書き込みは引数の位置（`Object` を受け取る操作）なので、反変でなければ健全になりません。共変にした結果、次のコードはコンパイルを通ってしまいます。 ```java String[] names = new String[1]; Object[] objs = names; // 共変なので許される objs[0] = Integer.valueOf(42); // コンパイル時は Object[] なので通る ``` しかし実行すると 3 行目で `ArrayStoreException` が送出されます。これは でいう型健全性が破れている状態で、Java は実行時に配列の要素型を検査する動的チェックを追加して穴を塞いでいます。ジェネリクス（`List` と `List`）が非変に設計されているのは、同じ失敗を繰り返さないためです。 ### 6.3. どちらが「正しい」のか 両者は同じ問題の異なる面を最適化しています。「図形の種類」と「図形に対する操作」からなる 2 次元の表を考えると、拡張の方向が直交していることが見えます。 | | 新しいデータ（三角形を追加） | 新しい操作（周長を追加） | |---|---|---| | 関数型（代数的データ型 + パターンマッチ） | 既存の全関数に分岐を書き足す必要がある | 新しい関数を 1 つ足すだけで済む | | オブジェクト指向（クラス + 動的ディスパッチ） | 新しいクラスを 1 つ足すだけで済む | 既存の全クラスにメソッドを足す必要がある | これが Wadler の言う「式問題」です。片方が楽な方向は、もう片方では苦しい方向になります。近年の言語（Scala、Rust、Swift、Kotlin）が代数的データ型とトレイト・プロトコルの両方を備えているのは、対象の性質に応じて拡張しやすい側を選べるようにするためです。パラダイムは信条ではなく、拡張の軸をどちらに取るかという設計判断だと考えるのがよいでしょう。 ## 7. 演習 言語 L の項 $\mathtt{pred}\ (\mathtt{succ}\ (\mathtt{succ}\ \mathtt{0}))$ を、 の規則名を添えながら正規形まで簡約してください。また、この項に で型が付くことを確かめてください。 最外の項は $\mathtt{pred}\ u$（$u = \mathtt{succ}\ (\mathtt{succ}\ \mathtt{0})$）の形です。$u$ は $\mathtt{succ}\ nv$ で $nv = \mathtt{succ}\ \mathtt{0}$ は数値なので、E-PredSucc が適用できます。 $$ \mathtt{pred}\ (\mathtt{succ}\ (\mathtt{succ}\ \mathtt{0})) \to \mathtt{succ}\ \mathtt{0} \qquad (\text{E-PredSucc},\ nv = \mathtt{succ}\ \mathtt{0}) $$ $\mathtt{succ}\ \mathtt{0}$ は数値なので値であり、 (1) よりこれ以上簡約できません。1 ステップで正規形に到達しました。E-Pred を先に使おうとしても、その前提 $u \to u'$ が同じ補題により成立しないので使えません。 型付けは、T-Zero で $\vdash \mathtt{0} : \mathtt{Nat}$、T-Succ を 2 回適用して $\vdash \mathtt{succ}\ (\mathtt{succ}\ \mathtt{0}) : \mathtt{Nat}$、最後に T-Pred で $\vdash \mathtt{pred}\ (\mathtt{succ}\ (\mathtt{succ}\ \mathtt{0})) : \mathtt{Nat}$ です。 の主張どおり、簡約後の $\mathtt{succ}\ \mathtt{0}$ も T-Zero と T-Succ により $\mathtt{Nat}$ 型を持ちます。 言語 L の項で、型が付かないにもかかわらず、簡約すると値に到達する（行き詰まらない）ものを 1 つ挙げ、両方を確認してください。この現象が と矛盾しない理由も述べてください。 $t = \mathtt{if}\ (\mathtt{iszero}\ \mathtt{0})\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{false}$ を取ります。 **型が付かないこと**：$t$ に型を与えうる規則は T-If だけで、その前提は $\vdash \mathtt{0} : T$ と $\vdash \mathtt{false} : T$ を**同じ** $T$ について要求します。$\mathtt{0}$ に型を与える規則は T-Zero だけなので $T = \mathtt{Nat}$、$\mathtt{false}$ に型を与える規則は T-False だけなので $T = \mathtt{Bool}$ です。$\mathtt{Nat} \ne \mathtt{Bool}$ なので両立せず、$t$ には型が付きません。 **値に到達すること**：E-If の前提を E-IszeroZero で導いて $t \to \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{false}$、次に E-IfTrue で $\to \mathtt{0}$。$\mathtt{0}$ は値です。 **矛盾しない理由**： は「型が付く $\Rightarrow$ 行き詰まらない」という一方向の含意であり、その逆「行き詰まらない $\Rightarrow$ 型が付く」は主張していません。そして が示すとおり、逆向きが成り立つ決定可能な型システムは（チューリング完全な言語では）そもそも存在しません。$\mathtt{false}$ の枝は決して実行されませんが、型検査器は「どちらの枝も実行されうる」という保守的な前提で判断します。 の証明で、$t = \mathtt{iszero}\ t_1$ の場合を、 をどこで使うかを明示しながら完全に書いてください。 $t_1$ の形で場合分けします。 (a) $t_1 = \mathtt{0}$ のとき。適用候補は E-IszeroZero と E-Iszero です。E-Iszero を使うには前提 $\mathtt{0} \to t_1'$ が必要ですが、$\mathtt{0}$ は数値なので (1) よりこの前提は成立しません。よって適用できるのは E-IszeroZero だけで、$t' = t'' = \mathtt{true}$ です。 (b) $t_1 = \mathtt{succ}\ nv$（$nv$ は数値）のとき。$t_1$ 自身が数値なので、同じく (1) より E-Iszero の前提は成立しません。適用できるのは E-IszeroSucc だけで、$t' = t'' = \mathtt{false}$ です。 (c) $t_1 = \mathtt{succ}\ u$ で $u$ が数値でないとき。E-IszeroSucc は右辺の $nv$ が数値であることを要求するので形が合いません。E-IszeroZero も形が合いません。よって両方の簡約は E-Iszero によるもので、それぞれ前提 $t_1 \to s$、$t_1 \to s'$ を持ちます。帰納法の仮定より $s = s'$、したがって $t' = \mathtt{iszero}\ s = \mathtt{iszero}\ s' = t''$ です。 (d) $t_1$ が上のいずれでもないとき（$\mathtt{true}$、$\mathtt{false}$、あるいは $\mathtt{if}$ や $\mathtt{pred}$ で始まる項）。E-IszeroZero も E-IszeroSucc も形が合わないので、両方 E-Iszero であり、(c) と同じ議論で $t' = t''$ を得ます。なお $t_1$ が $\mathtt{true}$ や $\mathtt{false}$ の場合は (2) より E-Iszero の前提も成立せず、そもそも $t$ は簡約できないため、$t \to t'$ という仮定のもとでは起こりません。 関数型の部分型規則を「引数についても共変」、すなわち $S_1 \le T_1$ かつ $S_2 \le T_2$ ならば $S_1 \to S_2 \le T_1 \to T_2$ と定めたとします。型 `Cat` と `Dog` がともに `Animal` の部分型であるとして、この規則のもとで型検査を通るのに実行時に破綻するプログラムを構成してください。 関数 $g$ を「猫を受け取り、その猫に鳴かせる」ものとします。すなわち $g : \mathtt{Cat} \to \mathtt{Unit}$ で、本体では `Cat` にしかない操作（たとえば「爪を研ぐ」）を呼びます。 いま仮の共変規則を使うと、$\mathtt{Cat} \le \mathtt{Animal}$ かつ $\mathtt{Unit} \le \mathtt{Unit}$ より $$ \mathtt{Cat} \to \mathtt{Unit} \ \le\ \mathtt{Animal} \to \mathtt{Unit} $$ が導けます。よって の包摂規則により、$g$ を型 $\mathtt{Animal} \to \mathtt{Unit}$ の値として使えます。 そこで、$\mathtt{Animal} \to \mathtt{Unit}$ を引数に取る高階関数 $h$ に $g$ を渡し、$h$ の中で $\mathtt{Dog}$ の値を適用します。$\mathtt{Dog} \le \mathtt{Animal}$ なのでこの適用は型検査を通ります。しかし実行時に $g$ の本体は渡された値に「爪を研ぐ」を要求し、`Dog` にはその操作がないので破綻します。型が付いたのに行き詰まったので、 の型健全性が失われています。 正しい規則 では、$\mathtt{Cat} \to \mathtt{Unit} \le \mathtt{Animal} \to \mathtt{Unit}$ を導くには $\mathtt{Animal} \le \mathtt{Cat}$ が必要ですが、これは成り立たないため、最初の一歩が塞がれます。 の Java 配列は、まさにこの反変性を破った実例です。 ## 参考文献 - Benjamin C. Pierce, *Types and Programming Languages*, MIT Press, 2002 — 第 3 章（算術式の意味論）、第 8 章（型付き算術式、進行定理と保存定理）、第 15 章（部分型）。この記事の言語 L と定理の骨格はこの本の構成に沿っています。 - Robert Harper, *Practical Foundations for Programming Languages*, 2nd ed., Cambridge University Press, 2016 — 構造的操作的意味論と型安全性の一般的な扱い。 - A. Wright and M. Felleisen, "A Syntactic Approach to Type Soundness", *Information and Computation* 115 (1994), 38–94 — 進行と保存による型健全性証明の定式化。 - H. P. Barendregt, *The Lambda Calculus: Its Syntax and Semantics*, revised ed., North-Holland, 1984 — 第 3 章に Church–Rosser の定理の完全な証明。 - A. V. Aho, M. S. Lam, R. Sethi, J. D. Ullman, *Compilers: Principles, Techniques, and Tools*, 2nd ed., Addison-Wesley, 2006 — 字句解析から最適化・コード生成までの標準的な教科書。 - B. H. Liskov and J. M. Wing, "A Behavioral Notion of Subtyping", *ACM Transactions on Programming Languages and Systems* 16(6) (1994), 1811–1841 — 置換原則の厳密な定式化。 - RISC-V International, *The RISC-V Instruction Set Manual, Volume I: Unprivileged ISA* — [https://riscv.org/technical/specifications/](https://riscv.org/technical/specifications/) 命令形式と符号化の一次資料。