azdavis.net投稿

プログラミング言語を定義する:積

前の投稿では、発言に関数を追加しました。

この投稿では、積型を追加します。本格的なプログラミング言語では、積は struct、record、tuple などでも呼ばれています。

型を複数取り、一個の型に重ねることができるのは積です。例えば、関数から複数の値を戻したければ、積は使えます。

構文規則

型を二つ重ねる積型は「ペア」といって、τ1×τ2\tau_1 \times \tau_2で表記します。e1,e2\langle e_1, e_2 \rangleはペア定数の式です。

ペアを使い他のペアを合わせることによって、二個の型以上の積を作り上げられます。

ペアを使用する為、中身の値を抽出せねば。その為eLe \cdot \mathtt{L}eRe \cdot \mathtt{R}の射影式も追加します。eeはペアであれば、この式は左と右の値をペアから射影します。

次、他の型を一切含まぬ積型を紹介します。この型を「単位」(unit)と呼び、1\mathbf{1}で表記します。値が一つだけあるので、その値も「単位」と呼び、\langle \rangleで表記します。

値が一つしかないから、単位型はあまり役立たないと思われるかもしれません。しかし、関数から何も戻したくなかったら役立てます。

例えば、多くのプログラミング言語では、関数は副作用を実行できます。副作用というのは、値を戻す以外のこと、例えばファイルを変更したりインターネットに繋がったりすることを言います。

実は、或る関数は副作用の為だけに使われ、面白い値を戻す必要などありません。この場合、単位を戻すのが便利です。

違う言語は単位を他の名前で表します:

τ::=  1 τ1×τ2e::=   e1,e2 eL eR\begin{aligned} \tau ::= \ & \dots \\ | \ & \mathbf{1} \\ | \ & \tau_1 \times \tau_2 \\ \\ e ::= \ & \dots \\ | \ & \langle \rangle \\ | \ & \langle e_1, e_2 \rangle \\ | \ & e \cdot \mathtt{L} \\ | \ & e \cdot \mathtt{R} \end{aligned}

静的意味論

単位の値の型は単位です。

Γ:1\frac {} {\Gamma \vdash \langle \rangle: \mathbf{1}}

式が二つあって、それぞれには型があれば、ペアを作り出せます。

Γe1:τ1Γe2:τ2Γe1,e2:τ1×τ2\frac { \Gamma \vdash e_1: \tau_1 \hspace{1em} \Gamma \vdash e_2: \tau_2 } {\Gamma \vdash \langle e_1, e_2 \rangle: \tau_1 \times \tau_2}

左側か右側を射影できます。

Γe:τ1×τ2ΓeL:τ1\frac {\Gamma \vdash e: \tau_1 \times \tau_2} {\Gamma \vdash e \cdot \mathtt{L}: \tau_1}

Γe:τ1×τ2ΓeR:τ2\frac {\Gamma \vdash e: \tau_1 \times \tau_2} {\Gamma \vdash e \cdot \mathtt{R}: \tau_2}

動的意味論

単位は値。

 val\frac {} {\langle \rangle \ \mathsf{val}}

中の式が両方値である場合、ペアも値。

e1 vale2 vale1,e2 val\frac { e_1 \ \mathsf{val} \hspace{1em} e_2 \ \mathsf{val} } {\langle e_1, e_2 \rangle \ \mathsf{val}}

左側の式が踏み出せれば、ペアもできます。

e1e1e1,e2e1,e2\frac {e_1 \mapsto e_1'} {\langle e_1, e_2 \rangle \mapsto \langle e_1', e_2 \rangle}

左側は値ですけれど、右側は踏み出せれば、ペアもできます。

e1 vale2e2e1,e2e1,e2\frac { e_1 \ \mathsf{val} \hspace{1em} e_2 \mapsto e_2' } {\langle e_1, e_2 \rangle \mapsto \langle e_1, e_2' \rangle}

射影式は、まずペアを値にします。次、値である時にはペア定数になっていますから、それの左側か右側の式に踏み出します。

eeeLeL\frac {e \mapsto e'} {e \cdot \mathtt{L} \mapsto e' \cdot \mathtt{L}}

