Pourquoi le sous-typage comportemental est-il indécidable?

Les travaux de Liskov dans ce domaine se sont concentrés sur le sous-typage comportemental qui, outre la sécurité du système de types discuté dans cet article, exige également que les sous-types préservent tous les invariants garantis par les supertypes dans certains contrats. [3] Cette définition du sous-typage est généralement indécidable, elle ne peut donc pas être vérifiée par un vérificateur de type.

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

type-systems subtypes q126y
la source

Réponses:

Que le contrat de fonctionnement ode Type Tsoit qu'il s'arrête pour toutes les entrées. Décidez maintenant si le fonctionnement odu sous-type S <: Tsatisfait ce contrat: vous venez de résoudre le problème d'arrêt .

Plus généralement, S::odoit calculer la même fonction que T::osi S <: T. Décider si deux programmes calculent la même fonction s'appelle le problème de fonction et équivaut à résoudre le problème d'arrêt.

En général, la décision statique de toute propriété d'exécution non triviale équivaut presque toujours au problème d'arrêt.

Jörg W Mittag
la source

Cette dernière ligne le cloue. Au moment où vous souhaitez prouver une propriété sur ce que le programme pourrait faire dans un cadre comportemental, vous entrez dans l'impossible. La raison pour laquelle les systèmes de types et les outils d'analyse statique fonctionnent est qu'ils traitent un langage différent (des types du programme, de la portée des variables dans le programme, etc.) et non des propriétés de la façon dont le programme s'exécute directement.

Benjamin Gruenbaum

@BenjaminGruenbaum Jorg et votre commentaire sont corrects mais il y a une subtilité à clarifier. Il est souvent possible de prouver une propriété sur un programme spécifique . Il n'y a tout simplement pas d'algorithme que vous pouvez suivre aveuglément qui fonctionnera pour tous les programmes. Considérez cette méthode écrite en Java:

BigInteger sum(int[] arr) { BigInteger sum = BigInteger.ZERO; for (int x: arr) sum = sum.add(BigInteger.valueOf(x)); return sum; }

il n'est pas difficile de prouver qu'une méthode particulière renvoie toujours la somme des éléments d'un tableau entier et ne fait rien d'autre (à condition que l'argument ne soit pas nul).

Doval

Et quand ce n'est pas équivalent au problème d'arrêt, c'est souvent encore pire . Parce que impossible n'était pas déjà assez difficile.

user2357112 prend en charge Monica

Ou pour mettre le point de Doval d'une autre manière (brutale), c'est précisément pourquoi les langages complets non- Turing sont intéressants et utiles. Souvent, vous n'avez pas besoin de l'intégralité de Turing (certainement au niveau d'un module) pour un vrai travail.

Leushenko

@Doval: Très bon point. S'il est vrai que vous ne pouvez pas avoir d'algorithme qui prouve la terminaison et / ou l'exactitude d'un programme aléatoire, il est possible d'écrire des programmes de manière à pouvoir prouver leur exactitude.

Giorgio

Parce que presque toutes les questions sur le comportement des programmes sont indécidables. Par le théorème de Rice , tout problème de décision de la forme:

Certains programmes calculent des fonctions qui ont cette propriété, d'autres programmes calculent des fonctions qui n'ont pas cette propriété. Étant donné un programme P, la fonction calculée par P a-t-elle la propriété susmentionnée ou non?

est indécidable. Ainsi, par exemple, vous ne pouvez pas toujours distinguer le code qui calcule le carré d'une entrée du code qui ne le fait pas. Bien que dans des cas simples, il soit souvent possible de prouver qu'une fonction le fait ou non, il n'y a pas de procédure générale qui fonctionne pour tous les programmes.

Presque tout invariant comportemental intéressant relève du théorème de Rice, car ces déclarations parlent rarement (voire jamais) de ce à quoi ressemble la méthode en interne, uniquement de ce qu'elle renvoie et des effets secondaires qu'elle provoque en réponse à certaines entrées.

la source

Vous pourriez clarifier un peu: ce n'est pas qu'un seul programme donné, aussi pathologique soit-il, puisse résister à toutes les analyses, mais que, pour une analyse donnée, il existe au moins un programme qui ne peut pas être correctement classé avec cela.

Nathan Tuggy