タグ: ラムダ計算

型付きλ計算と単純な拡張

 記事「プログラミング言語を形式的に取り扱う」、「ラムダ抽象への型の割りあて」において、変数、ラムダ抽象、関数適用の3つの要素からなるラムダ項に対して、型付け規則を導入しました。

 型の導入の仕方にはおおきく2つあります。最初に項を定義して、それらがどうふるまうかどうかを示す評価の部分、意味論を定義し、最後にプログラム的に意味を持たない型システムを導入するスタイルをカリースタイルとよびます。

 それに対して、項を定義し、それに対する型付け規則を定義して、正しく片付けされた項にのみ意味付けをするという、型付けが意味論に対して優先されるものをチャーチスタイルとよびます。

 これらどちらのスタイルを取るにしても、型付け規則は文字通り、項に対してどう型付けをするかという規則なだけで、型とはどういうものかは定義されていません。一般のプログラミング言語にはあらかじめ定義された基本型、あるいはプリミティブ型などとよばれる型があるのが一般的です。そこで型付きラムダ計算の単純な拡張として、まず基本型を定義するところからはじめていきましょう。

基本型の導入と単純型付きラムダ計算の拡張

 一般的なプログラミング言語でのプリミティブ型は数やブール値や文字などで、それらは構造を持たない単純な値の集合と考えることができます。また多くの場合、これらを操作するための適切な演算も定義されている。こうしたものを基本型の集合 Aと書くことにします。基本型は型システム的には内部構造を持たないため、原子型ともよばれています。これを型の定義に追加するとすれば、以下のような形になります。

型 T ::= T → T | A (原子型)

 基本的な数値を用いて組を作るということは計算をするときによくやります。たとえばほとんどの人は、数学で数字と数字を組み合わせて2次元座標を表現した経験があると思います。より難しい言葉でこの組の構造を表現すると「型 T, U の直積 {t ,u}」とか言ったりします。このときこの組の型は T × U という書き方をします。

 直積を導入する際に、第1要素と第2要素をそれぞれ取り出せないとデータ構造として不便というか使い物になりません。そこでそれぞれを取り出す構文として {t, u}.1 と {t, u}.2 を導入します。これはまた小難しい用語で射影などとよばれていたりします。

 さて、単純型付きラムダ計算を拡張してこれを導入するためには追加で以下の構文・評価・型付け規則の導入が必要になります。

コンポジットなパターン

 さて、もう少し複雑な拡張を考えてみることにしましょう。多くのプログラムでは種類が違う値が混合した集まりを扱う必要性があります。例えばディレクトリ構造を表現するような場合、要素としてフォルダとファイルという異なる種類のものを持てる必要性があります。これはより一般的にいえばこういう構造を木構造とよばれている、葉と枝という違った要素を子として持つような構造を指します。

 これまではある要素に対してはこの型の値しか入らないという硬直したシステムを取っていました。しかしこれでは木構造のようなものの表現がなかなか難しくなります。そこで、ざっくり言ってしまうと 「型 T か 型 U のどちらかが入っているような型」というものを定義してしまうことにしましょう。これは数学的に言うと、直和とよばれているもので T + U と書いたりします。

 T + U 型の値をつくるためには T の値、 U の値にそれぞれタグ付けをすれば良いです。T + U の表記の順番に従って、左側の型の値を left t として、右側の型の値を right r とします。

 また、この T + U 型の値は計算をするときは取り出せなければ困ります。そのためのパターンマッチ的な構文 case(x: T + U) of left t ~> t’ | right u ~> u’ も導入しておきます。このとき追加すべき構文・評価・型付け規則は以下のようになります。

 これで晴れて Int + Int や Int + Bool のような型とその値を表現できるようになりました。このような形は実際ScalaやHaskellといった言語では Either という形で実装されています。Javaなどでは、GoFのコンポジットパターンを用いて実装することができます。

 ちなみに直和型 T + U は T と U のすべての要素をどちらの集合出身かというラベリングをした上で保持するため、要素の数は T の要素の数と U の要素の数の和になっています。直積型 T × U は T と U それぞれの要素の数の組み合わせ、つまり掛け算した数だけ要素を持っています。

ラムダ抽象への型の割りあて

 ブール値と単純なラムダ計算を組み合わせた言語を考えてみましょう。このとき例えば以下のような項の正確な型解析は困難です。

if <<とても長く複雑な計算>> then true else (λx.x)

 これは実際に条件の項を評価するまで、ブール値を返すのか、関数を返すのか判断がつきません。しかしながら、ブール値も関数も両方ともラムダ抽象として表現することができます。つまり、true は λx.true と読み替え、λx.x は λx.y.y と読み替えるということです。

 そこでラムダ抽象自体に 型 → を割り当てる型付け規則 λx.t: → を追加すると先ほどの if 文は → と型付けすることができます。まあでもちょっとこれは無理がありますね。then節とelse節で返すものをむりやり → として同一視しましたが、結局は違うものなので、あまり意味がないのです。

 つまりただ単に関数が返されるというだけでなく、その関数がどんな型を返すのかということがわからなければ有用でないということになります。さらに関数が呼び出されたときに正しく振る舞うことを保証するために、引数の型がどうあるべきかということも分からなければ困ります。

