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

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

意味論とは、大雑把に言えば、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文はまだあります。

まず、与えられたものを見てみましょう。

// < - Returns true if a is less than b
public static boolean lessThan(int a, int b) { ... }

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

はじめの関数はそれほど複雑ではありません。

// > - Returns true if a is greater than b
public static boolean greaterThan(int a, int b) {
  return lessThan(b, a);
}

これは、$b<a$ があるときはいつでも、$a>b$ があることをすでに知っているため、うまくいきます。同様の理由でgreaterThanOrEqualToとlessThanOrEqualToの実装を書けます。

// >= - Returns true if a is greater than or equal to b
public static boolean greaterThanOrEqualTo(int a, int b) {
  return not(lessThan(a, b));
}
  
// <= - Returns true if a is less than or equal to b
public static boolean lessThanOrEqualTo(int a, int b) {
  return greaterThanOrEqualTo(b, a);
}
  
// ! - Returns the negation of b
public static boolean not(boolean b) {
  if (b)
    return false;
  else
    return true;
}

greaterThanOrEqualToの定義では、実質的にlessThanの結果を否定しています。したがって、$a\not <b$ のときは true を返し、$a<b$ のときは false を返します。しかし、$a\not <b$ のときは、$a\geq b$ がわかっているので、これは真を返さなければならない場合であり、真を返すのです。同様に、$a<b$ のとき、$ageb$ はありえないことが分かっているので、正しくfalseを返します。

これらの定義が与えられれば、equalToとnotEqualToを定義できます。

// == - Returns true if a equals b
public static boolean equalTo(int a, int b) {
  if (greaterThanOrEqualTo(a, b))
    return greaterThanOrEqualTo(b, a);
  else
    return false;
}
  
// != - Returns true if a does not equal b
public static boolean notEqualTo(int a, int b) {
  return not(equalTo(a, b));
}

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

ラムダ計算の組込み演算

以下は、完全なラムダ計算言語の文法です。

expr ::= "λ" id "." expr         (* abstraction, anonymous function definition *)
expr ::= expr expr               (* application, calling a function *)
expr ::= id                      (* variable use *)
expr ::= "(" expr ")"            (* grouping *)

また、省略形を作成できるようにするために、別の記法を紹介します。

definition ::= "let" id "=" expr

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

expr ::= "[" expr "]"

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

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

id ::= ? any printable, non-whitespace characters except ()[]=.;, "let", and "" ?

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

行のコメントには ";" を使う。

抽象化： 関数の定義

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

expr ::= "λ" id "." expr

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

ここまでのところでは、あまり何も定義できないようです。最初に思いつくのは、恒等式関数でしょう。

λx. x

つまり、この関数を指定したxに対して、xが返されます。 常に＆lambda;xを書く代わりに。 x 恒等関数を使用するたびに、省略形を作成できます

let identity = λx. x

次に、代わりに Identity を参照します。これは、構文的に重い＆lambda;x. xを参照するのと同じです。。

Javaでは、同じ定義は次のようになります。

 public static Function identity(Function x) {
   return x;
 }

ラムダ計算の値や型は関数だけなので、引数も戻り値も仮想的な「関数」型です。

適用： 関数呼出し

ルールを適用

expr ::= expr expr

は、関数を適用（または呼出す）できます。例えば、fが関数で、aがその引数であったとします。fをaに適用するには、両者を並べるだけでよい。

f a

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

f(a)
(f a)
((f) a)
((f) (a))
(f)a

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

f.apply(a)

というのは、「fをaに当てはめる」という意味になります。

β-リダクション

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

f a

次と同じになる

(λx. expr) a

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

expr [a/x]

先ほどの恒等式関数があれば、それを要素に適用できます。そこで

identity a

これと同じです。

(λx. x) a

これと同じです。

x [a/x]

となり、代入後は

a

また

identity identity

というのと同じです。

(λx. x) (λx. x)

これと同じです。

x [(λx. x)/x]

となり、代入後は

(λx. x)

であり、つまりは恒等式関数そのものです。

優先順位

左から右

複数の引数と字句のスコープ

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

λy. λx. x

これは、「任意のyが与えられたら、そのID関数を返す」と解釈すべきです。

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

λy. λx. y

この関数は、"任意の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: given n, returns a function that adds n to its argument
let create-adder = λn. (details left out for the moment)

create-adderが存在すると仮定すれば、足し算を定義するのは些細なことです。

let + = λn.λm. ((create-adder n) m)

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

読み方は、「＋」です。"任意のnが与えられたとき、任意のmが与えられたとき、n＋mを返す関数を返す "です。5と4が値として定義されていると仮定すると（この方法はすぐに紹介します）、"+"はそれらを足すために使うことができるのです。

((+ 5) 4)

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

(+ 5 4)

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

しかし、「＋」関数は具体的にどのようにして「n＋m」を返しているのでしょうか。本体はこうなっています。

