プログラミング言語/意味論
プログラミング言語の意味論

意味論とは、大雑把に言えば、ab+c、"ab "+"c"、mult(5,4)といった記号群に与えられた意味です。
プログラミング言語の意味論

例えば、5と4を足すという構文を表現するには、こう言えます。5と4の間に "+"記号を入れれば、"5 + 4 "となります。しかし、「5+4」の意味論も定義しておかなければなりません。算術的な意味論で言えば、5+4は9の表現/等価(=)です。
プログラミング言語の意味論

コンピュータサイエンスでは、プログラミング言語の作者は、'+'の定義を使うことも、新しく作ることも「可能」です。例えば、「+」は算術的な引き算(-)と定義できます。しかし、より一般的には、複素数や、「123a」、「aFsd」、「./etc」のような文字列(記号の並び)に対する関数(ある値を取り込んで別の値を出力します)として定義されることが多いようです。
プログラミング言語の意味論

意味論は、単なる理論や哲学ではありません。プログラミング言語の特性の多くは、厳密な解析によってのみ決定されます。例えば、"このプログラミング言語は安全である "というような発言をしたい。しかし、あるプログラミング言語が安全であることを証明するには、その言語の文法についての議論だけでは不十分です。安全性の正式な証明がなければ、システムは、多くの別々の相互作用する関心事がもたらす予期せぬ結果に対して脆弱になりかねないのです。このような証明を行う一つの方法は、数学的モデルを用いることです。
プログラミング言語の意味論

あるプログラミング言語のセマンティクスが与えられれば、他のプログラミング言語をそのベース言語の観点から記述するオプションがあります。つまり、あるプログラミング言語のセマンティクスを指定する1つの方法は、それを他の言語と関連付けることです。しかし、この場合、元のベースとなる言語を何にするかというブートストラップ問題が発生します。プログラミング言語の研究者は、この問題を、元々は論理学のために発明された数学モデルでありながら、計算機への劇的な応用を可能にするものを使うことで解決した。ラムダ計算です。
プログラミング言語の意味論

ラムダ計算とは、1920年代から30年代にかけてアロンゾ・チャーチやクリーネらによって発明されたもので、チューリング完全言語を記述する上で最も単純なものの1つです。関数という単一の値を持ち、関数の定義と関数の呼出しという2つの操作しか持たない言語です。さらに単純化すると、関数は1つのパラメータしか持つことができません。
プログラミング言語の意味論

ここでは、関数を引数として受け取り、他の関数を値として返す関数について考えてみましょう。非常に抽象的な概念ですが、これから説明するように、巧妙な定義によって、私たちが普段使っているプログラミング言語に近い形で言語を構築できます。例えば、これから紹介する最初のトリックの1つは、各関数が1つの引数しかとれないにもかかわらず、複数の引数をとることができるという同じ結果を得るための方法です。
プログラミング言語の意味論

ラムダ計算を扱う前に、より標準的なプログラミング言語でのパズルから始めましょう。Javaには二項演算子"<"しかなく、">"、">="、"<="演算子を与える関数を定義する必要があったとします。また、単項演算子もありませんが、if文はまだあります。
プログラミング言語の意味論

まず、与えられたものを見てみましょう。
プログラミング言語の意味論

私たちの課題はgreaterThan、greaterThanOrEqualTo、lessThanOrEqualToを定義することです。このパズルでは、lessThanの呼出しとif文の使用、そしてブール値の返り値しかできないことを忘れないでください。この先を読む前に、どのようなことができるかを考えてみてください。
プログラミング言語の意味論

はじめの関数はそれほど複雑ではありません。
プログラミング言語の意味論

これは、 b < a {\displaystyle b<a} があるときはいつでも、 a > b {\displaystyle a>b} があることをすでに知っているため、うまくいきます。同様の理由でgreaterThanOrEqualToとlessThanOrEqualToの実装を書けます。
プログラミング言語の意味論

