Structural operational semantics

Slides:



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

和田俊和 資料保存場所 /2/26 文法と言語 ー正規表現とオートマトンー 和田俊和 資料保存場所
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
2行+αチョンプに関する考察 京都大学 ○後藤順一 伊藤大雄.
離散数学入門 (集合論、ベン図) 情報システム学科 中田豊久.
アルゴリズムとデータ構造 第8回 ソート(3).
近似アルゴリズム 第10章 終了時刻最小化スケジューリング
© Yukiko Abe 2014 All rights reserved
ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話
    有限幾何学        第8回.
半順序集合ゲーム周期性定理の拡張 京都大学情報学研究科 ○後藤順一 伊藤大雄.
計算の理論 I 決定性有限オートマトン(DFA) と 非決定性有限オートマトン(NFA)
4-3:高度なソートアルゴリズム① (分割統治法にもとづくソート)
データ構造と アルゴリズム 理工学部 情報システム工学科 新田直也.
5.チューリングマシンと計算.
5.チューリングマシンと計算.
Extremal Combinatrics Chapter 4
プログラミング言語論 第6回 型 情報工学科 篠埜 功.
    有限幾何学        第12回.
Object Group ANalizer Graduate School of Information Science and Technology, Osaka University OGAN visualizes representative interactions between a pair.
計算の理論 II 文脈自由文法と プッシュダウンオートマトン
Natural Semantics 実行過程の、最初と最後の状態(state)の関係を考える。
Semantics with Applications
線形代数学 4.行列式 吉村 裕一.
データ構造と アルゴリズム 知能情報学部 新田直也.
言語処理系(5) 金子敬一.
Probabilistic Method 6-3,4
Probabilistic method 輪講 第7回
5.5 The Linear Arboricity of Graphs (グラフの線形樹化数)
計算量理論輪講 岩間研究室 照山順一.
プログラミング言語論プログラミング言語論 プログラムの意味論 水野嘉明
PROGRAMMING IN HASKELL
形式言語の理論 5. 文脈依存言語.
7.4 Two General Settings D3 杉原堅也.
逐次プログラムの正当性(2) 帰納的アサーション法(フロイド法)
 型推論1(単相型) 2007.
25. Randomized Algorithms
Selfish Routing and the Price of Anarchy 4.3
Additive Combinatrics 7
計算の理論 II 時間量と領域量 月曜5校時 大月美佳 2019/4/10 佐賀大学理工学部知能情報システム学科.
2016年度 有限幾何学 中間試験 問1 次のグラフを描け.(描けない場合は理由を述べよ) 各20点
プログラミング言語論 第9回 情報工学科 木村昌臣 篠埜 功.
生物情報ソフトウェア特論 (2)たたみ込みとハッシュに 基づくマッチング
4. システムの安定性.
計算の理論 I 決定性有限オートマトン(DFA) と 非決定性有限オートマトン(NFA)
補講:アルゴリズムと漸近的評価.
計算の理論 I 反復補題 月曜3校時 大月 美佳 平成15年7月14日 佐賀大学知能情報システム学科.
5.チューリングマシンと計算.
米澤研究室 全体ミーティング 2010/07/07 M2 渡邊裕貴.
情報工学概論 (アルゴリズムとデータ構造)
PROGRAMMING IN HASKELL
計算の理論 I -数学的概念と記法- 月曜3校時 大月 美佳.
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
d b c e a f 年度 有限幾何学 中間試験 問1 次の用語の定義をそれぞれ述べよ.
4.プッシュダウンオートマトンと 文脈自由文法の等価性
2017年度 有限幾何学 期末試験 注意:ループと多重辺がないグラフのみを扱う. 問1 次の定理と,その証明の概略を読み,各問に答えよ.
ヒープソート.
コストのついたグラフの探索 分枝限定法 A*アルゴリズム.
PROGRAMMING IN HASKELL
計算の理論 I 反復補題 火曜3校時 大月 美佳 平成16年7月13日 佐賀大学知能情報システム学科.
問2 次の問に答えよ. (ただし,握手補題,オイラーの定理,Oreの定理 は授業で紹介したものとする) (1) 握手補題を書け.
図2 x11 図1 x6 x10 x12 x3 x5 x7 x9 x13 x2 x4 x8 x14 (0,0) (1,0) x1 x15
情報数理Ⅱ 第10章 オートマトン 平成28年12月21日.
計算の理論 I プッシュダウンオートマトン 月曜3校時 大月 美佳 平成15年7月7日 佐賀大学知能情報システム学科.
計算の理論 II 多テープTuring機械 月曜4校時 大月美佳 平成16年11月29日 佐賀大学知能情報システム学科.
計算の理論 II 時間量と領域量 月曜4校時 大月美佳 2019/9/13 佐賀大学理工学部知能情報システム学科.
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
Static Enforcement of Security with Types
グラフの帯域幅連続多重彩色 を求めるアルゴリズム (Bandwidth Consective Multicolorings of Graphs) 西関研究室 西川和秀.
Time Reversal E-Text: pp.80-83(PDF: pp.49-50) FM08002 太神 諭
Presentation transcript:

