理論電腦科學

理論電腦科學lei5 leon6 din6 nou5 fo1 hok6（英文：theoretical computer science），或者叫電腦理論din6 nou5 lei5 leon6，係電腦科學當中最抽象化嘅子領域。

理論電腦科學嘗試了解運算呢樣嘢嘅數學性質，會用數學上用嘅方法－數學證明等－嚟搵出描述運算嘅定理。理論電腦科學純粹以增進人類對運算嘅了解為目的，所以係一個好理論化嘅領域，但理論電腦科學上嘅進步往往會引致按呢啲知識嚟設計嘅電腦能夠做更有效率嘅運算。

運算理論

運算理論（theory of computation）專門研究運算嘅本質，思考機械點樣用演算法（algorithm）解難，嘗試了解運算機械嘅能力同極限係乜。運算理論上嘅研究會用數學證明等嘅數學方法，思考

唔同種類嘅理論性運算機械喺解難能力上有乜嘢差異（自動機理論；automata theory）；
有啲乜嘢問題係能夠或者唔能夠用運算機械解嘅（可運算性理論；computability theory）；以及
一個運算上嘅問題最高嘅可能解決效率（運算複雜性理論；computational complexity theory）

... 等等嘅問題^[1]^[2]。

舉個例說明，停機問題（halting problem）就係可運算性理論上嘅一個經典問題：

例子：停機問題證明

首先，電腦程式可以分做兩大種^[3]：

例：while (true) continue；呢種程式唔會停機－部電腦一行呢個程式就會一路行落去，永世唔會停。

例：print "Hello, world!"；呢種程式會停機－部電腦會逐行逐行碼行咗佢，最後停低。

根據英國數學家亞倫圖靈（Alan Turing）嘅證明，呢個世界冇可能有電腦能夠攞一個程式嘅碼做輸入，再俾出正確嘅「呢段碼會唔會停機」輸出。個證明大致上係噉^[4]：

想像有個程式，halts(f)，如果 f 係一個會停機嘅子程序，halts(f) 會出「真」（1），否則halts(f) 會出「假」（0），再想像以下呢個程序：

def g(): # 定義 g
    if halts(g): # 如果 halt(g) 係真...
        loop_forever() # 做永遠唔停嘅 loop

呢個程序會引致一個大矛盾：如果 g() 係會停機嘅，噉 halts(g) 會出「真」，於是 g() 就會進入永遠係噉行（loop_forever）嘅狀態－出現矛盾；而如果 g() 係唔會停機嘅，噉 halts(g) 會出「假」，於是 g() 就唔會進入永遠係噉行（loop_forever）嘅狀態－又出現矛盾。因為噉，halts(f) 呢一個程式冇可能存在喺呢個世界上。

呢個證明對運算本質嘅了解作出咗貢獻，而且由頭到尾淨係用數學證明嘅做法^[4]^[5]。

		P = NP?
自動機理論	可運算性理論	運算複雜性理論	演算法	量子電腦

數據結構

數據結構（data structure）係指一部電腦組織內部數據嘅方法：要做運算，部電腦就實要用某啲方法儲住要用嘅數據，例：要做到將兩個數值加埋一齊，部電腦首先要能夠記住嗰兩個數值；好似陣列（array）噉，就係一種常用嘅數據結構，所有主流程式語言都有陳述式俾用家製造陣列，一個陣列有一個整數表示佢嘅大細，個整數表示個陣列有幾多個元素（element），每個元素都有個由 0 起始嘅數字表示佢係個陣列嘅第幾個元素，例：有個陣列叫 thearray，噉 thearray[0] 就係指 thearray 嘅第一個元素。數據結構上嘅研究思考部電腦以乜嘢方法儲住啲數據，以及唔同嘅儲數據方法有乜嘢優缺點，分別喺乜嘢時候啱用^[6]^[7]。

一個陣列；呢個陣列每一格都裝咗個字母，每一格上面嗰個整數表示嗰個元素係個陣列嘅第幾格。

資訊理論

資訊理論（information theory）係一個研究資訊要點樣量化、儲起同傳達嘅數學理論。資訊理論嘅核心概念係熵（entropy）^[8]；資訊理論當中嘅「熵」係一個指標，用嚟量度一個有隨機性喺入面嘅變數或者過程當中帶有幾多不確定性（uncertainty）喺入面。舉個例說明，想像家吓掟一個銀仔同擲一粒六面嘅骰仔，假設個銀仔同粒骰仔係冇出千嘅：掟一個銀仔有 2 個可能結果，而擲一粒六面骰有 6 個可能結果。擲骰仔當中有更多可能性喺度，所以不確定性亦都更加大－有更多嘅資訊熵；當一個人知道咗一次掟銀仔或者擲骰仔嘅結果嗰陣，佢會清楚知道結果－資訊熵變成 0。對比兩個情況，「話俾人知掟銀仔嘅結果」所俾到嘅資訊－消除嘅資訊熵－少過「話俾人知擲骰仔嘅結果」所俾嘅。由呢個例子可見，資訊理論做到將「資訊」呢個本來相當含糊嘅概念量化，令資訊成為一個喺科學上可以被研究嘅對象^[9]^[10]。

