判定程序（decision procedure）

判定程序是一套「總會結束、而且總會把是非題答對」的作法。想像一位仔細的收銀員：你拿任何商品來，他都掃描、查資料庫，然後告訴你「有貨」或「沒貨」——而且從不在掃描到一半時當機，也不會中途走神跑掉。重要的兩項美德是：它對每個輸入都會停止，而且給出的答案是對的。一個正確但可能永遠跑下去的程序不是判定程序；一個總會停止卻有時說謊的程序也不是。

扣回形式模型：語言 L 的判定程序，恰好就是一台作為 L 的判定器（decider）的圖靈機——對每個輸入都停機，接受 L 的成員、拒絕非成員。所以「L 有判定程序」「L 可判定」「L 是遞迴的」是同一件事的三個名字。當我們用白話虛擬碼描述一個演算法並論證它不可能迴圈（例如，因為每一步都讓某個有限量縮小、而它不可能降到零以下），我們就是在展示一個判定程序，即使沒有畫出任何圖靈機。

這個詞會反覆出現，是因為這個領域大多數有用的結果都長成這個樣子：「某某問題有判定程序」（它在演算法上很溫馴），或「某某問題沒有判定程序」（它不可判定）。例如，兩台 DFA 是否等價有判定程序；兩個上下文無關文法是否等價則沒有。確立「判定程序存在」，正是讓你有資格說「電腦能對每一個情形可靠地了結這個問題」的依據。