greaterThanOrEqualToの定義では、実質的にlessThanの結果を否定しています。したがって、 a ≮ b {\displaystyle a\not <b} のときは true を返し、 a < b {\displaystyle a<b} のときは false を返します。しかし、 a ≮ b {\displaystyle a\not <b} のときは、 a ≥ b {\displaystyle a\geq b} がわかっているので、これは真を返さなければならない場合であり、真を返すのです。同様に、 a < b {\displaystyle a<b} のとき、 a g e b {\displaystyle ageb} はありえないことが分かっているので、正しくfalseを返します。
プログラミング言語の意味論

これらの定義が与えられれば、equalToとnotEqualToを定義できます。
プログラミング言語の意味論

私たちは今、ラムダ計算の演算を構築するための方法を考え始めています。<と==だけでなく、数値、ブーリアン、数値に対するすべての演算、すべての関係演算、リンクリスト、if式、ループ構成、さらには出力やその他の副作用のモデルも発明する必要があります。
プログラミング言語の意味論

以下は、完全なラムダ計算言語の文法です。
プログラミング言語の意味論

また、省略形を作成できるようにするために、別の記法を紹介します。
プログラミング言語の意味論

このような「let」が行われた後、識別子は右辺の式に展開されるはずです。また、別の形の括弧を入れるが、これはすでに定義されている中括弧と何ら変わりはありません。
プログラミング言語の意味論

この言語には句読点( punctuation )があまりないため、多くの括弧が使用されます。そこで、2つの異なるタイプの括弧を許可することで、可読性を向上させます(グループの開始と終了を視覚的に一致させることができるため)。
プログラミング言語の意味論

最後に、識別子はどのような文字の並びでも構いませんが、それが既に他の何かを意味するトークンでないことが条件です。
プログラミング言語の意味論

つまり、一般的なプログラミング言語と異なり、ラムダ計算では、「i」「x」「y1」「reminder」「theReturnValue」がすべて識別子であるように、「0」「+」「%」「15」などが有効な識別子となるのです。
プログラミング言語の意味論

行のコメントには ";" を使う。
プログラミング言語の意味論

ラムダ計算の規則の指定を、仮想的なJavaのような言語との比較から始めることにします。抽象化ルールです。
プログラミング言語の意味論

を使うと、新しい関数を作られます。ラムダ「λ」記号は、新しい関数が定義されることを示し、それに続く識別子は、そのパラメータの名前です。ドット". "の後に続く式は、パラメータとスコープ内の他の変数を参照することができる式です。なお、ラムダ計算では、関数には名前がありません。もし名前を付けたい場合は、「let」形式で省略形を作るだけにしておく必要があります。
プログラミング言語の意味論

ここまでのところでは、あまり何も定義できないようです。最初に思いつくのは、恒等式関数でしょう。
プログラミング言語の意味論

つまり、この関数を指定したxに対して、xが返されます。 常に&lambda;xを書く代わりに。 x 恒等関数を使用するたびに、省略形を作成できます
プログラミング言語の意味論

次に、代わりに Identity を参照します。これは、構文的に重い&lambda;x. xを参照するのと同じです。。
プログラミング言語の意味論

Javaでは、同じ定義は次のようになります。
プログラミング言語の意味論

ラムダ計算の値や型は関数だけなので、引数も戻り値も仮想的な「関数」型です。
プログラミング言語の意味論

ルールを適用
プログラミング言語の意味論

は、関数を適用(または呼出す)できます。例えば、fが関数で、aがその引数であったとします。fをaに適用するには、両者を並べるだけでよい。
プログラミング言語の意味論

括弧はグループ化を提供するだけであり、fとaはすでに終端要素なので、以下のものはすべて上記と等価です。
プログラミング言語の意味論

仮にfがJavaのような仮想の言語におけるFunctionのインスタンスであったとします。関数適用はこのように書くことができるでしょう。
プログラミング言語の意味論

というのは、「fをaに当てはめる」という意味になります。
プログラミング言語の意味論

実際の応用のセマンティクスは置換規則(β-リダクション(β-reduction)ルールとも呼ばれます)です。f がラムダ関数で a が何らかの値であり、それらが並置されたとき、適用が行われます。例えば f のパラメータが x という名前で、何らかの式 expr が x を使っていたとします。そのとき
プログラミング言語の意味論

