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

ucrubyprogrammingbook

Posted onOct 17, 2014


今日からアンダースタンディング コンピュテーション (オライリー) を読みはじめた。第 1 章は Ruby 入門なので飛ばす。 第 2 章では SIMPLE という言語の小ステップスタイルな操作的意味論 (p.21) を Ruby で記述する。

操作的意味論を Ruby で記述する意義については p.22 に下の注意があった。

Ruby を使うことの大きな欠点は、単純な言語を説明するのにより複雑な言語を使っていることで、おそらく哲学的意義を損ねています。 数学的規則は意味論の信頼できる記述であり、Ruby を使うのは数学的規則が意味することを理解しやすくするため、 であることを忘れないでください。

数値とブール値

数値やブール値は値なので簡約できない。これを表すのに #reducible? メソッドで false を返すようにしておく。

class Number < Struct.new(:value)
  def reducible?
    false
  end
end
class Boolean < Struct.new(:value)
  def reducible?
    false
  end
end

足し算

$$\frac{e_1 \to e’_1} {e_1 + e_2 \to e’_1 + e_2}$$

$$\frac{e_2 \to e’_2} {v_1 + e_2 \to v_1 + e’_2}$$

$$n_1 + n_2 \to n\ \mathsf{if}\ n = n_1 + n_2$$

class Add < Struct.new(:left, :right)
  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

irb で実行するとこんな感じ。

>> Add.new(Number.new(3), Number.new(4)).reduce
=> <<7>>

かけ算

$$\frac{e_1 \to e’_1} {e_1 \ast e_2 \to e’_1 \ast e_2}$$

$$\frac{e_2 \to e’_2} {v_1 \ast e_2 \to v_1 \ast e’_2}$$

$$n_1 \ast n_2 \to n\ \mathsf{if}\ n = n_1 \times n_2$$

class Multiply < Struct.new(:left, :right)
  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

irb で実行するとこんな感じ。

>> Multiply.new(Add.new(Number.new(1), Number.new(2)), Number.new(3))
=> <<1 + 2 * 3>>
>> Multiply.new(Add.new(Number.new(1), Number.new(2)), Number.new(3)).reduce
=> <<3 * 3>>

Less than (<)

$$\frac{e_1 \to e’_1} {e_1 < e_2 \to e’_1 < e_2}$$

$$\frac{e_2 \to e’_2} {v_1 < e_2 \to v_1 < e’_2}$$

$$n_1 < n_2 \to \tt{true}\ \mathsf{if}\ n = n_1 < n_2$$

$$n_1 < n_2 \to \tt{false}\ \mathsf{if}\ n = n_1 \geq n_2$$

class LessThan < Struct.new(:left, :right)
  def reduce
    if left.reducible?
      LessThan.new(left.reduce, right)
    elsif right.reducible?
      LessThan.new(left, right.reduce)
    else
      Boolean.new(left.value < right.value)
    end
  end
end

仮想機械

仮想機械はどんどん簡約していくだけ。シンプル。

class Machine < Struct.new(:expression)
  def step
    self.expression = expression.reduce
  end

  def run
    while expression.reducible?
      puts expression
      step
    end
    puts expression
  end
end