プログラミング言語論1

プログラミング言語論
第13回
C言語のsubsetの意味の定義
（ while文の追加）および
ラムダ計算（演習付）
情報工学科木村昌臣
篠埜功
今後のスケジュール
12/17（水）第１３回ラムダ計算（導入）
12/24（水）第１４回
1/14（水）は月曜日の講義が行われるので無し。
期末試験は試験期間中に行う。日時、場所は未定。
練習問題
状態  = { (X, 10), (Y, 20), (Z, 30) } のとき、
 [ 40 / X ] はどういう状態か。
解答
状態  = { (X, 10), (Y, 20), (Z, 30) } のとき、
 [ 40 / X ] はどういう状態か。
X以外の値はそのままで、Xの値が40なので、
 [ 40 / X ] = { (X, 40), (Y, 20), (Z, 30) }
である。
文の定義
文を、代入文の並びで定義する。
<文> :: = <変数> = <式> ;
| <文> <文>
文の構文解析結果を以下で表す。
c ::= x = a;
| c c
c は文を表す。
x は変数を表す。
a は算術式を表す。
文の実行
状態のもとで文cを実行したら状態が’になる
ということを、
<c,  >  ’
と表す。
（例）状態 { (X, 10), (Y, 20), (Z, 30) }のもとで
文 Y = 40; を実行すると、状態は
{ (X, 10), (Y, 40), (Z, 30) }
になる。これを、
< Y = 40;, { (X, 10), (Y, 20), (Z, 30) } >
 < { (X, 10), (Y, 40), (Z, 30) } >