次と同じになる
プログラミング言語の意味論

アプリケーションでは、xの出現箇所をすべてaに置換えられます。この置換を次のように書きます。
プログラミング言語の意味論

先ほどの恒等式関数があれば、それを要素に適用できます。そこで
プログラミング言語の意味論

これと同じです。
プログラミング言語の意味論

これと同じです。
プログラミング言語の意味論

となり、代入後は
プログラミング言語の意味論

また
プログラミング言語の意味論

というのと同じです。
プログラミング言語の意味論

これと同じです。
プログラミング言語の意味論

となり、代入後は
プログラミング言語の意味論

であり、つまりは恒等式関数そのものです。
プログラミング言語の意味論

左から右
プログラミング言語の意味論

現在のところ、ラムダ計算ができることは、恒等関数を作って自分自身に適用すること以上のことはできないように思えます。この言語をさらに使いこなすには、抽象化操作をそれ自体が真の操作であると考えるようにする必要があります。例えば、恒等関数を定義する代わりに、恒等関数を作る関数を定義してみましょう。
プログラミング言語の意味論

これは、「任意のyが与えられたら、そのID関数を返す」と解釈すべきです。
プログラミング言語の意味論

これまでのラムダ関数本体では、パラメータを返すだけでした。上の例では、もう一つの選択肢として、自分が定義されている関数のパラメータを返すというものがあることがわかります。例えば、次のような場合はどうだろうか?
プログラミング言語の意味論

この関数は、"任意のyが与えられると、任意のxが与えられると、常にyを返す関数を返す "と解釈すべきです。つまり、数学でグラフ上の水平線として表現される定数関数を作るのです。(グラフ上の恒等関数は、代わりに原点を通る45度の角度の線となります)。このセクションでは、この新しいオプションによって、どのように豊かな概念を表現することができるかを紹介します。特に、複数の引数を取る関数のシミュレーションを行う方法を紹介します。
プログラミング言語の意味論

引数を1つしか取らない関数から、複数の引数を取る関数をシミュレートする方法として、すべての引数を1つの単位にまとめ(複素数が2つの浮動小数点数を含むように)、その単位を渡すという考え方があります。このような手法は、タプルの手法と言えます。実際に複数の値の集まりである引数を渡すことができる限り、最初にそれらの複数の値を渡すことと何ら変わりはないのです。
プログラミング言語の意味論

タプル技法は使えますが、ラムダ計算にはタプル型がありません。唯一の型は、単一の引数を受け取る関数です。しかし、上のxとyを使う2つの関数を思い出してください。λy関数がλx関数を生成するので、λx関数はxとyのどちらかを使えます。
プログラミング言語の意味論

この問題を考える一つの方法は、特定の例に注目することです。つまり、引数a, b, cを受け取り、それらの値を含む何らかの計算を行う新しい関数を定義したいとします。この関数は機械と考えられます。ラムダ計算では、この機械は1つの値しか取り込めないという制限があります。しかし、何を返すかについては厳密な制限はありません。つまり、aしか取り込めない機械は、bやcを知らないので、目的の計算をすることができないです、とまず考えます。しかし、aを知っているので、aを知る新しい機械を返せます。その機械もパラメータを受け取るので、それをbとします。したがって、今あなたはaとbを知っているがcを知っていない機械を手に入れました。
プログラミング言語の意味論

この概念をわかりやすくするために、足し算ができる機械を作りたいとします。つまり、「任意のnとmが与えられたら、n+mの和を返す」というような関数です。まず、もっと原始的な関数であるcreate-adderを作れば、そのような効果を得られます。ここではまだcreate-adderを実装しませんが、以下のような仕様で存在すると仮定します。
プログラミング言語の意味論

create-adderが存在すると仮定すれば、足し算を定義するのは些細なことです。
プログラミング言語の意味論

まず、「+」に惑わされないでください。これは、他の識別子と同じように単なる記号です。この関数の略称を「+」ではなく、「プラス」や「アド」とすることもできるのです。では、「+」機能そのものは何なのか。
プログラミング言語の意味論

