可计算性
可计算性理论明确了在理论上可计算的函数应具有的特征。那些定义在自然数集上的、理论上可计算的函数通常被称为部分递归函数。概念中强调“理论上可计算”，是因为某些可计算函数在实际计算中可能会耗费相当长的计算时间，可能在我们宇宙现存时间内都无法完成其计算。
直观地说，如果存在一段程序来计算一个函数，那么这个函数就是可计算的。更明确地说，如果对于函数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著冯建华等译 清华大学出版社