为什么行为亚型不可判定？

Question

Liskov在这方面的工作主要集中在行为子类型上，除了本文讨论的类型系统安全性外，还要求子类型保留某些契约中的超级类型所保证的所有不变量，3.这种子类型的定义通常是不可判定的，因此不能由类型检查器来验证。

来自：http://www.wikiwand.com/en/Subtyping#/Function_类型

Answer 1

让操作o ( T类型)的合同对所有输入停止。现在决定子类型o的操作S <: T是否满足这个契约:您刚刚解决了停止问题。

更普遍地说，S::o必须计算与T::o相同的函数，如果是S <: T的话。判定两个程序是否计算相同的函数称为函数问题，相当于解决停止问题。

通常，静态地决定任何非平凡的运行时属性几乎总是等同于停止问题。

Answer 2

因为几乎每一个关于程序行为的问题都是无法确定的。通过赖斯定理，表格中的任何决策问题：

一些程序计算具有此属性的函数，另一些程序计算不具有此属性的函数。给定程序P，由P计算的函数是否具有上述性质？

是无法判定的。因此，例如，不能总是区分计算输入平方的代码和不计算输入平方的代码。虽然在简单的情况下，通常可以证明一个函数确实或不这样做，但是没有一个通用的过程对所有程序都有效。

几乎任何有趣的行为不变式都属于Rice定理的范畴，因为这些语句很少(如果有的话)讨论方法内部的样子，只讨论它返回的内容，以及它对某些输入造成的副作用。