読み方は、「+」です。"任意のnが与えられたとき、任意のmが与えられたとき、n+mを返す関数を返す "です。5と4が値として定義されていると仮定すると(この方法はすぐに紹介します)、"+"はそれらを足すために使うことができるのです。
プログラミング言語の意味論

ここで、まず「+」を5に適用し、その結果を4に適用します。「+」は上位では2つの引数を取ると考えられるので、カッコをいくつか外すと分かりやすくなります。
プログラミング言語の意味論

を5に適用し、その結果を4に適用するという意味に変わりはありません(この場合、括弧をすべて削除しても同じ意味になります)。このような関数の呼び方は、前置記法とも同じです。
プログラミング言語の意味論

しかし、「+」関数は具体的にどのようにして「n+m」を返しているのでしょうか。本体はこうなっています。
プログラミング言語の意味論

ここで、create-adderにはnが渡されます。定義によれば、任意の数が与えられると、nとその数の和を返す関数が返されます。そして、その関数をすぐにmに適用して、n + mの和を得ます。
プログラミング言語の意味論

このトリックはカリー化( Currying )と呼ばれ、言語自体は技術的に単一引数の関数しか許さないにもかかわらず、複数引数を達成する方法です。
プログラミング言語の意味論

関数が1つの引数しか取らない言語に複数の引数を追加する方法がわかったので、他の拡張を検討できます。より多くのプログラミング構造を作るためには、制御フローを記述するだけでなく、新しい値も作る必要があります。
プログラミング言語の意味論

今までに作った値は、(1)恒等式関数、(2)恒等式関数を返す関数、(3)定数関数を返す関数だけです。
プログラミング言語の意味論

最初に作成する値は論理値のtrueとfalseです。まずtrueを恒等式と定義し、falseを恒等式を返す関数と定義してもよいのですが、それではこれらの定義を有用なものにするのは難しいでしょう。
プログラミング言語の意味論

そうではなく、trueとfalseを定義する前に、仮にtrueとfalseがあったとして、それを使って何をしたいのか?
プログラミング言語の意味論

望ましい性質の1つは、何らかの形でifを実行できることです。ifは、論理値、"then"値、"else"値の3つの引数を取る関数と考えられます。
プログラミング言語の意味論

ifはキーワードではなく、単なるシンボルであることに注意してください。"cond" が真であるとき、次のように定義したい。
プログラミング言語の意味論

次のようになります。
プログラミング言語の意味論

そして、"cond "がfalseのときは
プログラミング言語の意味論

次のようになります。
プログラミング言語の意味論

ここまで来ると、trueはパラメータ t とパラメータ f の2つのパラメータを持ち、tを返す関数だと思えばいいのです。
プログラミング言語の意味論

そして、falseは、パラメータ t とパラメータ f の2つのパラメータを持ち、fを返す関数と考えられます。
プログラミング言語の意味論

そう考えると、ifを定義するのは簡単です。
プログラミング言語の意味論

ここでは、論理値自体(condという名前)がすべての手間のかかる作業を行っています。論理値はAとBの両方に渡されます。論理値がtrueの場合は、Aを返し、論理値がfalseの場合はBを返す必要があります。trueとfalseを慎重に定義すると、このようになります。
プログラミング言語の意味論

[TODO: 要修正...とりあえず、thenとelseの値が両方評価されないように、何らかの形で遅延評価(lazy evaluation)を想定すべきです(無限ループを引き起こす可能性があります)]
プログラミング言語の意味論

真と偽の適切な定義ができたので、他の論理演算も簡単に定義できるようになりました。これは、以前Javaで行ったlessThanや他の関係する関数の演習を思い起こさせます。
プログラミング言語の意味論

not: 論理値に対するnot演算
プログラミング言語の意味論

もうお気づきかもしれませんが、"if" は実は必要ありません。なぜなら、"if" をカットして、値を直接論理値に渡せばよいからです。
プログラミング言語の意味論

ifを使うのは、単に可読性を高めるためのスタイル上の問題です。
プログラミング言語の意味論

