如果某条规则的前提里出现了一个结论里看不到、子项也算不出的类型，照着规则写函数就走不通，函数不知道该填什么。函数类型的规则就是典型例子：给 $𝜆𝑥.𝑡$（记号见 [附注] 求值策略、归约策略与合流性 ）定型时，参数 $𝑥$ 的类型在项里找不到。那时规则仍然定义了一个清清楚楚的关系，但从关系到算法的那一步，需要额外的设计和额外的证明。 [定义] 类型与类型判断 的布尔值／自然数语言足够小，避开了这个问题；但区分“规则”和“算法”、并分别证明可靠与完备的习惯，在更大的语言里同样适用。