:book: 文章 模算術:beginner:新手友善 :computer:程式語言 :heavy_division_sign:數論 同餘關係、模倒數 談 Void：以依值型態語言 Idris 為例 :computer:程式語言 𝝺函數程設 依值型態、Curry--Howard 對應 啥物是 Lambda Calculus

礙於技術限制，各項公式未能個別標註出處。 參考文獻統一排列於「參考文獻」節。 學術引用時務必完整標示所有文獻。 :::spoiler 目錄 ::: 偏序集 基本定義

這裡記錄一些有關結合律的演算法。 :::spoiler 目錄 ::: 前言 基本代數定義 這裡用比較偏集合論的語言來描述。

:::spoiler 目錄 ::: 形式冪級數 基本定義 交換環 $R$ 上的形式冪級數（formal power series）就是 $R$ 上的無窮序列 $A = (a_0, a_1, \dotsc)$。 我們形式上將它寫成 \[ A(x) = \sum_{k\ge 0} a_k x^k \]

礙於技術限制，各項公式未能個別標註出處。 參考文獻統一排列於「Reference」節。 學術引用時務必完整標示所有文獻。 $\newcommand{\args}[1]{\langle{#1}\rangle}$ $\newcommand{\Hrd}[2][w]{\mathbf{#1}\args{#2}}$ $\newcommand{\LcsI}[1]{\Hrd[u]{#1}}$ $\newcommand{\LcsII}[1]{\Hrd[v]{#1}}$ $\newcommand{\Mat}[1]{\begin{bmatrix} #1 \end{bmatrix}}$ $\newcommand{\HProd}[2]{\Mat{ #1 \ #2 }}$

{%hackmd @YuRen-tw/theorem-theme %} <!-- {%hackmd @YuRen-tw/article-theme %} --> <style> :root { --margin-between: 16px; --box-padding: 12px; --font-size: 16px; --br-space-width: 0; /* color */ --color-main: #fdc565; --color-light: #f6b763; --color-dark: #917254; --color-grey: #61574c; --color-alpha: rgb(253 197 101 / .2); /* theorem-theme */ --thm-margin: var(--margin-between); --thm-padding-box: var(--box-padding); --thm-bac

組合子 combinator I = \ x . x恆等函式：I x = x I = S K K Haskell：id K = \ x y . x 常數函式：K x = \ _ . x Haskell：const, pure for Applicative (r →)

模算術（modular arithmetic）又可稱為同餘算術，是一種特別的整數算術系統。 這個系統要先指定一個整數 $m$ 做為模數（modulus），而系統裡的數值就會像是在 $0$ 到 $m-1$ 的圈圈裡面一樣，如果互相運算後的數值要超出了這個範圍，就會繞回範圍內對應的數值。 日常生活中，表示時刻周而復始的時候就很常應用模算術。 比如說 22 點過了 $8$ 個小時之後會說是 6 點，而不會說是 30 點（好吧，事實上有人這麼說）。 一天 $24$ 小時，$24$ 就是這裡的模數，而我們講「幾點」的時候只在乎它距離半夜的 0 點過了多少小時，這種觀點下的 $30$ 跟 $6$ 會是一樣的意思。 同餘 同餘關係 如同上面一天 $24$ 小時的例子，在這樣周而復始的系統裡面，一個數值不管中間繞了多少圈，我們在乎的只有它比起點多了多少。

在許多程式語言中，我們可以為變數或函式標上型態。 型態能用來提示這個東西的結構以及它如何被使用，比如整數型態能做整數運算。 在實際執行程式以前，機器可以以此決定要分配多少空間來容納資料，或是根據型態做出特定的最佳化。 同時我們也能先透過型態檢查來避免人類的編寫錯誤，比如錯誤地將整數與文字相減。 更進一步地，我們也發展了型態理論（type theory），研究一個型態系統究竟可以表達出哪些機制來輔助我們。 這篇討論我們會提到兩種特別的型態：Unit 與 Void。 只有一個值屬於 Unit 型態，那個值記為 ()。 沒有任何值屬於 Void 型態。

在 HackMD 筆記加入下列，即可套用 article theme。 以下說明文件中標有「:gear:」的部分代表對應的 CSS 設定，使用者可以自己利用 <style> 做進一步的修改。 :::spoiler 大綱 ::: 更改 HackMD 預設樣式 標題

功能 在 HackMD 筆記加入下列，即可套用 theorem theme。 套用後，就可以用以下的 HTML 產出對應的定理區塊： <div class="theorem"> Prime numbers are more than any assigned multitude of prime numbers. </div> <div class="proof">

<!-- {%hackmd @YuRen-tw/theorem-theme %} --> <style> :root { --thm-margin: 16px; --thm-padding-box: 12px; --thm-padding-inline: var(--thm-padding-box); --thm-padding-head: 4px; --thm-italic-style: normal; /* color */ --thm-background-color: #eee; --thm-outline-color: #888; --qed-symbol: "\220E"; /* theorem head */ --thm-name: ""; --thm-info: ""; --thm-info-before: "："; --thm-info-after: ""; --thm-head-end: ""; --thm-na

話頭 Lambda calculus 是數學家 Alonzo Church 發表出來的，是用替換規則來稽考函數的一个形式系統。 原底 lambda calculus 干焦是欲用來研究數學的基礎，毋過後來咱發現伊有真濟袂䆀的應用，所以佇這馬的計算機科學（computer science）、邏輯學甚至是語言學攏會使看著伊的身影。 尤其是這幾冬，有愈來愈濟寫程式的人認捌著講函數型程式設計（functional programming）的理路是誠有智慧，寫 FP 袂輸一件蓋奅的代誌，lambda calculus 嘛綴咧出現佇逐家的面頭前。 雖然伊名後壁的 calculus 佮微積分仝名，無過莫予伊嚇驚著。 lambda calculus 無啥物複雜的運算，嘛無啥物恐怖的符號，干焦一點仔替換規則。 咱佇這篇文內底會對數學函數的概念開始，簡單、直覺的紹介 lambda calculus。 函數

數學家： 約翰·何頓·康威 U10511044 潘昱仁 約翰·何頓·康威 John Horton Conway (1937/12/26－2020/4/11) 外觀數列 Look-and-say sequence $1,11,21,1211,111221,312211,13112221,\dots$OEIS:A005150