and: 2つのブール値の論理和 bが真ならcを返し、そうでなければ偽を返す、したがって、bとcがともに真のときのみ真を返す
プログラミング言語の意味論

or:論理和演算:bとcの両方が偽のときのみ偽を返す
プログラミング言語の意味論

xor:論理的排他的論理和演算:bとcが異なるとき真,それ以外は偽を返す。
プログラミング言語の意味論

bool-eq: 論理的な等値性: bとcが同じ値であれば真を返す。
プログラミング言語の意味論

註:beq は not (xor b c) とも書けます。
プログラミング言語の意味論

チャーチ数--すべてのn>=0の場合:n番目のチャーチ数は「ゼロ」値zを取り込み、そのゼロ値に対して与えられた「後継」関数sをn回適用します。代数学的に言えば、0=z(すなわち、zにsを適用しないです)、1 = s(z), 2 = s(s(z)), 3 = s(s(s(z))), ... となります。
プログラミング言語の意味論

successor function: 与えられた数字にもう一回successorを適用します。
プログラミング言語の意味論

is-zero?:渡された数字がゼロに等しい場合に真を返します。これは、ゼロ関数を「真」、後継関数を常に「偽」を返す関数にすることで実現されています。したがって、trueはsuccessorが0回適用されたときのみ結果となります。
プログラミング言語の意味論

カリー化を使ったかわいらしいバージョンとしては、 { n (and false) true } がありますが、こちらの方がわかりやすいかもしれません。
プログラミング言語の意味論

addition:nとmの和を返す
プログラミング言語の意味論

[TODO: この長い形式も見たことがありますが、なぜこれが使われるのかはよくわかりません:] 。
プログラミング言語の意味論

multiplication: nとmの積を返します。「自分にnを足す」操作を0にm回適用することによって行われます。
プログラミング言語の意味論

自然数の累乗: n を m 乗します。
プログラミング言語の意味論

引き算はもっと厄介なので,まずペアを定義する必要があります。
プログラミング言語の意味論

ペアの1番目の要素を取り出す
プログラミング言語の意味論

ペアの2番目の要素を取り出す
プログラミング言語の意味論

cons, car, cdr: ペアをリストとして考える場合
プログラミング言語の意味論

さて、減算の話に戻りましょう。重要なのは、数の組 (a, b) を受け取って (a+1, a) を返す操作から始めることです。
プログラミング言語の意味論

ここで、(0, 0)を0として、next-pairをsuccessor 関数としてスタートすると、successor 関数をn回適用すると、次のようになることに注意してください。
プログラミング言語の意味論

註:(n next-pair(pair 0 0))は、n> = 1の場合はペア(n、n --1)を生成し、n = 0の場合は(0、0)を生成します。 n> = 1の場合はn-1、n = 0の場合は0になるために、このペアの2番目の要素を取得する必要があります。 これがまさにpredecessorの実装方法です。
プログラミング言語の意味論

subtraction: n − m {\displaystyle n-m} を返す; ただし、その値が負になる場合は、代わりに 0 が返される
プログラミング言語の意味論

減算ができるようになったので、数を比較することができるようになりました。
プログラミング言語の意味論

n は m より大きいか等しいか?
プログラミング言語の意味論

n が m 以下か?
プログラミング言語の意味論

n が m より小さいか?
プログラミング言語の意味論

nがmより大きいか?
プログラミング言語の意味論

equal: nとmは同じ数か?
プログラミング言語の意味論

not-equal: nとmは異なる数か?
プログラミング言語の意味論

div: 分子 n と分母 d が与えられたら、商を返す。
プログラミング言語の意味論

mod: 分子nと分母dを与えて余りを返す。
プログラミング言語の意味論

不動点Yコンビネーター(コール・バイ・バリュー(call-by-value)),再帰性を実現するために
プログラミング言語の意味論

Y: fixの別名
プログラミング言語の意味論

[TODO: この拡張について議論します。ラムダ計算を拡張して、プログラミング言語のモデルを作るのが一般的です。このモデルは、Javaが安全な言語であることを証明するために使われました(理論的には、このモデルは実装を考慮していません。]