この本の目的 ・ semantics ( 意味論 ) で使われる考え方 や method ( 方法 ) の記述すること ・ これら (↑) の考え方や method をわか りやすく解説すること ( アプリケーショ ン作ってみるよ ) ・ 様々な method の関係性を研究するこ と Specify.

Slides:



Advertisements
Similar presentations
プログラミング言語論 プログラミング言語の構 文 水野嘉明. 目次 1. プログラミング言語の構文 2. BNF 3. 文脈自由文法 4. 構文図式 2.
Advertisements

1 線形代数学. 2 履修にあたって 電子情報システム学科 必修 2005 年度1セメスタ開講 担当 草苅良至 (電子情報システム学科) 教官室: G I 511 内線: 2095 質問等は上記のいずれかに行なうこと。 注意計算用のノートを準備すること。
プログラミング言語論 第3回 BNF 記法について(演習付き) 篠埜 功. 構文の記述 プログラミング言語の構文はどのように定式化できるか? 例1 : for ループの中に for ループが書ける。 for (i=0; i
0章 数学基礎.
和田俊和 資料保存場所 /2/26 文法と言語 ー正規表現とオートマトンー 和田俊和 資料保存場所
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
第1回 確率変数、確率分布 確率・統計Ⅰ ここです! 確率変数と確率分布 確率変数の同時分布、独立性 確率変数の平均 確率変数の分散
第3回 論理式と論理代数 本講義のホームページ:
プログラミング基礎I(再) 山元進.
コンパイラ 2011年10月17日
プログラミング言語としてのR 情報知能学科 白井 英俊.
数値計算及び実習 第3回 プログラミングの基礎(1).
アルゴリズムとデータ構造1 2007年6月12日
プログラミング基礎I(再) 山元進.
情報とコンピュータ 静岡大学工学部 安藤和敏
プログラミング言語論 第6回 型 情報工学科 篠埜 功.
プログラミング言語論 第4回 式の構文、式の評価
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
Natural Semantics 実行過程の、最初と最後の状態(state)の関係を考える。
Semantics with Applications
構造体.
条件式 (Conditional Expressions)
模擬国内予選2014 Problem C 壊れた暗号生成器
言語処理系(5) 金子敬一.
コンパイラ 2012年10月15日
10.通信路符号化手法2 (誤り検出と誤り訂正符号)
電気回路Ⅱ 演習 特別編(数学) 三角関数 オイラーの公式 微分積分 微分方程式 付録 三角関数関連の公式
ML 演習 第 7 回 新井淳也、中村宇佑、前田俊行 2011/05/31.
シミュレーション演習 G. 総合演習 (Mathematica演習) システム創成情報工学科
ディジタル回路 3. 組み合わせ回路 五島 正裕 2018/11/28.
PROGRAMMING IN HASKELL
プログラミング言語論プログラミング言語論 プログラムの意味論 水野嘉明
プログラミング言語論 第3回 BNF記法について(演習付き)
第二回 VB講座 電卓を作ろう.
プログラミング 4 記憶の割り付け.
第7回 プログラミングⅡ 第7回
逐次プログラムの正当性(2) 帰納的アサーション法(フロイド法)
 型推論1(単相型) 2007.
Structural operational semantics
プログラミング言語論 第9回 情報工学科 木村昌臣 篠埜 功.
コンパイラ 2011年10月20日
C言語 はじめに 2016年 吉田研究室.
JavaScriptを含んだHTML文書に対する データフロー解析を用いた構文検証手法の提案
第1章 いよいよプログラミング!! ~文章の表示 printf~
文法と言語 ー文脈自由文法とLR構文解析ー
オブジェクト指向言語論 第三回 知能情報学部 新田直也.
プログラミング入門2 第6回 関数 情報工学科 篠埜 功.
5.チューリングマシンと計算.
プログラミング入門 電卓を作ろう・パートI!!.
アルゴリズムと数式の表現 コンピュータの推論
PROGRAMMING IN HASKELL
プログラミング言語論 第10回 情報工学科 篠埜 功.
4.プッシュダウンオートマトンと 文脈自由文法の等価性
情報処理Ⅱ 第7回 2004年11月16日(火).
情報処理Ⅱ 2005年10月28日(金).
PROGRAMMING IN HASKELL
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
コンパイラ 2012年10月11日
情報とコンピュータ 静岡大学工学部 安藤和敏
プログラミング入門2 第6回 関数 情報工学科 篠埜 功.
PROGRAMMING IN HASKELL
第7章 そろそろ int 以外も使ってみよう! ~データ型 double , bool~
オブジェクト指向言語論 第三回 知能情報学部 新田直也.
計算技術研究会 第5回 C言語勉強会 関数(function)を使う
情報処理Ⅱ 第3回 2004年10月19日(火).
情報処理Ⅱ 2006年10月20日(金).
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
プログラミング 3 ポインタ(1).
計算機プログラミングI 第2回 2002年10月17日(木) 履習登録 複習 ライブラリの利用 (2.6-7) 式・値・代入 (2.6-8)
Presentation transcript:

この本の目的 ・ semantics ( 意味論 ) で使われる考え方 や method ( 方法 ) の記述すること ・ これら (↑) の考え方や method をわか りやすく解説すること ( アプリケーショ ン作ってみるよ ) ・ 様々な method の関係性を研究するこ と Specify : 詳しく記述する illustrate : わかりやすく説明する application : アプリケーション, 適用

ちょっと注意事項 ・ semantics は詳しく、明確に、厳格に 記述する必要が有る ・ 記号は大体、普段数学で使うのと同じ ものです ※ syntax と semantics を明確に区別して 読み進めましょう ( 次のスライドからあ るよ ) Represent : 表す implementation : 実装, ( たまに、実行 ) analysis : 解析

Syntax と Semantics Syntax : grammatical structure( 構文, 文法 ) parser に書く内容のこと Semantics : the meaning ( 意味 ) 意味とはなんぞや? → 次のページ Syntax analysis : 構文解析

Semantics の3つの意味 ・ Operational semantics : どう計算する か ・ Denotational semantics : どんな結果が出るか ・ Axiomatic semantics : 実行するのに必要な条件は何か Execute : 実行する Construct : 構文 (syntax に従って書かれたもの ) Effect : 影響, エフェクト ( 実行してくと、それぞれお互いに影響し合ってく感じ) Statement : 命令文 Sequence : 並び

例 z := x; x := y; y := z; (x と y の中身を入れ替えるプログラムで す ) Assign : 与える, 譲渡する, 代入する

Operational semantics z:=x; x:=y; y:=z; をどうやって計算するか → 個々の命令文を、左から右に一つずつ 実行していく ( := は代入を表す ) A variable followed by ‘:=‘ 〜 : ( 大抵 ) 命令文の先頭の文字のこと z:=x; なら z 長くてよくわかんないんだよ。。。

Structual operational semantics ・ プログラムをどうやって実行するかを抽象的 に表す。 (small-step semantics) ・ レジスタとかアーキテクチャとかを考えてな いあたりが抽象的 ・ これを図で表したものを derivation sequence という (P3 上の表 ) Abstraction : 抽象 abstract : 抽象的 derivation : 導出 Derivation sequence : 訳せない。。。

Natural semantics ・ プログラムによって、 state ( 環境 ) がどう変 化していくかを記述している、らしい ・ どうして state がそんな変化をするかはあま りきにしていない (big-step semantic) ・ どのように state が変化していくかを表した ものを derivation tree ( 導出木 ) という (P.3 下 の図 ) abbreviation : 省略

Denotational semantics ・ プログラム全体を、個々の命令文の関数合成 と考える (P.4 真ん中の式 ) ・ 例えば、 z := x; は、 z の中身を変化させる関 数だと考える ・ とっっても数学です、プログラムはその対象 です ・ どうやって計算するかは特に考えてない、結 果が全て (Chapter 5 で意味がわかるのでせ う ) Reason : 推論する functional composition : 関数合成 apply : 適用する

Denotational & Operational ・ プログラムの推論 (?) をするには Denotational semantics が有効 ・ つくった言語を implement ( 実装 ) するには Operational semantics が有効 ・ Operational と Denotational が等価であると とても嬉しい → Chapter 4.3 楽しみだな〜 Equivalent : 同等な be adapt to ~ : 構成される

Axiomatic semantics ・ プログラムの部分的正当性を Precondition ( 前提条件 ) と Postcondition ( 後置条件 ) を満 たすかどうかで考える ・ { precondition } construct { postcondition } で表される ・ ただし、プログラムがちゃんと終了するかを 示すものではない ( だから「部分的」なのだ ) Partial : この場合は、終了するかは置いといて、 ( 正しいかどうか ) という感じ ( ついでに ) total : 必ず終了する, 定義域全てに対して値を返すような

Pre とか Post とかって何? 独断と偏見で説明します。 たとえば2次方程式の解を、解の公式を 使って求めるプログラムをつくったとき、プ ログラムがちゃんと動くには、 a, b, c に実数 が入っていて、 a != 0, b^2 - 4ac > 0 の2式が成り立ってる必要があります。こ れが precondition です。 Partial correctness property : ( 終了するかは考えない、プログラムの ) 部分的正当性

Pre とか Post とかって何? で、プログラムが終了 (?) したときには、 変数 x に何らかの実数 ( 求めた解 ) が入ってな いと困りますね。これが Postcondition です。 ちなみに、何回か登場する assertion という言葉 ( 日本語だと「表明」と言う ) は、プログ ラムの中で、プログラマが「ここの時にはこの変数の値はこうなってるか調べてくれ 〜!」 …… というのをプログラム中に書いたりすること ? とかまたはそこに書かれたこ とを言うようです。 Precondition とか Postcondition は ( というか axiomatic semantics は ) 周囲は考えず、た だ与えられた construct が正しいかどうかを判断するためのものなので、 assertion とは 大分意味合いが違います。

話は戻って Axiomatic ・ プログラムの部分的正当性の証明を表したも のを証明木という (P.6 上の図 ) ・ ただし、 {} の中身が同じだからといって、プ ログラムが同じ動きをするとは限らない (P.6 真ん中 ) ・ Axiomatic semantics の利点は、プログラム の性質を簡単に証明できることにある Specification : 仕様 ( 書 )

今後の展望 ・ 3つの semantics を While のために展開す る ・ 3 つの semantics の弱点や利点を While を拡 張することによって図解する ・ While ( の実装 ?) のために、3つの〜の関連 性を証明する ・ 〜のメリットを図解するために、意味記述ア プリケーションの例を示す 3 つの semantics はそれぞれに向き不向きがある。成果を競っているのではない。

While 言語 この本で使うプログラミング言語 ( 定義は P.7) BNF : 前期でおなじみ、みんなよく使ってる、 ( 文脈自由文法の ) 構文の記述法 Syntactic category : 統語範疇 cf. 戸次先生 例えば、前期での 「項」 とか 「値継続」 とか Meta-variables : メタ変数 プログラムで使う変数ではなく、 syntactic category を代表 する変 数のこと 数字なら n, ( まだ出てこないけど ) 文字列は str とかはおなじみ Range over : 動き回る, ( 表す, と考えてよいと思う ) Numeral : (syntactic category としての ) 数 Arithmetic expressions : 計算すると ( 普通の ) 数字になる表現 ( プログラム ) Boolean expressions : 計算すると真偽値になる表現 ( プログラム ) Statement : 命令文

While 言語 ※この定義は抽象的なものなので、よく理解するには、 実際に構文解析木 (syntax tree) を描いてみると良い。 ※最左、最右の区別はない ( 文脈自由文法だから ) ※ていうか、書かれているものが、どの syntactic category に属するかが問題なのである ※ () は必要に応じて多用してよい ※ でも面倒だから + - * and or not なんかは普段数学で 使ってる結合規則を使う Primed : ダッシュをつける subscripted : 下付き文字をつける string : ( 普通の意味で ) 文字列 digit : ( 文字としての ) 数字 Letter : 文字 ( アルファベッ ト ) Basis element : たとえば b の expression のなかで b を含まないもの Composite element : たとえば b の expression のなかで b を含むもの

While 言語 ・ While 言語 ( で書かれたプログラム ) の意味は、 Semantic function ( 意味関数, 後述 ) によって 与えられる ・ Semantic function のためにここまでいろい ろ … 以下略 Entity : もの (syntax 側のものを指しているらしい ) assume : 仮定する Syntactic entity : (syntax に従って書かれたプログラムの ) argument : 引数 Assign : 譲渡する、代入する Semantics function : 意味関数 特にこの本では、 P.7 の syntax で定義されたプログラム (syntactic entity) を受け 取ってきて、その意味 ( 大体は、プログラムを計算した値 ) を返す関数のこと ( あとで 詳しく )

いよいよ Semantics 注意!! ここからしばらく、 numerals は2進法にな ります 他のとこでは10進法です。でも簡単にす るために2進法にします。どう簡単なのかは、 先に進めばわかります。 Binary system : 2進法

しばらく読むだけです P.9 の式を参照 ※ syntactic entity と semantics (meaning) の違 いをはっきり読み分けてください ( 単語も違 うものがあてられています ) ※意味関数の引数は二重角かっこでくくります Number : ( 普通の意味で、10進法の ) 数 Total function : 全ての定義域に対して値を返し、かつ終了する関数 clause : 節 bracket : 角かっこ ( ただ単にかっこ, くくるみたいな意味でも使ってるも よう ) Corresponding : ( 厳密に1対1で ) 対応する application : 適用 Semantics clause : すみません、訳せません。 P.10 に出てくるような定義の一行のこ とです Equation : 方程式

N を合成定義で書く P.10 上半分くらい ・ P.9 の numeral の定義に沿っているでしょう? ※ 二重角かっこの中身が syntax なもの ( 業界では syntax は二重角かっこでくくる習慣があり ます ) ※ ↑ 以外が semantics (meaning) 書いてある数字、記号 は普通に演算できる ※一応、細字が syntactic entity で、太字が semantics らしい ( よくわかんないなあ ) Compositional definition : 合成定義 Obtain : 得る Subconstruct : construct の一部, 部分式

N が well-defined である証明 P.10 真ん中〜 P.11 真ん中 Well-defined : ちゃんと定義されている cf. 計算基礎論 Induction : 数学的帰納法 Base case : 数学的帰納法の最初のところ Induction step : n’ で命題が成立するならば、 n のとき〜 のところ Hypothesis : 仮説 Hold : 有効である, 成り立つ Omit : 省く ex. The case 〜 is similar and we omit the details.

Compositional definition ・ syntactic category が basis element と composite element によって、 ( 明確に ) 定義さ れているとき ・ syntactic category の全ての element に対し て、 semantic clause を定義する。 Composite element に対しては、その構造に見合った定 義をする。 Immediate constituents of the element : Composite element の中に出てくる、自身の syntactic category と同じメタ変数 …… 自分で書いてて何がなんだか あれだ、 b で言えば、 b1 ^ b2 の b1 と b2 がそれだ

Compositional Definition ・ composite element の定義は、部分式に自分 と同じ syntactic category の式を含んでおり ・ さらにその部分式が自分よりも小さくなって いる → composite element を定義に従って分解して いくと、必ず basis element が出てきて、分 解が止まる! → → 帰納法が使える(次スライド) Immediate constituents of the element : Composite element の中に出てくる、自身の syntactic category と同じメタ変数 …… 自分で書いてて何がなんだか あれだ、 b で言えば、 b1 ^ b2 の b1 と b2 がそれだ

Structual Induction ・ compositional definition の証明で有効 ・ まず、 basis element で命題が成り立つこと を証明する ・ 次に、 composite element で、 immediate constituents of the elements では命題が成り 立つという仮説 (induction hypothesis) を立て、 証明をする Structual Induction : 構造帰納法 ※ このあとの numeral は全て10進法です。

Semantic function プログラムの意味(値)を返す関数 → 変数の中身によって返ってくるものが変 わる Semantic function : 意味関数

State ・ 変数をうけとると、その中身を返す関数 ・ “ 環境 ” とは違う (state は変数の中身が変わ る ) ・ 状況 s に変数 x の中身をきくときは、 s x で表す ・ 他の表し方もあるにはあるが、めんどい State : 状況, 状態

意味関数 A ・ expression と state によって、値が決まる → expression と state を受けとって、値を返す 関数 ( A ) を定義する ・ p.9 の型の通り、 A に [[ AExp ]] を渡すと、 state を受け取ると値を返す関数が返ってき て、それに state を渡すと、値が返ってくるよ うな関数である ・ 表記法も ↑ に従っているようだ Functionality : 機能性, 型

意味関数 A ・ 具体的な ( 合成 ) 定義は p.10 上の表 ・ Compositional Definition に従って、=の右側の A の 引数は、左側で引数となっている syntactic entity の 部分式 (immediate 〜 ) となっている ・ さらに、=右側に書かれているものは、演算子など も全て semantic であることに着目されたし ( 二重角 かっこ内は除く ) Sum : 和 product : 積 difference : 差