((create-adder 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 A B

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

if cond A B

次のようになります。

A

そして、"cond "がfalseのときは

if cond A B

次のようになります。

B

ここまで来ると、trueはパラメータ t とパラメータ f の2つのパラメータを持ち、tを返す関数だと思えばいいのです。

let true = λt. λf. t

そして、falseは、パラメータ t とパラメータ f の2つのパラメータを持ち、fを返す関数と考えられます。

let false = λt. λf. f

そう考えると、ifを定義するのは簡単です。

let if = λcond. λA. λB. cond A B

ここでは、論理値自体（condという名前）がすべての手間のかかる作業を行っています。論理値はAとBの両方に渡されます。論理値がtrueの場合は、Aを返し、論理値がfalseの場合はBを返す必要があります。trueとfalseを慎重に定義すると、このようになります。

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

論理演算

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

not: 論理値に対するnot演算

let not = λb.
  if b
    false
    true

もうお気づきかもしれませんが、"if" は実は必要ありません。なぜなら、"if" をカットして、値を直接論理値に渡せばよいからです。

let not = λb. b false true

ifを使うのは、単に可読性を高めるためのスタイル上の問題です。

and: 2つのブール値の論理和 bが真ならcを返し、そうでなければ偽を返す、したがって、bとcがともに真のときのみ真を返す

let and = λb. λc.
  if b
    c
    false

or：論理和演算：bとcの両方が偽のときのみ偽を返す

let or = λb. λc.
  if b
    true
    c

xor：論理的排他的論理和演算：bとcが異なるとき真，それ以外は偽を返す。

let xor = λb. λc.
  if b
    (not c)
    c

bool-eq: 論理的な等値性: bとcが同じ値であれば真を返す。

let bool-eq = λb. λc.
  if b
    c
    (not 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))), ... となります。

let 0 = λs. λz. z
let 1 = λs. λz. s z

successor function: 与えられた数字にもう一回successorを適用します。

let succ = λn.
  λs. λz.
    s (n s z)

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

let is-zero? = λn. n (λx. false) true

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

addition：nとmの和を返す

let + = λn. λm. n succ m

[TODO: この長い形式も見たことがありますが、なぜこれが使われるのかはよくわかりません:] 。

let + = λs. λz. m s (n s z)

multiplication: nとmの積を返します。「自分にnを足す」操作を0にm回適用することによって行われます。

let * = λn. λm. m (+ n) 0

自然数の累乗： n を m 乗します。

let pow = λn. λm. m (* n) 1

リスト

引き算はもっと厄介なので，まずペアを定義する必要があります。

let pair = λfirst. λsecond. λbool. bool first second

ペアの1番目の要素を取り出す

let first = λpair. pair true

ペアの2番目の要素を取り出す

let second = λpair. pair false

cons, car, cdr: ペアをリストとして考える場合

let cons = pair
let car = first
let cdr = second

減算

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

let next-pair = λp. pair (succ (first p)) (first p)

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

適用回数        ペアの値        n で表したペアの値
-------------   -------------   ---------------------------
n =         0   (0, 0)          (n, n)
n =         1   (1, 0)          (n, n - 1)
n =         2   (2, 1)          (n, n - 1)
n =         3   (3, 2)          (n, n - 1)
n =         4   (4, 3)          (n, n - 1)

註:（n next-pair（pair 0 0））は、n> = 1の場合はペア（n、n --1）を生成し、n = 0の場合は（0、0）を生成します。 n> = 1の場合はn-1、n = 0の場合は0になるために、このペアの2番目の要素を取得する必要があります。 これがまさにpredecessorの実装方法です。

let pred = λn. second (n next-pair (pair 0 0))

subtraction: $n-m$ を返す; ただし、その値が負になる場合は、代わりに 0 が返される

let - = λn. λm. m pred n

関係演算と除算

減算ができるようになったので、数を比較することができるようになりました。

n は m より大きいか等しいか？

let >= = λn. λm. is-zero? (- m n)

n が m 以下か？

let <= = λn. λm. >= m n

n が m より小さいか？

let < = λn. λm. not (>= n m)

nがmより大きいか？

let > = λn. λm. not (>= m n)

equal: nとmは同じ数か？

let equal = λn. λm. and (>= n m) (>= m n)

not-equal: nとmは異なる数か？

let not-equal = λn. λm. not (equal n m)

div: 分子 n と分母 d が与えられたら、商を返す。

let / = λn. λd.
  (if (< n d)
     0          ; -- (n < d)
     (if (equal n d)
        1          ; -- (n == d)
        ; subtract d from n until the value is < d -- (n > d)
        (n
          [λn'.
            (if (< n' d)
               n'
               (- n' d))] n)))

mod: 分子nと分母dを与えて余りを返す。

let mod = λn. λd. (- n (* (/ n d) d))

Y-コンビネーター

不動点Yコンビネーター（コール・バイ・バリュー(call-by-value)），再帰性を実現するために

let fix = λf.
  [λx. f (λy. x x y)] [λx. f (λy. x x y)]

Y: fixの別名

let Y = fix

プリミティブで拡張されたラムダ計算機

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