可計算性
可計算性理論明確了在理論上可計算的函數應具有的特征。那些定義在自然數集上的、理論上可計算的函數通常被稱為部分遞歸函數。概念中強調“理論上可計算”，是因為某些可計算函數在實際計算中可能會耗費相當長的計算時間，可能在我們宇宙現存時間內都無法完成其計算。
直觀地說，如果存在一段程序來計算一個函數，那么這個函數就是可計算的。更明確地說，如果對於函數f: A -> B存在一個算法，以任意x∈A作為輸入，都可以得到y = f(x)作為輸出，則這個函數是可計算的。
在20世紀30年代，普林斯頓大學的Alonzo Church提出了一個重要的原理，稱為Church理論。Church理論是關於數學定義和真實計算之間的關系的，該理論認為任何通用計算設備都能夠計算定義在整數集上的一個函數集。這個函數集就是部分遞歸函數的集合，有時也稱為可計算函數集。在數學上有對這類函數的定義，在計算機科學中有兩個等價的定義，分別是圖靈機和lambda演算。圖靈機由一個無限長的磁帶、一個磁帶讀/寫頭和一個有限狀態控制器組成。在每一步計算中，圖靈機從磁帶上讀出一個符號，並由有限狀態控制器決定是否在當前磁帶區上寫入不同的符號，然后決定是否需要將磁帶讀/寫頭向前或向后移動一位。Lambda演算有三個部分：一個用於定義函數的符號、一個用於證明表達式等價的證明系統以及一組被稱為歸約的演算規則集合。Lambda演算系統通過歸約的方式，將函數應用於一個或多個參數，並且計算出結果。Church在闡明他的理論時所引用的一個證據就是圖靈機與lambda演算是等價的。
停機問題
有可計算的函數，當然也就有不可計算的函數。一個著名的例子就是停機問題。為了簡化問題，這里我們將一個程序也作為數據對象來處理，並且能夠作為某個程序的輸入。如果P是一個程序，x是程序的輸入，則P(x)為該程序的輸出。
停機問題就是指：給定一個只需要一個輸入的程序P，以及一個對象x，確定程序P在以x作為輸入時是否會停機。
停機問題的可不判定性是指停機問題是不可計算的。下面我們給出停機問題的不可判定性的證明。
證明：
第一步，假設停機問題是可計算的，並且將停機問題實現為程序Halt。程序Halt有兩個輸入，第一個輸入是一個程序對象P，第二個輸入是一個對象x。程序Halt的行為如下：
Halt(P,x) = if P(x)停機 then 輸出"halts" else 輸出"does not halt"
也就是說，如果程序P以對象x作為輸入是能夠停機的，則程序Halt輸出字符串“halts”；否則，程序Halt輸出字符串“does not halt”。其中重要的一點是對於任何P和x，Halt(P , x)都會停機。
第二步，通過程序Halt，我們可以構造一個程序Try，它只接受一個輸入對象P，並且有可能該程序不能停機。程序Try定義如下：
Try(P) = if Halt(P , P) = halts then 始終運行 else 停機
也就是說，如果Halt(P , P)輸出字符串“halts”，即P(P)停機，則程序Try會無限運行下去；否則，程序Try就停機。
第三步，讓我們思考程序Try以自身作為輸入的情況，即Try(Try)是否會停機的問題。如果Try(Try)能夠停機，則Halt(Try , Try)將會輸出字符串“halts”，那么根據程序Try的定義，程序Try(Try)將始終運行，不停機；而如果Try(Try)不停機，則Halt(Try , Try)將輸出字符串“does not halt”，則根據程序Try的定義，得知Try(Try)將會停機。於是，出現了矛盾。
第四步，由第一步的假設推出了第三步的矛盾，也就是第一步的假設不正確，所以，停機問題是不可計算的。
證明完畢。
正是由於停機問題的不可判定性，程序的某些特性是無法實現確定的，程序設計語言的實現在檢查程序錯誤時不可能報告程序是否會停機，例如無法確定一些循環是否會停止，是否會出現無限遞歸的情況等等。
參考《程序設計語言概念》 John C. Mitchell著馮建華等譯 清華大學出版社