53ningen.com

@gomi_ningen's Website

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

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

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

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

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

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

一般的なプログ...

Read More

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

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

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

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

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

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

Read More

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

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

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

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

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

項 t ::= true | false | if t then t else t | 0 | succ t | pred t | iszero t

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

[帰納的な項の定義] 項の集合とは以下の条件を満たす最小の集合 T である
(1) {...
Read More

Copyright © 53ningen.com