Skip to content

Instantly share code, notes, and snippets.

@pi8027
Last active February 4, 2022 04:29
Show Gist options
  • Save pi8027/01fc48c13f2ed893e326439bd9a266b1 to your computer and use it in GitHub Desktop.
Save pi8027/01fc48c13f2ed893e326439bd9a266b1 to your computer and use it in GitHub Desktop.
Hilbert-Post Completeness of BoolState
以下は Lecture 1: Algebraic Effects I (Gordon Plotkin) - Exercise 5 の解である。
http://cs.ioc.ee/ewscs/2015/plotkin/plotkin-slides-exercises1.pdf
p. 31 の等式理論 BoolState より、いかなる式に対しても
read(write_b1(x), write_b2(y)) (x, yは変数)
という形の normal form が自然に与えられる。
以下のように、2つの異なる normal form に関する等式を仮定する:
read(write_b1(x), write_b2(y)) = read(write_b1'(x'), write_b2'(y')) (b1 ≠ b1' ∨ x ≠ x' ∨ b2 ≠ b2' ∨ y ≠ y')
このとき、b1 ≠ b1' ∨ x ≠ x' の場合は write_true、b2 ≠ b2' ∨ y ≠ y' の場合は write_false を上に示した等式の外側に付け、公理に従って式変形し、代入を行うことで
write_b3(z) = write_b3'(z') (b3 ≠ b3' ∨ z ≠ z')
が導ける。ここから、いかなる b, w, w' についても write_b(w) = write_b(w') が成り立つことを導く。
- b3 = b3' かつ z ≠ z' の場合:
各変数への代入(b3 = b3' = b, z = w, z' = w')により目的の式が導ける。
- b3 ≠ b3' の場合:
必要に応じて対称律を用いることで write_true(z) = write_false(z') が導ける。この両辺に z = z' = read(write_b(w), write_b(w')) を代入すると、
write_true(z) = write_true(read(write_b(w), write_b(w'))) = write_true(write_b(w)) = write_b(w),
write_false(z') = write_false(read(write_b(w), write_b(w'))) = write_false(write_b(w')) = write_b(w')
となるので、write_b(w) = write_b(w')。
上に示したように、任意の b, w, w' について write_b(w) = write_b(w') が成り立つので、任意の x, y について
read(write_true(x), write_false(x)) = read(write_true(y), write_false(y))
が導ける。この式と
read(write_true(x), write_false(x)) = read(x, x) = x,
read(write_true(y), write_false(y)) = read(y, y) = y
より、x = y。
2つの異なる normal form に関する等式が成り立つと仮定し、BoolState の公理を用いて任意の x, y について x = y であることを示したので、等式理論 BoolState は Hilbert-Post complete である。
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment