標題: | 一般化位值計數系統 Generalizing Positional Numeral Systems |
作者: | 賴廷彥 穆信成 楊武 Luā, Tîng-Giān Mu, Shin-Cheng Yang, Wuu 資訊科學與工程研究所 |
關鍵字: | 構造性數學;計數系統;定理證明;一階邏輯;Agda;Constructive mathematics;Numeral systems;Theorem proving;Agda;First-order logic |
公開日期: | 2017 |
摘要: | 日常生活中充滿了數值,而位值計數系統是最常見的數值表示方式。
在這篇論文中我們探討並研究各種計數系統的有趣性質與應用,並且在 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. |
URI: | http://etd.lib.nctu.edu.tw/cdrfb3/record/nctu/#GT070356008 http://hdl.handle.net/11536/140398 |
顯示於類別: | 畢業論文 |