Structural operational semantics Transition relation の形は、                <S, s> ⇒ r と表す。       (1)rが<S’, s’>の形           状態sにおけるSの実行が終わらなかっ  た。結果ではなく、中間の形。      (2)rがs’の形                      状態sにおけるSは終了して、最終状態はs’。 rが存在しなければ、stuck(行き詰まった?)と 呼ぶ。

finite と infinite 状態sからステートメントSを実行したとき、derivation sequence は以下の2つのどちらかになる。                    (1) finiteなシーケンス              r0, r1, r2, ‥ rk rkはterminalかstuck  の形                       (2)infiniteなシーケンス             r0, r1, r2, ‥

ステップ数の表し方 r0 ⇒i ri ‥ r0からriまで実行するのにiステップあることを示す。 r0 ⇒* ri ‥ r0からriまで実行するのに、有限回のステップがあることを示す。 上の2つは、derivation sequence でなくてもよい。riがterminal もしくは、stuckの形であればよい。

terminateとloop <S, s>から始めて、有限のderivation sequenceになるとき、状態sにおけるステートメントSの実行はterminateするという。 <S, s>から始めて、無限に続くderivation sequenceになるとき、状態sにおけるステートメントSの実行はloopするという。

定義 状態sにおけるステートメントSの実行は、<S, s> ⇒* s’になるとき、成功した(terminate successfully)という。 また、Sがすべてのsにおいて終了するとき、Sはいつでも終了するという。 また、Sがすべてのsにおいてloopするとき、Sはいつでもloopするという。

Property of the semantics Structural operational semantics では、derivation sequence の長さにおける帰納法で証明するのが好都合である。 実際証明するときは、この帰納法のステップは以下のどちらかを調べることでなされる。(1)syntaxの要素の構造         (2)derivation sequenceの最初の  transitionの正当性を証明する導出木

Induvction on the Length of Derivation Sequence(derivation sequenceの長さにおける帰納法) 1, まず示したい性質が全ての長さが0のderiation sequenceにて成立することを示す。 2, 次に他の全てのderivation sequence にて成立することを示す。長さが最大でkの全てのderivation sequenceを満たすことを仮定する(induction hypothesis)。そして、長さがk+1のderivation sequenceでも成立することを示す。

定理2.19 <S1; S2, s> ⇒k s” ならば、  <S1, s> ⇒k1 s’かつ<S2, s’> ⇒k2 s”である。(ただしk = k1 + k2)         となるような状態sと自然数k1とk2が存在する。

deterministic テーブル2.2が、全てのS, s, r, r’において、<S, s> ⇒ r かつ<S, s> ⇒ r’ならば r = r’であるとき、テーブル2.2はdeterministicであるという。