e1,e2 vale1,e2Le1\frac {\langle e_1, e_2 \rangle \ \mathsf{val}} {\langle e_1, e_2 \rangle \cdot \mathtt{L} \mapsto e_1}

eeeReR\frac {e \mapsto e'} {e \cdot \mathtt{R} \mapsto e' \cdot \mathtt{R}}

e1,e2 vale1,e2Re2\frac {\langle e_1, e_2 \rangle \ \mathsf{val}} {\langle e_1, e_2 \rangle \cdot \mathtt{R} \mapsto e_2}

助手

助手判断も機械的に更改します。

置き換え

[xe]=\frac {} {[x \mapsto e] \langle \rangle = \langle \rangle}

[xe]e1=e1[xe]e2=e2[xe]e1,e2=e1,e2\frac { [x \mapsto e] e_1 = e_1' \hspace{1em} [x \mapsto e] e_2 = e_2' } {[x \mapsto e] \langle e_1, e_2 \rangle = \langle e_1', e_2' \rangle}

[xe]e1=e1[xe]e1L=e1L\frac {[x \mapsto e] e_1 = e_1'} {[x \mapsto e] e_1 \cdot \mathtt{L} = e_1' \cdot \mathtt{L}}

[xe]e1=e1[xe]e1R=e1R\frac {[x \mapsto e] e_1 = e_1'} {[x \mapsto e] e_1 \cdot \mathtt{R} = e_1' \cdot \mathtt{R}}

自由変数

fv()=\frac {} {\mathsf{fv}(\langle \rangle) = \emptyset}

fv(e1)=s1fv(e2)=s2fv(e1,e2)=s1s2\frac { \mathsf{fv}(e_1) = s_1 \hspace{1em} \mathsf{fv}(e_2) = s_2 } {\mathsf{fv}(\langle e_1, e_2 \rangle) = s_1 \cup s_2}

fv(e)=sfv(eL)=s\frac {\mathsf{fv}(e) = s} {\mathsf{fv}(e \cdot \mathtt{L}) = s}

fv(e)=sfv(eR)=s\frac {\mathsf{fv}(e) = s} {\mathsf{fv}(e \cdot \mathtt{R}) = s}

語源

結論する前、「積」の語源を考えましょう。

積型は何ゆえそう呼ばれているかと聞くと、型の値の数が原因です。積型にある型の値の数をかければ、積型の値の数になります。

例えばBool\mathtt{Bool}には値が二つあります。true\mathtt{true}false\mathtt{false}

ではBool×Bool\mathtt{Bool} \times \mathtt{Bool}という型には値がいくつありますか。それは四つ。

  1. true,true\langle \mathtt{true}, \mathtt{true} \rangle
  2. true,false\langle \mathtt{true}, \mathtt{false} \rangle
  3. false,true\langle \mathtt{false}, \mathtt{true} \rangle
  4. false,false\langle \mathtt{false}, \mathtt{false} \rangle

Bool×1\mathtt{Bool} \times \mathbf{1}も見ましょう。Bool\mathtt{Bool}と同じく、値が二つあります。

  1. true,\langle \mathtt{true}, \langle \rangle \rangle
  2. false,\langle \mathtt{false}, \langle \rangle \rangle

ですから単位の型を1\mathbf{1}で書くのは妥当です。単位の型である1\mathbf{1}は、積型の×\timesの単位元です。

整数なら、任意の整数aaを取れば、

a×1=aa \times 1 = a

ここでは×\timesは掛け算。

同様に、τ|\tau|というのを「τ\tauの値の数」という意味を付け、任意な型τ\tauを取れば、

τ×1=τ|\tau \times \mathbf{1}| = |\tau|

ここでは×\timesは積型。

もっと全般的に言えば、

τ1×τ2=τ1×τ2|\tau_1 \times \tau_2| = |\tau_1| \times |\tau_2|

ここで左側の×\timesは積型で、右は掛け算を表します。

結論

定理の証明もまたGitHubにあります。

次の投稿では和型を追加します。