¿Por qué el subtipo conductual es indecidible?

12

El trabajo de Liskov en esta área se centró en el subtipo de comportamiento, que además de la seguridad del sistema de tipos discutido en este artículo también requiere que los subtipos preserven todos los invariantes garantizados por los supertipos en algún contrato. [3] Esta definición de subtipo es generalmente indecidible, por lo que no puede ser verificada por un verificador de tipo.

De: http://www.wikiwand.com/en/Subtyping#/Function_types

type-systems subtypes q126y
fuente

Respuestas:

24

Deje que el contrato de operación ode Tipo Tsea ​​que se detenga para todas las entradas. Ahora decida si la operación odel subtipo S <: Tsatisface ese contrato: acaba de resolver el problema de detención .

Más generalmente, S::odebe calcular la misma función que T::osi S <: T. Decidir si dos programas computan la misma función se llama Problema de función y es equivalente a resolver el Problema de detención.

En general, decidir estáticamente cualquier propiedad de tiempo de ejecución no trivial es casi siempre equivalente al problema de detención.

Jörg W Mittag
fuente
3
Esa última línea lo clava. En el momento en que desea probar una propiedad sobre lo que el programa podría hacer en un entorno de comportamiento, está entrando en lo imposible. La razón por la que funcionan los sistemas de tipos y las herramientas de análisis estático es que tratan un lenguaje diferente (de los tipos del programa, del alcance de las variables en el programa, etc.) y no las propiedades de cómo se ejecuta el programa directamente.
Benjamin Gruenbaum
55
La respuesta de @BenjaminGruenbaum Jorg y su comentario son correctos, pero hay una sutileza que me gustaría aclarar. A menudo es posible probar una propiedad sobre un programa específico . Simplemente no hay un algoritmo que pueda seguir ciegamente que funcione para todos los programas. Considere este método escrito en Java: BigInteger sum(int[] arr) { BigInteger sum = BigInteger.ZERO; for (int x: arr) sum = sum.add(BigInteger.valueOf(x)); return sum; }no es difícil demostrar que un método en particular siempre devuelve la suma de los elementos de una matriz entera y no hace nada más (siempre que el argumento no sea nulo).
Doval
1
Y cuando no es equivalente al problema de detención, a menudo es aún peor . Porque lo imposible ya no era lo suficientemente difícil.
user2357112 es compatible con Monica el
2
O para expresar el punto de Doval de otra manera (contundente), esta es precisamente la razón por la cual los idiomas completos que no son Turing son interesantes y útiles. A menudo no necesita la integridad de Turing (ciertamente a nivel de módulo) para un trabajo real.
Leushenko
@Doval: Muy buen punto. Si bien es cierto que no puede tener un algoritmo que pruebe la terminación y / o la corrección de un programa aleatorio, es posible escribir programas de tal manera que pueda probar su corrección.
Giorgio
12

Porque casi todas las preguntas sobre el comportamiento de los programas son indecidibles. Según el teorema de Rice , cualquier problema de decisión de la forma:

Algunos programas calculan funciones que tienen esta propiedad, otros programas calculan funciones que no tienen esta propiedad. Dado un programa P, ¿la función calculada por P tiene la propiedad mencionada o no?

Es indecidible. Entonces, por ejemplo, no siempre se puede distinguir el código que calcula el cuadrado de una entrada del código que no lo hace. Aunque en casos simples, a menudo es posible demostrar que una función lo hace o no, no existe un procedimiento general que funcione para todos los programas.

Casi cualquier invariante conductual interesante cae dentro del teorema de Rice, ya que esas afirmaciones rara vez (si alguna vez) hablan sobre cómo se ve internamente el método, solo qué devuelve y qué efectos secundarios causa en respuesta a ciertas entradas.


fuente
3
Podría aclarar un poco: no es que un solo programa dado, no importa cuán patológico, pueda resistir todos los análisis, sino que, para cualquier análisis dado, existe al menos un programa que no se puede clasificar adecuadamente con eso.
Nathan Tuggy