読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

二進表現じゃない整数型

この前作ったマイポジティブ型は、ペアノの公理を元にした形式化だったので、それを使って、ペアノゼットという整数型を作ってみた。
既存のポジティブ型とマイポジティブ型との間の同型対応は、前回示してあるので、それをもとにしている既存のZ型とペアノゼット型との間の同型も示すことができる(ここでいう同型とは、環同型および順序同型のことである)。
よって、新たに作ったPeanoZという整数型に対しても、既存のZとその演算に関する全ての定理が成り立つことが示せる。さらに、今後ZもしくはPeanoZで示すことができた性質は、両方で成り立つことが保証されるのである。