# 204 PTT (in Japanese)

第 204 回 PTT のお知らせ

日時: 1995年1月26日 (木) 18:30 から

場所: 東大工学部6号館1階大会議室(103号室内線 6948) (19時を過ぎると正面の玄関が閉まってしまうので, 遅れて来た人は玄関にある内線電話で大会議室にいる人を呼び出して下さい)

  安 |            |        |  |       |   |
  田 |            +--------+  +-------+   -
  講 |                                       正門
  堂 |            +--------+  +-------+   -
  ---+            | 法文   |  | 工学部|   |
                  |        |  | 列品舘|   |
                  +--------+  +-------+   |
                                          |                             
  ---------+  +-------+             +----+|                             
  工学部   |  |工学部 |             |工11||
  2号館    |  |6号館  =入口         |    ||                             
           |  |       |             |    ||                             
  ---------+  +-------+             |    ||

話者：下國治 (東大)

題目：あの世とこの世は地続きだ --- 部分計算への抽象解釈の応用

概要：


  部分計算の為に展開(unfolding)を行なうことを考える. 部分計算の分類のう
  ち, 展開時に判明する値を利用する部分計算を Online 部分計算という.
  例えば, 
  
	f a =	g a,		if a = 0
		h a,		otherwise

	g x =	true,		if x != 0
		false,		otherwise

  であるとき, g a に対して, [a -> 0] という環境を渡し, g 0 に対する特殊
  化を行なう. すなわち, 

	f a =	true,		if (a = 0 && a != 0)
		false,		if (a = 0 && !( a != 0))
		h a,		otherwise	

	    =	false,		if a = 0
		h a,		otherwise	

  となる. 逆に展開時に判明する値を利用しなければ, 楽観的な展開の戦略を用
  いれば不必要になる式を(組合せ的増加で)生成し, 悲観的な展開の戦略を用い
  れば十分に展開をすることなく部分計算が打ち切られてしまう.

  このように展開時に判明する値を利用したいのであるが, 現在の大部
  分の部分計算系は例のように代入された値と 等しいか等しくないか のみ判断
  が可能である. また, 例では否定演算子(!)を使用したが, 否定の導入も非常
  に難しく, 二村の一般部分計算(GPC)のみに導入されている. 

  プログラムの意味を求める解析は, 広域解析, 型推論などが行なわれているが,
  今回, 抽象解釈(Abstract Interpretation)を取りあげる. 抽象解釈は関数型
  言語や論理型言語の翻訳時/実行時の実行順(評価順)計画に用いられる応用が
  良く知られている. 

  本発表では部分計算の展開制御に抽象解釈を応用することを示す. 
  プログラムを「この世=標準解釈(Standard Interpretation)」で解釈し展開す
  る前に「あの世=抽象解釈(Abstract Interpretation)」で解釈し, その展開が
  無駄になるか否かを判断してから「この世」で展開する手法を述べる. 特に, 
  プログラムの字面を操作せねばならないので, 意味の世界と構文の世界との対
  応を取り得る機構の導入と,「あの世」に対する解釈の与え方が複数あっても, 
  それらがプログラムの字面にのどの部分から出てきたかを知ることにより, 複
  数の「あの世」の情報を統合できることを示す.

食事:

第 204 回 PTTメモ

日時: 1995年1月25日 18:30 - 20:30

場所: 東京大学工学部6号館大会議室

題目: あの世とこの世は地続きだ --- 抽象解釈の部分計算への応用

話者: 下國治

出席者: 並木美太郎, 早川栄一(以上農工大), 伊知地宏, 左口泰之(以上富士ゼロックス), 田中淳裕(NEC), 中山泰一, 多田好克, 中村嘉志(以上電通大), 石畑清(明大), 佐々木崇郎, 大駒誠一, 金子裕之(以上慶大), 岩崎英哉, 田中哲郎, 小川宏高, 下國治(以上東大), 和田英一 nil

共立出版社の雑誌 bit における多田先生の広告にも関わらず, 論文シーズンの為か出席者が少なかった. 新学期からはより多くの参加者が参加されることが期待される.

質疑応答:

部分計算の概略(特にOffline 部分計算), および抽象解釈の概略をのべ,
Offline 部分計算の拡張として, 解析の領域を rich にした抽象解釈を利用する
ことにより Online 部分計算の特徴である条件分岐の then 部, else 部への述
語部分から得られる制約の伝播を実現する案を述べた. 抽象解釈の領域は, 具象
領域のある側面を抽象化しているものであり, 様々な性質を一つの抽象領域で抽
象することは抽象領域の増大を招き, 必要な計算量を著しく増大させるので, 逆
に, 独立な抽象解釈の結果を統合できる手法の案を述べた.

部分計算及び抽象解釈, プログラム意味論に馴染みのない聴衆があまた来ること
を期待して, 前半に力を入れたが, 蓋を空けて見ればワケシリの人ばかりが聴衆
であった為, 後半にもっと時間を割くべきであった.