ひよこの外部記憶

めもおきば

アンダースタンディングコンピューテーション 2章

下の書籍2章の話

https://www.amazon.co.jp/dp/487311697X

※ 読んでる時に書いたメモです、アンダースタンディングコンピューテーションを要約するようには書いていません。

第一部 プログラムと機械

計算

計算には以下の要素が必要

  • 計算を行う機械
  • 機械が解釈できる言語
  • 言語によって書かれる実行すべき計算を表すプログラム

意味論とは?

言葉と意味の関係に関する学問

形式的意味論

プログラミングの意味を明確にし、プログラミングに関する興味深い事を発見する
→ 数学のトポロジーみたいな感じかな？

プログラミング言語の仕様を完全に記述するには

  1. 構文(どのように見えるか)
  2. 意味論(何を意味するか)

が必要

プログラミングの言語の仕様

実装による仕様

Rubyもこれ
→MRI(Matz's Ruby Interpreter)によって定義、JRubyやMacRuby等はMRIの振る舞いと完全に一致する必要がある

公文書による仕様

JavaやECMAScript
専門家によって十分に議論されたドキュメントにより仕様を定義

形式意味論による仕様

数学的手法によりプログラミング言語の意味を正確に記述する

構文とは？

特定の言語により有効なプログラムであるかを判定する規則
→パーサにより判断

パーサの役割はASTを作成する事
= 構文上問題ない場合(ASTが問題なく作られる場合)でもプログラムとしては問題がある状態がある

# AST作れるけど、プログラム的には問題がある例
y = x + 1

操作的意味論

  • プログラムがある種のプログラム上でどのように実行されるのか、規則を定義する
  • プログラム言語毎に異なる抽象機械が必要

スモールステップ意味論

  • 構文を小さなステップに簡約することで、プログラムを評価する機械を考える
    • 評価出来る部分から評価する

四則演算のふるまい記述

class Number < Struct.new(:value)
  def to_s
    value.to_s
  end

  def inspect
    "<<#{self}>>"
  end

  def reducible?
    false
  end
end

class Add < Struct.new(:left, :right)
  def to_s
    "#{left} + #{right}"
  end

  def inspect
    "<<#{self}>>"
  end

  def reducible?
    true
  end

  def reduce
    if left.reducible?
      Add.new(left.reduce, right)
    elsif right.reducible?
      Add.new(left,right.reduce)
    else
      Number.new(left.value + right.value)
    end
  end
end

class Multiply < Struct.new(:left, :right)
  def to_s
    "#{left} * #{right}"
  end

  def inspect
    "<<#{self}>>"
  end

  def reducible?
    true
  end

  def reduce
    if left.reducible?
      Multiply.new(left.reduce, right)
    elsif right.reducible?
      Multiply.new(left, right.reduce)
    else
      Number.new(left.value * right.value)
    end
  end
end

同様な感じで他の四則演算記号や"<"やBool値等も作れる

変数

変数の機能を持つためには、仮想機械は現在の式の他に環境(environment)を持つ必要がある
→#reduceをenvironmentを引数に取るように変更、仮想機械は自身の式の中に変数が出てきたらenvironmentを探して簡約する

こんな感じ

class Variable
  def reduce(environment)
    environment[name]
  end
end

# 各#reduceは以下の様な感じに変更
def reduce(environment)
  if left.reducible?
    Add.new(left.reduce(environment),right)
  end
  ・・・
end

if文

こんな感じ

class If < Struct.new(:condition, :consequence, :alternative)
・・・
  
  def reduce(environment)
    ・・・
    case condition
    when Boolean.new(true)
      [consequence, environment]
    when Boolean.new(false)
      [alternative, environment]
    end
  end
end

while文

if文に置き換える事で解決 こんな感じ (SequenceとDoNothingは書籍参照)

class While < Struct.new(:condition, :body)
  ・・・
  def reduce(environment)
    [If.new(condition, Sequence.new(body, self), DoNothing.new), environment]
  end
end

ビックステップ意味論

  • ビックステップはASTを一度走査することで、どうやってプログラム全体の結果を計算するかを記述
  • スモールステップよりも大雑把な感じ(再帰で一片に解決する)

※載せると長くなるので省略

OCamlのコア言語はビックステップで説明されている

式と文

  • 文はそれ単体で完結する → 評価された時に戻り値を捨てる
  • 式は何かの一部 → 評価された時の戻り値を使う

だから、SQLのCASE式というのは評価され何かに置き換わる →どこにでも書ける

  • RubyとPythonの違いは式と文の違いがあるかどうか(るびま)
    • 例えばa=1とかは文であるが、Rubyは戻り値を返す、Pythonは式を書くべき箇所に文を書くとエラーになる

式

  • 評価されることで別の式を生成
    • スモールステップではreduce出来ない所までreduceする
  • 式をreduceして新たな式を作る、これをreduce出来ない所まで繰り返す
  • 今までやっていた例は全ての部分が式

文

評価されることで抽象機械のenvironmentを変更

代入では

x = x + 1

の場合、右辺が式、全体は文になる

  • 文の評価は、右辺がreduce出来るか見て、出来ればreduce、出来なければ代入を行う
  • 文の評価によって、初めて状態が変更される

表示的意味論

  • プログラムをネイティブ言語から別の表現に変換
    • 「Rubyで書くとこんな書き方〜」

walkの意味を伝える場合 - 実際に歩いてみせる(操作的) - 「歩く」の英語表現、等と既に知っているであろう知識とマッピングする(表示的)

  • Rubyで実装する場合には、ASTが意図した意味を表現するRubyコード文字列に変換する事
    • procオブジェクトを作る感じ

Rubyで書いたため実行可能であるが、例えば「数式」「英語」等で表される場合にはもちろん無理

まとめ的なもの

今までの動作の違い

今までの違いを見るにはwhileの動作を見るとわかりやすい

スモールステップ意味論のwhile

  • 抽象機械の簡約規則として書かれる
    • ループとしての振る舞いは出てこない スモールステップ意味論から言語を理解するには、スモールステップ規則を全て調べ、それがどのように作用するか見る

ビックステップ意味論のwhile

  • 最終的な環境を直接計算する方法が書かれる
    • どのように振る舞うかはWhileの記述を見ればわかるが、これを見ただけでは環境がどのように変更されるか等が分からない

表示的意味論のwhile

実際の形式意味論

形式意味論の重要な応用は

  • 「実装による仕様」等の非形式的仕様に頼らない、あいまいさのない仕様を与えること
  • 言語の一般的な特性及び具体的なプログラムの特性を証明すること

  • 振る舞いを変えることなく効率をこうじょうさせるようプログラムを安全に変換する方法を見つけること

  • 操作的意味論はインタプリタの実装に密接に関係するため、言語の正当性を証明出来る

  • 表示的意味論はプログラムの実行方法を無視して別の表現に変換する方法に着目している、これは、コンパイラが行う動作に近い