と書き表す。
文の実行に関する規則
代入文の場合
<a,  >  n
< x = a;,  >   [ n / x ]
文の並びの場合
<c1,  >  1 <c2, 1>  2
< c1 c2,  >  2
例１
状態  = { (X, 10), (Y, 20), (Z, 30) } において文Y=40; を
実行すると状態はどうなるか。
< 40,  >  40
< Y = 40;,  >   [ 40 / Y ]
< { (X, 10), (Y, 40), (Z, 30) } >
例２
状態  = { (X, 10), (Y, 20), (Z, 30) } において
文X = 3; Y=40; を実行すると状態はどうなるか。
< 3,  >  3
< X = 3;,  >   [ 3 / X ]
< 40,  >  40
< Y = 40;,  [ 3 / X ] >  ( [3 / X]) [ 40 / Y ]
< X = 3; Y = 40;  >  ( [3 / X]) [ 40 / Y ]
< { (X, 3), (Y, 40), (Z, 30) } >
練習問題
状態  = { (X, 10), (Y, 20), (Z, 30) }
において、文 X = Y + 2; Y = Y + 3 を実行したら
状態はどうなるか。規則を使って導出せよ。
解答
状態  = { (X, 10), (Y, 20), (Z, 30) }
において、文 X = Y + 2; Y = Y + 3 を実行した
ら状態はどうなるか。規則を使って導出せよ。
<Y, >  20
<2, >  2 <Y, [22/X]>  20 <3, >  3
< Y + 2;,  >  22
<Y + 3;,  [ 22 / X]>  23
<X = Y + 2; >   [ 22 / X ] <Y = Y + 3;  [ 22 / X ]>  ( [ 22 / X ]) [23 / Y]
< X = Y + 2; Y = Y + 3,  >  (  [ 22 / X ] ) [ 23 / Y ]
{ (X, 22), (Y, 23), (Z, 30) }
while文
文にwhile文を追加する。
<文> :: = <変数> = <式> ;
| <文> <文>
| while (<式>) { <文> }
構文解析結果は以下で表す。
c ::= x = a;
| c c
| while ( a ) { c }
c は文を表す。
x は変数を表す。
a は算術式を表す。
while文の意味
<a,  >  0
< while (a) { c },  >  
<a,  >  n <c,  >  1 < while (a) { c }, 1 >  2
if n 0
< while (a) { c },  >  2
例３
状態  = { (X, 10), (Y, 20), (Z, 30) } において
文while ( Y ) { Y = Y – 20; } を実行すると状態はどうなる
か。
<Y,  >  20 <20,  >  20
< Y,  [0/Y] >  0
<Y-20,  >  0
<Y;,  >  20 <Y=Y-20;, >   [0/Y] <while(Y){Y=Y-20;}, [0/Y]>  [0/Y]
< while (Y) {Y = Y - 20;} ,  >   [0 / Y]
< { (X, 10), (Y, 0), (Z, 30) } >
練習問題
状態  = { (X, 10), (Y, 40), (Z, 30) } (Yの初期値が４０)
において、文 while ( Y ) { Y = Y – 20; } を実行したら
状態はどうなるか。規則を使って導出せよ。
解答
状態  = { (X, 10), (Y, 40), (Z, 30) } において
文while ( Y ) { Y = Y – 20; } を実行すると状態はどうなるか。
<Y,  >  40 <20,  >  20
<Y-20,  >  20
…略（例３と同様）
<Y,> 20 <Y=Y-20;, > [20/Y] <while(Y){Y=Y-20;},[20/Y]> [20/Y][0/Y]
< while (Y) {Y = Y - 20;} ,  >   [20/Y] [0/Y]
< { (X, 10), (Y, 20), (Z, 30) } >
（例３の初期状態と同じ）
< { (X, 10), (Y, 0), (Z, 30) } >
今日のトピック：ラムダ計算
ラムダ計算とは：
プログラミング言語の核となる部分を取り出した言語
計算可能なプログラムをすべて表現可能。
ラムダ式
ラムダ式の定義
<ラムダ式> ::= <定数>
| <変数>
| (<変数> . <ラムダ式>)
| (<ラムダ式> <ラムダ式>)
<定数> ::= 0 | 1 | 2 | 3 | …
<変数> ::= x | y | z | w | …
ラムダ式
ラムダ式の構文木を以下のように定義する。
M ::= c
|x
| (x .M)
| (M M)
定数（0, 1, 2, 3,等）
変数（x, y, z, w, 等）
ラムダ抽象
関数適用
ラムダ式
ラムダ式を表記する場合の約束事項
1. 関数適用は左結合する。
2. ラムダ抽象x .MにおけるMはできるだけ
大きくとる。
3. 括弧を省略した場合、1, 2の約束に従う。
例 x y z は、(x y) zを表す。
例 x. y. z. x y z は、 x. (y. (z. ((x y) z))) を表す。
ラムダ式
計算の本質を追究する過程で考えられた言語
ラムダ記法は直感的には関数の表記法。
g(x)=x+1
で定義される関数g : Z  Z を、
g=xZ.x+1
のように表記する。Zが明らかな場合省略して
g =  x. x + 1
のように書く。
型無しラムダ計算
通常は関数の引数は型があったものが与えら
れる必要があるが、型を無視して形式的な
式変形（変換、次ページで説明）を行うの
が型無しラムダ計算。
変換
ラムダ式 M, N, P, 変数xについて、 変換を
以下のように再帰的に定義する。
• (x. M) N  M [N / x]
• M  N ならば、
(x. M)  (x. N)
MP  NP
PM  PN
M [N / x]はラムダ式M中のxをNで置き換えた
ラムダ式を表す。ただし、束縛変数が自由
変数とかぶらないように、束縛変数の名前
の付け替えを行う。
自由変数
ラムダ式 Mの自由変数の集合FV(M)を以下
のように定義する。
FV( c ) = { }
FV ( x ) = { x }
FV ( x. M ) = FV (M) \ { x } （\ は集合の差を
とる演算を表すものとする。）
FV (M1 M2) = FV (M1)  FV (M2)
変換列
ラムダ式M1に変換を有限回（0回以上）繰り
返してラムダ式Mnが得られるとき、
M1  M2  …  Mn
を変換列という。これはM1 * Mn
と表せる。
また、M  N かつ N  M のとき、
M  N と書く。
例
ラムダ式 (x. y. x y) z w に対して、以下の
は以下の変換列が存在する。
(x. y. x y) z w
 (y. z y) w
 zw
練習問題
ラムダ式 (x. y. x y) (z. z) w は、変換列
によってwに変換できるが、その過程を示
せ。
解答
黒板で説明。

Download Report