ラムダ抽象に型を割り当てる

 もう一度、λx.t のようなラムダ抽象に型を割り当てることについて考えてみましょう。これまでにわかったようにラムダ抽象が引数に適用するとどんな型を返すのかということと、引数に期待されている型が何かという情報が必要そうです。

 引数に期待されている型がわかるようにラムダ抽象 λx.t を λx:T. t と書くようにしましょう。このときこのラムダ抽象における引数 x は 型 T の値となることが期待されることを意味します。

 さて次にラムダ抽象 λx.t の返す型についてですが、正しい型の引数 x が与えられれば、 t の型になるのは明らかです。t の型を U としておきましょう。そうするとこのラムダ抽象は型 T の引数を受け取り、型 U の値を返すという特徴を持った関数であると言えます。

 これを直感的に T → U と書くとわかりやすいのではないでしょうか。さらにこれは冒頭で定義したラムダ抽象への型付け → で不足していた情報が補われた形となっています。さて、それではこういったものを型の体系に組み込むために型 Bool 上の単純型の集合を次のように定義しておきます。

 こうするとラムダ抽象への型付け規則を以下のように定義することができます(推論式の上段 => 推論式の下段という書き方をしています)。

 またラムダ抽象は入れ子になり得るために、自由変数がどんな型を持つかという情報が必要になります。したがって型付け関係は t: T の二項関係ではなく、Γ ├ t:T という三項関係になり、ちょっと複雑になります。Γ は型付け文脈や型環境と呼ばれたりします。文脈を持たない場合は Φ ├ t:T または省略して ├ t:T などと書きます。

 ラムダ抽象への型付け規則のより一般的なものは以下のようになります。

ラムダ計算への単純な型付け

 ラムダ計算は変数・ラムダ抽象・関数適用からなるというものでした。うちラムダ抽象に対して型付け規則を定義しました。ここでは残りの変数と、関数適用についても型付け規則を定義してみましょう。

まとめると以下のような形になります。

 このように規定される計算を単純型付きラムダ計算とよびます。

ラムダ計算について調べた(前編)

関数プログラミングとその背景にある数学的なお話を理解する上でラムダ計算の知識が必要そうなので,確認していきます. というかなんかよくよく調べていくと,「計算機科学の理論としては常識」とか書いてあったりするので,あせって基礎をさらいました. まずは型なしのラムダ計算まで. 間違ったところがあったらご指摘頂けると嬉しいです.

ラムダ計算とは何か?

Wikipediaによるとラムダ計算とは次のようなものとされています.

ラムダ計算(lambda calculus)は、計算模型のひとつで、計算の実行を関数への引数の評価(evaluation)と適用(apply)としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。

ラムダ計算では,関数をラムダ抽象を使って記述します. たとえば f(x)=2x+1 なる関数は f=λx.2x+1 というように書きます. こうすることにより,関数を返す関数などを定義することができるようになります. また名前をつけずに値のように関数を取り扱えるようになりました.

たとえば, g(x,y)=x+2y+1 は g=λx.(λy.x+2y+1) といったように 2変数関数は,1変数を返す関数として定義することができます.このような変換をカリー化(currying)とよびます. また関数を値として受け取ったり,返したりする関数のことを高階関数(higher-order function)とよびます.

関数に値を適用したい場合はラムダ抽象の後ろに値を書けば良いです. たとえば f(x)=2x+1 に x=2 を適用するときは ((λx.2x+1)2) と書きます. これを関数適用といいます.

またλx.x+y についてx は束縛されているといい y は自由であるといいます.

型なしラムダ計算(lambda calculus)

ラムダ式の構文

型なしラムダ計算の抽象構文は e::=x|λx.e|e1e2 のように定義されます. 単純にいうとラムダ式は,変数か,ラムダ抽象か,関数適用から構成されるということです.

ラムダ計算の実行

ラムダ計算の実行はα-変換,β-簡約,η-変換の3つの操作に抽象化できます.

  • α-変換(α-conversion)
    • λx.M→αλy.M[x:=y]
    • 束縛変数の名前はMの中に自由なyがなければ置き換えられる:λx.f⇒λy.f[x→y]
  • β-簡約(β-reduction)
    • (λx.M)N→βM[x:=N]
    • 関数適用そのものを指す:λx.fy⇒f[x→y]
  • η-変換(η-conversion)
    • λx.Mx→ηM
    • 関数の外延性を表す:λx.fx⇒λy.f

ラムダによるデータの表現

自然数

以下のように自然数をラムダ式で表せる.このようなラムダ式をチャーチ数(Church Number)とよびます.

  • 0 を λs.λz.z
  • 1 を λs.λz.sz
  • 2 を λs.λz.s(sz)

これは足し算を plus=λg1.λg2.λs.λz.g2sg1z を定義して, plus 1 2 などを計算してみると納得がいくと思います

論理値

論理値 true は λt,λf.t ,false は λt.λf.f とすると, if e1 then e2 else e3 を e1e2e3 としてうまい具合にif-elseの構造を表せる. これは if true then e1 else e2 = true e1 e2 = (λt.λf.t)e2e3 →(λt.e2)e3→e2 かつ if false then e1 else e2 = false e1 e2 = (λt.λf.f)e2e3 →(λf.g)e3→e3 となることから納得がいくと思います.

その他 この資料 が結構良い感じにまとまっています