プログラミング言語を定義する：関数

翻訳：English • 日本語

前の投稿では、発言という整数とブーリアンの型があるプログラミング言語を紹介しました。

この投稿では、発言に関数を追加します。これで、発言の表現力は単純型付ラムダ計算とほぼ同じとなります。

構文規則

式の構文規則を改め、変数、関数定数、そして関数適用を追加し、更に型の構文規則に関数型を追加します。

変数はxxかyyかx1x_1かx′x'などで表記する。変数の名前は無限です。

λ(x:τ) e\lambda (x: \tau) \ eは関数定数で、xxというτ\tauの型のある引数を一つ取り、実引数に適用されたらeeを評価します。xxはeeの中に現れるのは可能です。

e1(e2)e_1(e_2)は関数適用式で、関数のe1e_1を実引数のe2e_2への適用を表現します。

τ1→τ2\tau_1 \rightarrow \tau_2はτ1\tau_1を入力とし、τ2\tau_2を出力とする関数の型です。

τ::= …∣ τ1→τ2e::= …∣ x∣ λ(x:τ) e∣ e1(e2) \begin{aligned} \tau ::= \ & \dots \\ | \ & \tau_1 \rightarrow \tau_2 \\ \\ e ::= \ & \dots \\ | \ & x \\ | \ & \lambda (x: \tau) \ e \\ | \ & e_1(e_2) \end{aligned}

静的意味論：Γ⊢e:τ\Gamma \vdash e: \tau

λ(x:Int) x\lambda (x: \mathsf{Int}) \ xの式をご覧ください。式の型はInt→Int\mathsf{Int}\rightarrow \mathsf{Int}のはずです。

それに似た式λ(x:Bool) x\lambda (x: \mathsf{Bool}) \ xの型はBool→Bool\mathsf{Bool} \rightarrow \mathsf{Bool}のはずです。

この式両方では、xxの式は含まれています。しかし、xxの型は違います。一番目ではInt\mathsf{Int}で、二番目ではBool\mathsf{Bool}です。

この例に描かれたように、変数の型は、その変数はどう宣言されたによります。文脈により同じ式（この場合はxx）の型が異なるというのは、今までなかったことです。

変数を対処する為、静的意味論の構造を根本的に改変せねばなりますまい。

まず、文脈というのを形式化します。一つの文脈をΓ\Gammaと表記し、それは変数と型のペアのリストです。

文脈は空か、既に存在する文脈に一つの変数と型のペアが追加された物です。

Γ::= ⋅∣ Γ,x:τ \begin{aligned} \Gamma ::= \ & \cdot \\ | \ & \Gamma, x: \tau \end{aligned}

前の型の判断はe:τe: \tauで、「eeの型はτ\tauだ」と読みましたが、新たなる判断はΓ⊢e:τ\Gamma \vdash e: \tauと表記し、「Γ\Gammaはeeの型がτ\tauだということを含意する」と読みます。

前の投稿の静的意味論の規則を改めなくてはいけません。これらは文脈を一切変えません。

Γ⊢n‾:Int \frac {} {\Gamma \vdash \overline{n}: \mathsf{Int}} Γ⊢true:Bool \frac {} {\Gamma \vdash \mathsf{true}: \mathsf{Bool}} Γ⊢false:Bool \frac {} {\Gamma \vdash \mathsf{false}: \mathsf{Bool}} Γ⊢e1:BoolΓ⊢e2:τΓ⊢e3:τΓ⊢if e1 then e2 else e3:τ \frac { \Gamma \vdash e_1: \mathsf{Bool} \hspace{1em} \Gamma \vdash e_2: \tau \hspace{1em} \Gamma \vdash e_3: \tau } { \Gamma \vdash \mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3: \tau }

これで新たな式の為の規則を定義します。

文脈により変数の型を調べる為、Γ(x)=τ\Gamma(x) = \tauの判断を定義します。

