練習問題

問1

自然数の仕様のモジュール NAT+ において、+ に交換律が成り立つことを証明する証明譜を作成し、CafeOBJ に読み込ませて証明せよ。

問2

+ の結合律と交換律が証明済みのモジュール NAT+AC と自然数上の乗算 * が定義された NAT* は、以下のように定義できる:

mod! NAT+AC {
  pr(NAT+)
  op _+_ : Nat Nat -> Nat { assoc comm }
}

mod! NAT* {
  pr(NAT+AC)
  op _*_ : Nat Nat -> Nat
  eq 0 * M:Nat = 0 .
  eq s(N:Nat) * M:Nat = M + (N * M) .
}

上記のモジュール NAT* を用いて、分配律 i * (j + k) = (i * j) + (i * k) が成り立つことを証明する証明譜を作成し、CafeOBJ に読み込ませて証明せよ。

問3

交換律や結合律を、問2のモジュール NAT+AC のように宣言せず、次のように等式で宣言するのは妥当かどうか検討せよ。

mod! NAT+AC2 {
  pr(NAT+)
  -- associativity on _+_
  eq (I:Nat + J:Nat) + K:Nat = I + (J + K) .
  -- commutativity on _+_
  eq I:Nat + J:Nat = J + I .
}

[Next]

Original Copyright © Takahiro Seino, all rights reserved.