Understanding Computationを読む[1~2章]

アンダースタンディングコンピュテーションは、計算理論について数式を用いずに、rubyによる実装で解説していく本です。

勉強ログをローカルで保存しても読み返さないと思うのでブログで書いていきます。

1章

rubyの文法解説なので省略

Ⅰ部 プログラムと機械

計算を行うために必要な3つの構成要素
  • 計算を実行することができる機械
  • 機械が理解できる命令を書くための言語
  • 上記の言語で書かれた、機械が実行すべき計算を正確に記述したプログラム

2章

コンピュータサイエンス形式意味論

プログラムの意味を明確にし、プログラミング言語について色々発見したり、証明したりする。

例: 言語の仕様化、コンパイラ最適化、プログラムの正当性の数学的証明

構文

どんな文字列がその言語で有効なプログラムとして見なされるかを記述した規則

例: y = x + 1>/;x:1@4を区別できる

プログラム文字列をパーサが読み込んで抽象構文木(AST)に変換する

操作的意味論

プログラムをある種の装置上で実行した時、言語の構成要素はどのように振る舞い、それらを組み合わせたときどんな効果が起こるのか、を見る方法。抽象機械と呼ばれる架空のコンピュータ上で実行される。

  • スモールステップ意味論

構文を小さなステップで繰り返し簡約し、プログラムを評価する機械を考える。

以降、この章ではSIMPLEという簡単なプログラミング言語の意味論について調べていく。

演算子AddMultiplyは常に簡約可能。値Numberは簡約不可能。

足し算式を簡約する場合、左右の引数が両方簡約可能なときは簡約する順序の規則を作る。

スモールステップ操作的意味論では、ある規則によって式が別の式に変換される。

言語を評価する仮想機械を実装することで、簡約ステップを自動化する。

変数を作る。変数名から値をマッピングする環境(rubyではHash)

文の目的は、評価されることで抽象機械の状態を変更すること。式を簡約しても環境は変化しない。

→ 式は純粋であり、文は純粋でない

正当性

x = true, x = x +1を実行しようとすると、true1を足そうとして失敗する。

これを防ぐために、式が簡約可能かどうかをさらに制限する。すると、評価が停止する可能性が出てくる。

ビッグステップ意味論

どうやって式や文から直接結果を得るかを記述する。大きな式を評価するために小さな部分式をすべて評価し、最終的な答えを得る。

プログラムの実行プロセスを反復ではなく、再帰としてみなす。

表示的意味論

プログラムをその言語の表現から別の言語の表現に変換し、説明する。