(Γ,x:τ)(x)=τ \frac {} {(\Gamma, x: \tau)(x) = \tau} x≠yΓ(x)=τ(Γ,y:τ′)(x)=τ \frac { x \ne y \hspace{1em} \Gamma(x) = \tau } {(\Gamma, y: \tau')(x) = \tau}

この規則は「shadowing」という現象を生み出します。これは、同じ変数のある複数のペアが文脈に存在することができるけれど、そのペアの中、一番右のペアはその変数の型を決定する、ということを指します。例えば、規則によると

(⋅,x:Int,x:Bool,y:Int)(x)=Bool (\cdot, x: \mathsf{Int}, x: \mathsf{Bool}, y: \mathsf{Int})(x) = \mathsf{Bool}

この判断を使い、変数の型の規則を制作します。

Γ(x)=τΓ⊢x:τ \frac {\Gamma(x) = \tau} {\Gamma \vdash x: \tau}

関数定数は、仮引数の型は入力の方で、関数の本体の型は出力の型です。

しかし、関数定数に束縛された変数は、本体に現れるのは可能だから、本体の型を決める時だけに、変数とその型を文脈に追加します。

Γ,x:τ1⊢e:τ2Γ⊢λ(x:τ1) e:τ1→τ2 \frac {\Gamma, x: \tau_1 \vdash e: \tau_2} {\Gamma \vdash \lambda (x: \tau_1) \ e: \tau_1 \rightarrow \tau_2}

適用は、仮引数と実引数の型が一致しなければなりません。

Γ⊢e1:τ1→τ2Γ⊢e2:τ1Γ⊢e1(e2):τ2 \frac { \Gamma \vdash e_1: \tau_1 \rightarrow \tau_2 \hspace{1em} \Gamma \vdash e_2: \tau_1 } {\Gamma \vdash e_1(e_2): \tau_2}

動的意味論：e vale \ \mathsf{val}とe↦e′e \mapsto e'

関数の本体は値かどうかにも関わらず、関数定数は値です。

λ(x:τ) e val \frac {} {\lambda (x: \tau) \ e \ \mathsf{val}}

適用式はまず関数、次実引数を値にします。

e1↦e1′e1(e2)↦e1′(e2) \frac {e_1 \mapsto e_1'} {e_1(e_2) \mapsto e_1'(e_2)} e1 vale2↦e2′e1(e2)↦e1(e2′) \frac { e_1 \ \mathsf{val} \hspace{1em} e_2 \mapsto e_2' } {e_1(e_2) \mapsto e_1(e_2')}

両方が値の時、関数は関数定数であることは証明できます。

関数本体に踏み出し、その式の中の関数により束縛された変数を実引数に置き換えます。「e′e'に、自由変数xxをeeに置き換えればe′′e''となる」を[x↦e]e′=e′′[x \mapsto e] e' = e''と表記します。

e2 val[x↦e2]e=e′(λ(x:τ) e) e2↦e′ \frac { e_2 \ \mathsf{val} \hspace{1em} [x \mapsto e_2] e = e' } { (\lambda (x: \tau) \ e) \ e_2 \mapsto e' }

置き換え：[x↦ex]e=e′[x \mapsto e_x] e = e'

関数適用の動的意味論を定義する為、式の置き換えをも定義します。

置き換えは整数とブーリアンの定数を変えません。

[x↦ex]n‾=n‾ \frac {} {[x \mapsto e_x] \overline{n} = \overline{n}} [x↦ex]true=true \frac {} {[x \mapsto e_x] \mathsf{true} = \mathsf{true}} [x↦ex]false=false \frac {} {[x \mapsto e_x] \mathsf{false} = \mathsf{false}}

条件と適用の式は、ただその中の式に帰納します。

[x↦ex]e1=e1′[x↦ex]e2=e2′[x↦ex]e3=e3′[x↦ex]if e1 then e2 else e3=if e1′ then e2′ else e3′ \frac { \begin{aligned} &[x \mapsto e_x] e_1 = e_1' \hspace{1em} \\&[x \mapsto e_x] e_2 = e_2' \hspace{1em} \\&[x \mapsto e_x] e_3 = e_3' \end{aligned} } { \begin{aligned} [x \mapsto e_x] &\mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3 = \\&\mathsf{if} \ e_1' \ \mathsf{then} \ e_2' \ \mathsf{else} \ e_3' \end{aligned} } [x↦ex]e1=e1′[x↦ex]e2=e2′[x↦ex]e1(e2)=e1′(e2′) \frac { [x \mapsto e_x] e_1 = e_1' \hspace{1em} [x \mapsto e_x] e_2 = e_2' } { [x \mapsto e_x] e_1(e_2) = e_1'(e_2') }

変数は、どうするかはその変数が置き換えられている変数かによります。そうであれば置き換えるけれど、そうでなければ無視します。

[x↦ex]x=ex \frac {} {[x \mapsto e_x] x = e_x} x≠y[x↦ex]y=y \frac {x \ne y} {[x \mapsto e_x] y = y}

関数定数は、また変数が同じかどうかを見ます。同じだったら関数を変えません。これは、静的意味論では同じ変数のある複数のペアが文脈にある場合の扱い方に首尾一貫します。

[x↦ex]λ(x:τ) e=λ(x:τ) e \frac {} {[x \mapsto e_x] \lambda (x: \tau) \ e = \lambda (x: \tau) \ e}

変数が違ったら、変数捕獲を回避する必要があります。例えばもし

x≠y[x↦ex]e=e′[x↦ex]λ(y:τ) e=λ(y:τ) e′ \frac { x \ne y \hspace{1em} [x \mapsto e_x] e = e' } {[x \mapsto e_x] \lambda (y: \tau) \ e = \lambda (y: \tau) \ e'}

を規則として定義したらば、規則を使い

