『アンダースタンディング コンピュテーション ―単純な機械から不可能なプログラムまで』
https://images-na.ssl-images-amazon.com/images/I/51kSuWt53uL._SX389_BO1,204,203,200_.jpg https://www.amazon.co.jp/%E3%82%A2%E3%83%B3%E3%83%80%E3%83%BC%E3%82%B9%E3%82%BF%E3%83%B3%E3%83%87%E3%82%A3%E3%83%B3%E3%82%B0-%E3%82%B3%E3%83%B3%E3%83%94%E3%83%A5%E3%83%86%E3%83%BC%E3%82%B7%E3%83%A7%E3%83%B3-%E2%80%95%E5%8D%98%E7%B4%94%E3%81%AA%E6%A9%9F%E6%A2%B0%E3%81%8B%E3%82%89%E4%B8%8D%E5%8F%AF%E8%83%BD%E3%81%AA%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%A0%E3%81%BE%E3%81%A7-Tom-Stuart/dp/487311697X
第I部
第一章
計算(computation)の基本構成要素
機械(machine)
プログラム(program)
第二章
プログラムの意味(semantics)
意味(semantics)
形式的意味論(formal semantics)
とらえどころのないプログラムの意味を明確にする学問
プログラム
構文自体に意味があるわけではない
プログラミング言語には有効なプログラムだとみなされるための構文規則がある
これをsyntaxという
このsyntaxをコンピューターが読むためにパーサー(parser)がある
プログラムの構文規則を抽象構文木(Abstract Syntax Tree, AST)に変換する
操作的意味論(operational semantics)
プログラムを実行すると、その構成要素がどのように振る舞うのか、それを組み合わせるとどんな効果が生まれるのか
プログラムがある種の装置上でどのように実行されるのかの規則を定義したもの
プログラム実行時の振る舞いをきちんと定義したもの
プログラムの実行プロセスが「反復(iterative)」になる 他の呼び名
構造的意味論(strctural operational semantics)
遷移意味論(transition semantics)
構文を小さなステップ(small step)で繰り返して、簡約(reduce)してプログラムを評価するような機械 メタ言語によって数学的に記述された簡約関係(reduce relation)を推論規則(inference rule)といい、この集合をいう。 評価して別の式を生成することが目的
環境は変更されないので純粋(pure)
評価することで抽象機械の状態を変更することが目的
代入(assignment)など...
環境が変更されるので純粋でない(inpure)
簡約の順序などが例
変数などを導入したとき、これを簡約するためには仮想機械に環境(environment)を導入する必要がある
ビッグステップ意味論
他の呼び名
自然意味論(natural seamntics)
関係意味論(relational semantics)
文がどのように動くのかをもっと直接的に説明する方法
どうやって式や文から直接結果を得るかを記述する
プログラムの実行プロセスが再帰(recursive)になる 表示的意味論(denotational semantics)
他の呼び名
不動点意味論(fixed-point semantics)
数学的意味論(mathmactical semantics)
プログラムをネイティブ言語から別の表現に変換することに関心
すでに確立された低レイヤーで形式的な言語の意味を利用して新しい言語を説明すること
言語を振る舞いにするのではなく、ある言語を別の言語に置きかえる
実際の形式的意味論
数学的表記が基本
パーサー(parser)
...