一般化位值計數系統

Abstract

日常生活中充滿了數值，而位值計數系統是最常見的數值表示方式。 在這篇論文中我們探討並研究各種計數系統的有趣性質與應用，並且在 Agda 裡去建構並且驗證我們發展的一種一般化位值計數系統的方法。我們不只會去探索我們的計數系統與皮亞諾公理的自然數之間的關係，也會發展一套方法去自動轉換彼此之間的定理與證明。

Numbers are everywhere in our daily lives, and positional numeral systems are arguably the most important and common representation of numbers. In this work, we will investigate interesting properties and applications of some variations of positional numeral systems and construct a generalized positional numeral system to model and formalize them in Agda. We will not only examine properties of our representation and its relationship with the classical unary representation of natural numbers but also demonstrate how to translate propositions and proofs between them.