[x↦y]λ(y:Bool) x=λ(y:Bool) y[x \mapsto y] \lambda (y: \mathsf{Bool}) \ x = \lambda (y: \mathsf{Bool}) \ y

は証明できてしまうのです。この場合、変数のyyは関数の束縛されたyyにより捕獲されたのです。

これを回避する為、変数はeeの自由変数ではないことを不可欠な前提とします。従って規則を改善し、exe_xの中の自由変数をfv(ex)\mathsf{fv}(e_x)と表記します。

x≠yy∉fv(ex)[x↦ex]e=e′[x↦ex]λ(y:τ) e=λ(y:τ) e′ \frac { x \ne y \hspace{1em} y \notin \mathsf{fv}(e_x) \hspace{1em} [x \mapsto e_x] e = e' } {[x \mapsto e_x] \lambda (y: \tau) \ e = \lambda (y: \tau) \ e'}

自由変数：fv(e)\mathsf{fv}(e)

式の自由変数も定義します。

整数とブーリアンには変数がありません。

fv(n‾)=∅ \frac {} {\mathsf{fv}(\overline{n}) = \emptyset} fv(true)=∅ \frac {} {\mathsf{fv}(\mathsf{true}) = \emptyset} fv(false)=∅ \frac {} {\mathsf{fv}(\mathsf{false}) = \emptyset}

条件と適用はまた帰納します。

fv(e1)=s1fv(e2)=s2fv(e3)=s3fv(if e1 then e2 else e3)=s1∪s2∪s3 \frac { \mathsf{fv}(e_1) = s_1 \hspace{1em} \mathsf{fv}(e_2) = s_2 \hspace{1em} \mathsf{fv}(e_3) = s_3 } { \mathsf{fv}(\mathsf{if} \ e_1 \ \mathsf{then} \ e_2 \ \mathsf{else} \ e_3) = s_1 \cup s_2 \cup s_3 } fv(e1)=s1fv(e2)=s2fv(e1(e2))=s1∪s2 \frac { \mathsf{fv}(e_1) = s_1 \hspace{1em} \mathsf{fv}(e_2) = s_2 } { \mathsf{fv}(e_1(e_2)) = s_1 \cup s_2 }

一つの変数は自由。

fv(x)={x} \frac {} {\mathsf{fv}(x) = \{ x \}}

関数は一つの変数を束縛し、その自由を奪います。

fv(e)=sfv(λ(x:τ) e)=s∖{x} \frac {\mathsf{fv}(e) = s} {\mathsf{fv}(\lambda (x: \tau) \ e) = s \setminus \{ x \}}

定理

判断事態は少し変わったから、定理も少し言い直します。

進歩

For all Γ\Gamma and ee and τ\tau, if Γ⊢e:τ\Gamma \vdash e: \tau and fv(e)=∅\mathsf{fv}(e) = \emptyset, then e vale \ \mathsf{val} or there exists e′e' such that e↦e′e \mapsto e'.

eeには自由変数が全くないことを前提とします。これで、評価しながら必要となると置き換えられます。

この前提はなぜ必要かを答える為に、eeを次の式にして見ましょう。

(λ(x:Bool→Bool) x) (λ(y:Bool) x) (\lambda (x: \mathsf{Bool} \rightarrow \mathsf{Bool}) \ x) \ (\lambda (y: \mathsf{Bool}) \ x)

この式には自由変数のxxがあります。規則によれば、この式は値ではなく、踏み出すこともできないのです。原因は、xxは実引数には自由なのに関数に束縛されているのです。

もっと小さな例は式のxxです。また規則によれば、変数は値ではなく、踏み出せません。変数は、置き換えにより意味が与えられるのです。

維持

For all Γ\Gamma and ee and e′e' and τ\tau, if Γ⊢e:τ\Gamma \vdash e: \tau and fv(e)=∅\mathsf{fv}(e) = \emptyset and e↦e′e \mapsto e', then Γ⊢e′:τ\Gamma \vdash e': \tau and fv(e′)=∅\mathsf{fv}(e') = \emptyset.

維持定理は型だけではなく、自由変数の有無も維持します。e′e'を進歩させる為には自由変数がないのは進歩定理の前提として必要だから、その有無が維持できるのは大事です。

安全

また、この定理を合わせれば安全定理の出来上がりです。

For all Γ\Gamma and ee and τ\tau, if Γ⊢e:τ\Gamma \vdash e: \tau and fv(e)=∅\mathsf{fv}(e) = \emptyset, then e vale \ \mathsf{val} or there exists e′e' such that e↦e′e \mapsto e' and Γ⊢e′:τ\Gamma \vdash e': \tau and fv(e′)=∅\mathsf{fv}(e') = \emptyset.

証明はまたGitHubにあります。

次の投稿では、積型を紹介します。これらを struct や tuple とも言います。