プログラミング言語を定義する:関数
翻訳:English • 日本語
前の投稿では、発言という整数とブーリアンの型があるプログラミング言語を紹介しました。
この投稿では、発言に関数を追加します。これで、発言の表現力は単純型付ラムダ計算とほぼ同じとなります。
式の構文規則を改め、変数、関数定数、そして関数適用を追加し、更に型の構文規則に関数型を追加します。
変数はxかyかx1かx′などで表記する。変数の名前は無限です。
λ(x:τ) eは関数定数で、xというτの型のある引数を一つ取り、実引数に適用されたらeを評価します。xはeの中に現れるのは可能です。
e1(e2)は関数適用式で、関数のe1を実引数のe2への適用を表現します。
τ1→τ2はτ1を入力とし、τ2を出力とする関数の型です。
τ::= ∣ e::= ∣ ∣ ∣ …τ1→τ2…xλ(x:τ) ee1(e2)
λ(x:Int) xの式をご覧ください。式の型はInt→Intのはずです。
それに似た式λ(x:Bool) xの型はBool→Boolのはずです。
この式両方では、xの式は含まれています。しかし、xの型は違います。一番目ではIntで、二番目ではBoolです。
この例に描かれたように、変数の型は、その変数はどう宣言されたによります。文脈により同じ式(この場合はx)の型が異なるというのは、今までなかったことです。
変数を対処する為、静的意味論の構造を根本的に改変せねばなりますまい。
まず、文脈というのを形式化します。一つの文脈をΓと表記し、それは変数と型のペアのリストです。
文脈は空か、既に存在する文脈に一つの変数と型のペアが追加された物です。
Γ::= ∣ ⋅Γ,x:τ前の型の判断はe:τで、「eの型はτだ」と読みましたが、新たなる判断はΓ⊢e:τと表記し、「Γはeの型がτだということを含意する」と読みます。
前の投稿の静的意味論の規則を改めなくてはいけません。これらは文脈を一切変えません。
Γ⊢n:IntΓ⊢true:BoolΓ⊢false:BoolΓ⊢if e1 then e2 else e3:τΓ⊢e1:BoolΓ⊢e2:τΓ⊢e3:τこれで新たな式の為の規則を定義します。
文脈により変数の型を調べる為、Γ(x)=τの判断を定義します。
(Γ,x:τ)(x)=τ(Γ,y:τ′)(x)=τx=yΓ(x)=τこの規則は「shadowing」という現象を生み出します。これは、同じ変数のある複数のペアが文脈に存在することができるけれど、そのペアの中、一番右のペアはその変数の型を決定する、ということを指します。例えば、規則によると
(⋅,x:Int,x:Bool,y:Int)(x)=Boolこの判断を使い、変数の型の規則を制作します。
Γ⊢x:τΓ(x)=τ関数定数は、仮引数の型は入力の方で、関数の本体の型は出力の型です。
しかし、関数定数に束縛された変数は、本体に現れるのは可能だから、本体の型を決める時だけに、変数とその型を文脈に追加します。
Γ⊢λ(x:τ1) e:τ1→τ2Γ,x:τ1⊢e:τ2適用は、仮引数と実引数の型が一致しなければなりません。
Γ⊢e1(e2):τ2Γ⊢e1:τ1→τ2Γ⊢e2:τ1
関数の本体は値かどうかにも関わらず、関数定数は値です。
λ(x:τ) e val適用式はまず関数、次実引数を値にします。
e1(e2)↦e1′(e2)e1↦e1′e1(e2)↦e1(e2′)e1 vale2↦e2′両方が値の時、関数は関数定数であることは証明できます。
関数本体に踏み出し、その式の中の関数により束縛された変数を実引数に置き換えます。「e′に、自由変数xをeに置き換えればe′′となる」を[x↦e]e′=e′′と表記します。
(λ(x:τ) e) e2↦e′e2 val[x↦e2]e=e′
関数適用の動的意味論を定義する為、式の置き換えをも定義します。
置き換えは整数とブーリアンの定数を変えません。
[x↦ex]n=n[x↦ex]true=true[x↦ex]false=false条件と適用の式は、ただその中の式に帰納します。
[x↦ex]if e1 then e2 else e3=if e1′ then e2′ else e3′[x↦ex]e1=e1′[x↦ex]e2=e2′[x↦ex]e3=e3′[x↦ex]e1(e2)=e1′(e2′)[x↦ex]e1=e1′[x↦ex]e2=e2′変数は、どうするかはその変数が置き換えられている変数かによります。そうであれば置き換えるけれど、そうでなければ無視します。
[x↦ex]x=ex[x↦ex]y=yx=y関数定数は、また変数が同じかどうかを見ます。同じだったら関数を変えません。これは、静的意味論では同じ変数のある複数のペアが文脈にある場合の扱い方に首尾一貫します。
[x↦ex]λ(x:τ) e=λ(x:τ) e変数が違ったら、変数捕獲を回避する必要があります。例えばもし
[x↦ex]λ(y:τ) e=λ(y:τ) e′x=y[x↦ex]e=e′を規則として定義したらば、規則を使い
[x↦y]λ(y:Bool) x=λ(y:Bool) yは証明できてしまうのです。この場合、変数のyは関数の束縛されたyにより捕獲されたのです。
これを回避する為、変数はeの自由変数ではないことを不可欠な前提とします。従って規則を改善し、exの中の自由変数をfv(ex)と表記します。
[x↦ex]λ(y:τ) e=λ(y:τ) e′x=yy∈/fv(ex)[x↦ex]e=e′
式の自由変数も定義します。
整数とブーリアンには変数がありません。
fv(n)=∅fv(true)=∅fv(false)=∅条件と適用はまた帰納します。
fv(if e1 then e2 else e3)=s1∪s2∪s3fv(e1)=s1fv(e2)=s2fv(e3)=s3fv(e1(e2))=s1∪s2fv(e1)=s1fv(e2)=s2一つの変数は自由。
fv(x)={x}関数は一つの変数を束縛し、その自由を奪います。
fv(λ(x:τ) e)=s∖{x}fv(e)=s
判断事態は少し変わったから、定理も少し言い直します。
For all Γ and e and τ, if Γ⊢e:τ and fv(e)=∅, then e val or there exists e′ such that e↦e′.
eには自由変数が全くないことを前提とします。これで、評価しながら必要となると置き換えられます。
この前提はなぜ必要かを答える為に、eを次の式にして見ましょう。
(λ(x:Bool→Bool) x) (λ(y:Bool) x)この式には自由変数のxがあります。規則によれば、この式は値ではなく、踏み出すこともできないのです。原因は、xは実引数には自由なのに関数に束縛されているのです。
もっと小さな例は式のxです。また規則によれば、変数は値ではなく、踏み出せません。変数は、置き換えにより意味が与えられるのです。
For all Γ and e and e′ and τ, if Γ⊢e:τ and fv(e)=∅ and e↦e′, then Γ⊢e′:τ and fv(e′)=∅.
維持定理は型だけではなく、自由変数の有無も維持します。e′を進歩させる為には自由変数がないのは進歩定理の前提として必要だから、その有無が維持できるのは大事です。
また、この定理を合わせれば安全定理の出来上がりです。
For all Γ and e and τ, if Γ⊢e:τ and fv(e)=∅, then e val or there exists e′ such that e↦e′ and Γ⊢e′:τ and fv(e′)=∅.
証明はまたGitHubにあります。
次の投稿では、積型を紹介します。これらを struct や tuple とも言います。