計算理論有一些子領域，像是自動推論領域，探討的就是如何利用電腦證明數學定理。(Prove mathematical theorem using computer)，但是這個問題其實不像我們想像的那麼狹窄，廣義的來看，自動推論問題其實就是在探究如何利用電腦解決問題 (Computer-based problem solving)。
\begin{align} \forall x \forall y \forall z\quad x*(y*z) = (x*y)*z \\ \end{align}
\begin{align} A_1 & ... & A_n => P_1 & ... & P_n \end{align}
在自動推論中，經常使用某些公理系統，作為推論的基本法則，這些公理系統必須具備「一致性」(consistent)，不能有邏輯矛盾的情況出現。計算機科學家必須研究如何利用這些公理証明所有可證明的定理，這幾乎就是在研究電腦能力的極限了。
Theoretical computer science
1. what can be computed
2. Given a problem, how much resource do we need to compute it ?
Automatic deduction
Narrative : Prove mathematical theorem using computer.
Broad : Computer-based problem solving.
Why ?
xyz x*(y*z) = (x*y)*z
x y x * y = y
x y y*x = e (x y (x * y = y & y z z*y = x))
A1&…&An => P1&…&Pn
Algorithm
Given input with property x, Output a solution with property y.
x p(x) => z q(x, z)
p(x) : input specification.
q(x,z) : output specification
Middle exclusive :
P | -P => true // doesn't carry any information.
Godel incomplete theorem :
Any theory that contains formal number theory is either incomplete or inconsistent.
(N, 0, succ, +, *, >, =)
Well-founded
N*N : (0,0) < (0,1) < (0,2) …< (1,0) < (1,1) < …< (2,0) < …
If we use a algorithm to enumerate from (0,0) to (2,0), it may fall into infinite loop.
If we use a algorithm to enumerate from (2,0) to (0,0), it always terminate.
Mathematical Induction
f(0), x f(x) => f(x+1) x f(x)
Q: How to express the problem ? A: Language-syntax
Q: How to manipulate the expression A: Proof Theory
(How to produce a proof ? ) (Axioms + inference rule)
Q: How to find the goal soon ? A: search plan
(which inference rule to apply ?)
Notion of truth => model theory => semantics
Language + model theory = logic
Programming language + interpreter (compiler) = algorithm
Given a proof theory,
It should be
sound : it only proves "true" thing
complete : it can prove everything that's true.
Computer => Efficient
Most proving search time is undecidable, so we cannot compare which one
is more efficient .
The search complexity for propositional logic is co-NP complete.
History :
1900: Hilbert : 23 problem.
1929: Pressberg complete theorem :(N, +, 0, S, >) can be mechanismed.
1933: Godel incomplete theorem :(N, 0, S, +, *, >) cannot be mechanized.
1933-1936 :
Turing : Turing Machine :
Kleene : Recursive function.
Church : lambda-calculus
Markov :
Post :
無限大的意義
所謂的無限大（∞），並不是一個數，而是一種辯證法，因此、認為 ∞ 沒有意義，
是指 ∞ 這個數是沒有意義的，而非 ∞ 這個辯證法是沒有意義的。
所謂一集合的cardinality是countable infinite, 是指在 ∞ 這個辯證法底下，該集合可以被
enumerate，而所謂一集合的cardinality是uncountable infinite, 是指在 ∞ 這個辯證法底下，
該集合可以被辯證出無法被enumerate。
因此、所有N的 subset 所成的集合F(N) 是uncountable infinite是指F(N)可被辯證出是可以
enumerate（和N 1-1 onto mapping），所有N的countable infinite subset 所成的集合
C(N)是countable infinite，是指C(N) 被被辯證出可和N 1-1 onto mapping.
∞ 辯證法：對於任意一個數x, 必然可以找到另一個數y, 使y>x and y in N, 則N這個set的
cardinality |N| = ∞。
xy(N(x)&N(y)&y>x)=>|N| = ∞
Finite state automata :
M = (K, Σ, δ, S, F)
K : set of state
Σ: finite set of input symbol
s : s in K, initial state
δ: (K*Σt*Σs)->K * Σ*
F : F in K, final state set
regular expression :
A->wB, A->w
Pumping lemma for regular expression
if z in L and |z| >= n, we may write z = uvw
1. |v| >= 1
2. |uv| <= n
3. i uviw in L
Theorem : L(Finite state automata) = L(Regular expression)
Push down automata
M = (K, Σi, Σs, δ, s, F)
K : set of state
Σi: finite set of input symbol
Σs: finite set of stack symbol
s : s in K, initial state
δ: (K * Σi * Σs)-> K * Σ*
F : F in K, final state set
Context free grammar :
G = (V,T,P,S)
A->α, αin (V∪T)*
Pumping lemma for context free grammar :
if z in L and |z| >= n, we may write z = uvwxy
1. |vx| >= 1
2. |vwx| <= n
3. i uviwxiy in L
Turing Machine (TM)
M = (K,Σ,δ,S)
K : set of state
Σ: finite set of symbol
s : s in K, initial state
δ: (K*Σ)->(K∪{h,”yes”,”no”})* Σ*(←,—,→)
example : A TM that decide plaindromes
plaindromes (迴文) : 正讀倒讀都一樣的 word。
K Σ δ
s 0 (q0 ,> ,→) s :start,q0:上次讀的bit為0.
s 1 (q1 ,> ,→) q1: 上次讀的bit為1.
s > (s ,> ,→) 寫上一個 >
s _ (yes,_ ,—)
q0 0 (q0 ,0 ,→) q0:移到最後一個bit “_”
q0 1 (q0 ,1 ,→)
q0 _ (q0’,_ ,←)
q1 0 (q1 ,0 ,←) q1:移到最後一個bit “_”
q1 1 (q1 ,1 ,←)
q1 _ (q1’,_ ,←)
q0’ 0 (q ,_ ,←) q0’: 看看是否為0
q0’ 1 (no ,1 ,—)
q0’ > (yes,_ ,→)
q1’ 0 (no ,1 ,—) q1’: 看看是否為1
q1’ 1 (q ,_ ,←)
q1’ > (yes,> ,→)
q 0 (q ,0 ,←) q : 回到開頭，繼續檢查下一個。
q 1 (q ,1 ,←)
q > (s ,> ,→)
Unrestricted Grammar
α->β
Theorem : L(Turing Machine) = L(Unrestricted Grammar)
L(Turing Machine) = L(First Order Logic)
Church-Turing Thesis :
“Computable function” can be identified with the class of partial recursive functions.
Closure Property :
A class of languages is closed under a particular operatio.
Example :
intersection : L1∩L2
union : L1∪L2
concatenation : L1L2
Kleene operator : L1*
Post preview:
Close preview