proof🚧
proof
數學是建構而成。上一個主題衍生下一個主題。
以最近流行的深度學習作為範例。當我們想要學習什麼是訓練神經網路，學習路線大致如下：
數數：自然數0 1 2 3 4……。 加法：數數重複很多次。 乘法：加法重複很多次。 反運算：已經知道加法／乘法計算結果，反過來找到重複次數。 形成減法與除法。 算式：加減乘除組合起來。先乘除、後加減。 方程式：算式挖空一個數字。利用反運算得到挖空的數字。 關係：算式挖空兩個數字。一個當作輸入，一個當作輸出。 函數：關係追加限制條件。一種輸入只有一種輸出、不能有多種輸出。 根：什麼輸入使得輸出是零。 極值點：什麼輸入使得輸出最小／最大。 連續函數：如果輸入相鄰，那麼輸出相鄰。 微積分：連續函數的運算，除了加減乘除，又追加了微分與積分。 積分：輸出前綴和乘以dx。每種輸入都要算。 微分：輸出相鄰差除以dx。每種輸入都要算。積分的反運算。 最佳化：找到極值點。極值點位於微分等於零的地方。 梯度下降法：修改輸入，讓輸出變大。 利用微分（梯度），找到讓輸出變小的修改方向。 一直修改，直到遭遇微分等於零的地方。 神經網路：一個函數的輸出，作為另一個函數的輸入。 一大堆函數，串成網路。 反向傳播法：神經網路的梯度下降法。 尋找梯度，從尾端函數依序到首端函數。 修改輸入，從首端函數依序到尾端函數。 迴歸：給予輸入與輸出的大量配對，求得函數係數。 建立平方誤差函數，變成最佳化問題。 訓練神經網路：神經網路迴歸。
證明就是找出這條建構路線。想方設法找到路線上面每個主題。表示成列表風格或者樹狀風格，一如邏輯學的自然演繹。
大家認識數學，是從數數開始。數學家深入追溯數數的源頭，發現了更加基礎的主題，並且以此建構出數數，或者換句話說，證明數數。以方才的範例來說明，數學家發現了數數的上面還有一連串更加基礎的主題，而且擁有許多種建構方式，例如Heyting arithmetic。
大學數學課本當中，直接當作常識的等於運算律：自反律、對稱律、遞移律，加法運算律：交換律、結合律、分配律，都可以用這些更加基礎的主題來證明。
小學數學課本當中，直接當作常識的1+1=2，也可以用這些更加基礎的主題來證明。我想要那艘戰艦。
proof theory
Type Theory and Formal Proof: An Introduction Proof Theory / Gaisi Takeuti Basic Proof Theory Natural Deduction: A Proof-Theoretical Study
type🚧
type theory
Type Theory and Formal Proof: An Introduction Homotopy Type Theory: Univalent Foundations of Mathematics PROGRAM = PROOF
https://www.ps.uni-saarland.de/courses.html http://www.cs.cmu.edu/~rwh/courses/chtt/ http://www.cs.ru.nl/~freek/courses/tt-2013/ http://www.cs.cornell.edu/courses/cs6180/ https://www.cs.cornell.edu/courses/cs3110/2020sp/lectures.html
我不打算整理。我只找了資源，各位請自便。
category theory
Category Theory for Programmers Category Theory for Computer Science Category Theory for the Sciences
The Joy of Abstraction: An Exploration of Math, Category Theory, and Life An Invitation to Applied Category Theory: Seven Sketches in Compositionality Introduction to Higher-Order Categorical Logic
category theory = type theory https://cs.stackexchange.com/questions/3028
我不打算整理。我只找了資源，各位請自便。
mathematical logic🚧
mathematical logic
數學邏輯重塑邏輯學所有概念，重新歸類命名，形成四大領域：
set theory 集合論（來自predicate） proof theory 證明論（來自derivation） model theory 模型論（來自interpretation） recursion theory 遞迴論（來自language/automaton）
數學名詞全面以邏輯學名詞重新定義，變得嚴謹。
[formal language]
sentence = statement
language = a set of sentences
grammar = a set of rule of inference
substitution = rule of replacement
[formal proof]
theory = a set of sentences
calculi = inference
axiom = a set of premisses
proof = derivation
assumption = argument
hypothesis = premiss
theorem = conclusion
[formal proof with first-order logic]
formula = theorem
valuation = interpretation
structure = (?)
model = a set of satisfiable intepretations for all formulas
(consistency)
programming language🚧
programming language
Programming Language Pragmatics Types and Programming Languages Practical Foundations for Programming Languages The Structure of Typed Programming Languages Formal Semantics of Programming Languages Introduction to the Theory of Programming Languages Software Foundations Communicating Sequential Processes
https://github.com/steshaw/plt
想要瞭解程式語言理論，可以讀這些書。
imperative programming language
C++ Primer The C++ Programming Language A Tour of C++ Discovering Modern C++: An Intensive Course for Scientists, Engineers, and Programmers Effective C++: 55 Specific Ways to Improve Your Programs and Designs Effective Modern C++: 42 Specific Ways to Improve Your Use of C++11 and C++14
指令式程式語言是當今最普遍的程式語言。甚至現在已經成為中學課程的一部分了。生而為人，這是必須要知道的基本常識。
硬體韌體C、應用程式C++、視窗軟體C#、手機軟體Java與Kotlin、函式庫調用Python、瀏覽器操作JavaScript、網頁設計PHP、伺服器程式GO、系統程式Rust、定位不明的D、數學工具MATLAB、統計學工具R、科學計算Fortran、金融交易COBOL、……，這些都是指令式程式語言。語言越來越多，分工越來越細。
這邊只提供C++的書單，難易程度位於程式設計師生涯第一年的程度。主要原因是我只有這種程度。次要原因是C++花樣很多。C++是一個實驗性語言，一直在添加新想法。雖然作為營生工具算是挺痛苦的，但是拿來開開眼界還是挺不賴的。
functional programming language
Programming Languages: Functional Programming Formosan Summer School on Logic, Language, and Computation Structure and Interpretation of Computer Programs https://zhuanlan.zhihu.com/p/24648375 https://en.wikipedia.org/wiki/Domain_theory
如果你喜歡函數式程式語言，別錯過台灣中研院的研習營。
Haskell、Clojure、Scala是知名的函數式程式語言。C++、Rust、JavaScript包山包海，可以做到函數式編程。
logic programming language
Foundations of Logic Programming Introduction to Logic Programming
Prolog是知名的邏輯式程式語言。我一點興趣都沒有。
automated reasoning🚧
書籍、講義
Logic in Computer Science: modelling and reasoning about systems
https://web.stanford.edu/class/cs227/ https://lfcps.org/course/constlog-schedule.html https://www.amazon.science/blog/a-gentle-introduction-to-automated-reasoning https://symbolaris.com/
我不打算整理。我只找了資源，各位請自便。
automated reasoning
自動推理。四個主題，由易到難。
satisfiability checking：判斷邏輯敘述是否可以為真（是否恆假）。 proof verification：判斷邏輯推論是否正確（是否有效／可衍生）。 theorem proving：給定前提、結論，找到衍生過程。 logical reasoning：找到前提、結論、衍生過程。
satisfiability problem（SAT）
http://www.satlive.org/ https://sat-smt.codes/ http://www.cs.man.ac.uk/~korovink/ https://homepage.iis.sinica.edu.tw/~bywang/courses/comp-logic/
給定邏輯敘述，判斷是否可以為真（判斷是否恆假）。
簡易解法：interpretation。
進階解法：邏輯敘述改寫成CNF，觀察每個括號是否皆真。
大家編寫程式進行檢查，稱作SAT solver。這個網站整理了一份詳細列表：
conjunctive normal form（CNF）
CNF是一種格式：變數適度加上¬，括號裡面全是∨，括號之間全是∧，括號只有一層。
例如(p∨¬q)∧(q)∧(¬q∨¬r∨¬s)∧(r∨s)。
變數適度加上¬稱作「字面值literal」。
例如p、¬q、q、¬q、¬r、¬s、r、s是字面值。
括號稱作「子句clause」。
例如(p∨¬q)、(q)、(¬q∨¬r∨¬s)、(r∨s)是子句。
CNF容易判斷真假：每個子句皆是真，那麼整體是真。子句裡面任何一個字面值是真，那麼子句是真。
CNF容易設計演算法。
邏輯敘述總是可以改寫成CNF
一、移除→、↔。改寫成¬、∧、∨。
例如p→q換成¬p∨q。
例如p↔q換成(p∧q)∨(¬p∧¬q)。
二、笛摩根定律：移除括號附帶的¬。
例如¬(p∧q)換成¬p∨¬q。
三、分配律：移除括號之間的∨。
例如(p∧q)∨(r∧s)換成(p∨(r∧s))∧(q∨(r∧s))再換成(p∨r)∧(p∨s)∧(q∨r)∧(q∨s)。
四、雙反律：移除變數附帶的多餘¬。
例如¬¬p換成p。
例如¬¬¬q換成¬q。
k-SAT
SAT有個重要特例是k-SAT：CNF括號裡面至多k個字面值。
k=1擁有一次方時間演算法，手法是檢查x和¬x是否同時出現。k=2擁有一次方時間演算法，手法是化作圖論問題。k≥3是NP-complete問題，只有指數時間演算法，手法是回溯法。
現實應用，k都很大，基本無望。然而大家依舊努力改良演算法，盡可能減少計算時間。詳情請見TAOCP 4B。
resolution
「檢查兩個子句是真」精簡成「檢查一個子句是真」。
p∨r , q∨¬r ⊨ p∨q
p₁∨...∨pₙ∨r , q₁∨...∨qₘ∨¬r ⊨ p₁∨...∨pₙ∨q₁∨...∨qₘ
講一下思路。當前提為真，以r和¬r為主角，分成兩種情況。一、如果r真，那麼q真。二、如果¬r真，那麼p真。也就是說，p q至少有一個是真。
延伸閱讀：semantic tableaux
樹狀圖。遇到∧：分配律共催落去。遇到∨：分支。
如果你不喜歡CNF，那麼可以用這個方法。
p∧(p∨¬q)
| ⊙ open
(p∧p)∨(q∨p) × close
/ \
(p∧p) (q∨p)
⊙ ×
satisfiability modulo theories（SMT）
SMT是SAT加強版本。援引集合、追加函數。
大家編寫程式進行檢查，稱作SMT solver。知名工具Z3。維基百科整理了一份詳細列表：
proof verification
給定邏輯推論，判斷是否有效。
解法：將邏輯推論改寫成邏輯敘述，利用SAT解決。
邏輯推論無效，只有一種情況：前提是真、結論是假。
前提不改變、結論追加¬，兩者∧起來，形成邏輯敘述。敘述可以為真，推論無效。敘述是恆假句，推論有效。
verify p₁ , p₂ , ... , pₙ ⊨ q if p₁ ∧ p₂ ∧ ... ∧ pₙ ∧ ¬q can be ⊤, then p₁ , p₂ , ... , pₙ ⊨ q is invalid. if p₁ ∧ p₂ ∧ ... ∧ pₙ ∧ ¬q is always ⊥, then p₁ , p₂ , ... , pₙ ⊨ q is valid.
theorem proving
https://tpchina.github.io/readings/ http://www.cs.ru.nl/~herman/ https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html http://www.inf.ed.ac.uk/teaching/courses/ar/
http://logitext.mit.edu/ https://www.tptp.org/CASC/
簡易解法：規則表變成圖，利用狀態空間搜尋找到衍生過程。
進階解法：規則表變成自動機，利用自動機遍歷找到衍生過程。
大家編寫程式進行檢查，稱作theorem prover。知名工具Coq、Isabelle、Lean、ACL2。維基百科整理了一份詳細列表：
reasoning
大家編寫程式進行檢查，稱作reasoning system。目前沒有知名工具。維基百科整理了一份詳細列表：
formal verification🚧
書籍、講義
Principles of Model Checking Model Checking Systems and Software Verification: Model-Checking Techniques and Tools
https://im.ntu.edu.tw/~tsay/dokuwiki/doku.php?id=courses:ssv2022:main https://www.cs.cmu.edu/~15414/
Formosan Summer School on Logic, Language, and Computation SRI: Summer School on Formal Techniques
我不打算整理。我只找了資源，各位請自便。
formal verification
https://www.cis.upenn.edu/~stevez/vellvm/ https://nfm2022.caltech.edu/ Formal Verification: An Essential Toolkit for Modern VLSI Design
形式驗證。模擬驗算。
形式formal是一個形容詞，意思是在架空世界建立規律。
現實世界的詞彙，開頭冠上formal，便得到架空世界的詞彙。例如形式科學、形式證明、形式謬誤、形式驗證、形式語言、……。
工程當中，創新事物，改造現實。想要檢查創新事物是否合理，那就建立一個架空世界，令創新事物媒合虛擬規則，改為檢查虛擬規則是否合理。
計算機工程當中，編譯器領域的LLVM、網路領域的加密演算法，使用了形式驗證。至於電子、航太、金融、製造、醫療，我只有聽說似乎有在使用，詳情我就不清楚了。
設計規則，然後又設計規則以驗證這些規則，乍看自討苦吃。然而這些領域一旦犯錯，將會消耗巨大成本，甚至消耗人命。而驗證成本相對較少。即便是看似無謂的苦工，也值得一做再做。
model checking = theorem proving
https://www.cs.cornell.edu/courses/cs6480/2020sp/schedule/ http://spinroot.com/cs118/ https://saw.galois.com/
https://www.prismmodelchecker.org/ https://www.stormchecker.org/about.html
模型檢測。
利用邏輯學進行形式驗證。創新事物改寫成邏輯敘述、邏輯推論。檢查邏輯敘述是否恆假、邏輯推論是否無效。
大家編寫程式進行檢查，稱作model checker。已有各式各樣的工具，用於各式各樣的用途。例如Infer和TLA+用來檢查程式運作（編寫程式碼檢查程式碼）、Spin用來檢查多執行緒軟體、SAW用來檢查加密演算法。維基百科整理了一份詳細列表：
temporal logic🚧
temporal logic
https://en.wikipedia.org/wiki/Linear_temporal_logic https://en.wikipedia.org/wiki/Büchi_automaton https://en.wikipedia.org/wiki/Computation_tree_logic https://5nizza.github.io/2016/08/11/ctl-to-haa/