一般化位值計數系統

Generalizing Positional Numeral Systems

賴廷彥(Tîng-Giān Luā)

指導教授 ： 穆信成 ； 楊武

國立交通大學/資訊學院/資訊科學與工程研究所/碩士(2017年)

摘要

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

關鍵字

構造性數學 ； 計數系統 ； 定理證明 ； 一階邏輯 ； 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.

並列關鍵字

Constructive mathematics ； Numeral systems ； Theorem proving ； Agda ； First-order logic

參考文獻

[1] P. Benacerraf. What numbers could not be. The Philosophical Review, 74(1):47–73, 1965.

[4] R. Hinze et al. Numerical representations as higher order nested datatypes. Technical report, Citeseer, 1998.

[5] D. E. Knuth. The art of computer programming. volume 2, seminumerical algorithms. 1998.

[9] C. McBride and J. McKinna. The view from the left. J. Funct. Program., 14(1):69– 111, Jan. 2004.

[10] S.-C. Mu. Dependently typed programming. Lecture handouts, jul 2016.