Tractability Proof System:可解性證書、正常形逃逸與 clocked enumeration

重要校正:對任意圖靈機程式碼判斷是否多項式時間執行確實一般不可判定,但這不阻止建立一個外延完備(extensionally complete)的 P 正常形語言——Cobham 的 bounded recursion 與 Bellantoni-Cook 的 safe recursion 早已給出這種語法即保證多項式的經典刻畫。區分三種完備性:機器索引完備性(太強,不可判定)、證明完備性、外延正常形完備性(已有成熟理論)。等號隊因此不必再對任意 SAT solver 逐一證明多項式,可以直接在「屬於這個語法就保證多項式」的正常形語言裡構造 SAT;若成功,直接得到 P=NP。不等號隊的對稱任務是找一個被初始函數、composition、safe recursion 全部保存、但 SAT characteristic function 違反的語義不變量(Grammar Invariant Program)。同時建立 clocked Turing machine 作為第二個有效正常形,為下一輪的對角化鋪路。