$S=-\sum _{i}p_{i}\log _{2}(p_{i})$	$\mathbb {E} _{X,Y}[SI(x,y)]$
資訊熵	相互資訊

形式化方法

形式化方法（formal methods）泛指一啲用嚟描述、開發同驗證軟件同硬件系統嘅數學方法。呢啲方法會用數學模型描述軟件同硬件系統，幫分析者手分析個系統，例：個電腦系統嘅運算速度（ ${\text{sp}}$ ）有條公式表示個速度受邊啲因素（ $x_{i}$ ）影響， ${\text{sp}}=\beta _{1}x_{1}+...$ ；分析者只要知道嗰啲因素嘅數值，佢就可以用條公式計出個電腦系統嘅運算速度；所以有咗條公式，佢就有得計出啲因素要喺乜嘢數值，先可以令速度最大化；喺呢點上，電腦科學同第啲工程學領域一樣－用數學模型模擬一個系統，並且靠呢啲模型對系統嘅設計作出思考，最後設計出更加能夠幫設計者達到佢目的嘅系統。形式化方法好多時會用到運算理論、資訊理論同程式語言理論上嘅知識，而且可以話係軟件工程嘅理論基礎^[11]^[12]。

睇埋

電腦科學

攷

↑ Sipser, M. (2006). Introduction to the Theory of Computation (Vol. 2). Boston: Thomson Course Technology.
↑ Lewis, H. R., & Papadimitriou, C. H. (1997). Elements of the Theory of Computation. Prentice Hall PTR.
↑ Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics. 58 (58): 345–363.
↑ ^4.0 ^4.1 Alan Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, Volume 42 (1937), pp 230–265.
↑ Davis, Martin (1965). The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. New York: Raven Press.. Turing's paper is #3 in this volume. Papers include those by Godel, Church, Rosser, Kleene, and Post.
↑ Black, Paul E. (15 December 2004). "Data structure". In Pieterse, Vreda; Black, Paul E. (eds.). Dictionary of Algorithms and Data Structures. National Institute of Standards and Technology.
↑ Peter Brass, Advanced Data Structures, Cambridge University Press, (2008).
↑ Demystifying Entropy. Towards Data Science.
↑ Delgado-Bonal, Alfonso; Martín-Torres, Javier (2016-11-03). "Human vision is determined based on information theory". Scientific Reports. 6 (1).
↑ Huelsenbeck, J. P.; Ronquist, F.; Nielsen, R.; Bollback, J. P. (2001). "Bayesian inference of phylogeny and its impact on evolutionary biology". Science. 294 (5550): 2310–2314.
↑ Phillip A. Laplante, 2010. Encyclopedia of Software Engineering Three-Volume Set (Print). CRC Press. p. 309.
↑ Hall, A. (1990). Seven myths of formal methods. IEEE software, 7(5), 11-19.

拎

SIGACT directory of additional theory links.
Theory Matters Wiki Theoretical Computer Science (TCS) Advocacy Wiki.
List of academic conferences in the area of theoretical computer science.
Theoretical Computer Science - StackExchange.
Computer Science Animated.

[1] Sipser, M. (2006). Introduction to the Theory of Computation (Vol. 2). Boston: Thomson Course Technology.

[2] Lewis, H. R., & Papadimitriou, C. H. (1997). Elements of the Theory of Computation. Prentice Hall PTR.

[3] Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics. 58 (58): 345–363.

[turing1937-4] 4.0 ^4.1 Alan Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, Volume 42 (1937), pp 230–265.

[5] Davis, Martin (1965). The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. New York: Raven Press.. Turing's paper is #3 in this volume. Papers include those by Godel, Church, Rosser, Kleene, and Post.

[6] Black, Paul E. (15 December 2004). "Data structure". In Pieterse, Vreda; Black, Paul E. (eds.). Dictionary of Algorithms and Data Structures. National Institute of Standards and Technology.

[7] Peter Brass, Advanced Data Structures, Cambridge University Press, (2008).

[entropy-8] Demystifying Entropy. Towards Data Science.

[9] Delgado-Bonal, Alfonso; Martín-Torres, Javier (2016-11-03). "Human vision is determined based on information theory". Scientific Reports. 6 (1).

[10] Huelsenbeck, J. P.; Ronquist, F.; Nielsen, R.; Bollback, J. P. (2001). "Bayesian inference of phylogeny and its impact on evolutionary biology". Science. 294 (5550): 2310–2314.

[11] Phillip A. Laplante, 2010. Encyclopedia of Software Engineering Three-Volume Set (Print). CRC Press. p. 309.

[12] Hall, A. (1990). Seven myths of formal methods. IEEE software, 7(5), 11-19.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]