月別: 2015年1月

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

 記事「プログラミング言語を形式的に取り扱う」、「ラムダ抽象への型の割りあて」において、変数、ラムダ抽象、関数適用の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 などと書きます。

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

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

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

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

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

プログラミング言語を形式的に取り扱う

 型なしの算術式と型付きの算術式を例に、計算がどのように体系付けられていくのか、その流れの一例をみていきます。これによりプログラミング言語の基本的な側面を形式的に取り扱うことができます。

 ちなみにこの記事は型システム入門とプログラム意味論という本を参考にして書いてます。厳密でないところや間違ったところがたくさんあると思いますが、気になる箇所はこちらの本をあたると良いと思います。間違いなどはこっそりコメントを頂けたりすると嬉しいです。

言語構文の定義付けについて考える

 次のように、真理値true, false、条件式、数値定数0、後者関数 succ、前者関数 pred、ゼロ判定の演算子iszero の簡単な構文からなる小さな言語を考えてみましょう。

これと同じことを次のように帰納的な形で定義することもできます。

また以下のように推論規則による定義の仕方もあります。

[推論規則による項の定義] 項の集合は次の規則によって定義される
rule
 この推論規則は、上段を前提として下段を導けるというものです。とくに上段がない、つまり前提を必要としない規則のことを特に公理と呼びます。また以下のように項の要素を生成する具体的手続きを書き下すことによる定義の仕方もあります。

[具体的な項の定義] 自然数 i について、集合T_i、 項の集合 T をそれぞれ以下のように定義する。
rule2

項の評価について考える

 以上のように色々な方法で言語の構文を定式化できました。さてプログラミング言語を考えるときには各項がどのように評価されるということも考えなければなりません。この評価がどのようにされるかという議論を意味論と呼びます。意味論の形式化にも様々なバリエーションがあります。

 さて、手始めにブール値の評価について考えてみましょう。すると次の3つの評価関係が成り立つと一般的な言語機能として良さそうだということはなんとなく分かるかと思います。

 このように項の状態に対して遷移規則を定めることにより、項の評価を定義していく方法を操作的意味論と言います(そのなかでもスモールステップ意味論というスタイルになります)。なお表記の都合上、推論規則は (上段) => (下段) という書き方をしています。

 この3つの規則が何を言っているのかと同じくらい、何を言っていないのかということも重要です。たとえばこれらの規則から「if全体が評価される前にthen節やelse節が評価されることはない」という評価戦略が読み取れます。

 この3つの評価関係から例えばif false then false else true という項は、(2) を適用して true という値に評価することができます。true はこれ以上適用できる規則がありません。このような項を正規形と呼びます。

評価できない項

 ブール値の評価について定めましたが数値についてはまだでした。まとめて評価規則を定義しましょう。まずは構文と値の再確認をしておきます。

つづいて評価規則についてみてみます。

 このように言語の操作的意味論を形式化すると、例えば succ true のようにこれ以上評価できない、つまり正規形であるが、値ではないというようなパターンが生まれてしまいます。こういうような項を行き詰まり状態と呼びます。

 プログラミング言語の機能としてこの行き詰まり状態をどう扱うかということはひとつ大きな課題となります。エラーを表す新しい項を導入したり、型を導入してこの手のエラーを予め防ぐなどいくつかのアプローチがあります。

型の導入による行き詰まり状態の回避の試み

 項を実際には評価せずとも succ true のような行き詰まり状態にならないことが分かると便利です。このような仕組みのひとつとして型を導入することを考えましょう。前述の言語では、値として数値とブール値を扱っていたためそれらに対応する型 Nat と Bool を導入します。

 以上のような型付け規則により、項 t が評価したときにある型の値になることを静的に、つまり評価することなく判断することができるようになります。項 t に対してある型 T が存在して、t: T となるとき t は型付け可能と言います。

安全性を支える型システム

 行き詰まり状態を回避する手段のひとつとして型を導入したことからも何となく分かるように、型システムの最も基本的な性質は「安全性」です。正しく型付けされた項は行き詰まり状態にならない「安全性」は少し難しい話になりますが、型の進行定理と保存定理というものによって保証されます。証明はしませんが、それぞれ以下のような内容になります。

 これら2つの定理によって、正しく型付けされた項は最終的に値として評価でき、行き詰まり状態に陥らないということがわかります。