Est-il possible de calculer si deux fonctions sont égales extensionnellement?

Si vous avez deux fonctions implémentant un algorithme de tri différent, est-il alors possible de déduire par code source qu'elles ont toutes les deux les mêmes propriétés externes? Cela signifie qu'ils auront tous les deux une séquence non triée possible comme entrée et une séquence triée comme sortie? De quelle manière ces propriétés externes pourraient-elles être déterminées par le code source? Et comment décririez-vous ces propriétés externes? Quelle notation serait utilisée?

Les propriétés externes pourraient être connues en les définissant explicitement, par exemple dans un système de type, mais je me demande si cela pourrait être fait implicitement. Ou est-il théoriquement impossible de déduire ce genre de sémantique? Je m'intéresse à savoir si cela est possible pour des fonctions arbitraires, pas seulement pour les algorithmes de tri, en supposant que des choses comme les fonctions s'arrêteront toujours et n'auront pas d'effets secondaires.

Dois-je regarder la sémantique dénotationnelle ou est-elle sans rapport?

Je suis intéressé par des pointeurs de recherche dans ce domaine et par différents termes utilisés pour décrire le sujet qui pourraient aider ma recherche documentaire.

Oui. Si vous pouvez vérifier qu'ils sont identiques, il en va de même pour un ordinateur.

Voici une spécification rapide pour un tri entier dans Coq:

Inductive natlist : Type :=
| nil : natlist
| cons : nat → natlist → natlist.

Fixpoint is_sorted (l : natlist ) : bool :=
    match l with
    |  nil => true
    |  (cons x nil) => true
    |  (cons x (cons y r)) => if x <= y then is_sorted (cons y r) else false
    end.

...

Theorem sort_spec : forall l, is_sorted (sort_list l).

Une spécification peut être directement encodée dans la déclaration de tri à l'aide de types dépendants.

Pour ce problème particulier, John Darlington a démontré dans les années 70 que 6 familles d'algorithmes de tri peuvent être dérivées en transformant mécaniquement la spécification d'un tri en une implémentation; Je crois que cela passe sous le nom de «dérivation de programme basée sur la sémantique».

Dans le monde de l'ingénierie logicielle, la recherche de fonctions d'extension équivalentes est connue sous le nom de «détection de clones sémantiques».

Dave Clarke a également donné une bonne réponse à cette question sur le CS StackExchange: /cs/2059/how-do-you-check-if-two-algorithms-return-the-same-result -pour-n'importe quelle entrée

Tout cela relève des parapluies des méthodes formelles et des langages de programmation . La sémantique dénotationnelle est une classe de techniques de modélisation de la sémantique, mais elle est tombée en disgrâce car elle est difficile à utiliser par rapport à la sémantique opérationnelle.

L'égalité d'extension dans les langages de programmation complets de Turing est indécidable en général, mais cela ne devrait pas vous empêcher de vérifier ou de falsifier que deux fonctions spécifiques sont égales sur le plan de l'extension.

$f = g \Leftrightarrow \forall x^{\alpha}. f(x) = g(x)$$f$$g$$\alpha \rightarrow \beta$

Une réponse rapide (j'avoue que je n'ai pas passé beaucoup de temps ...) Le théorème de Rice dit que pour toute question non triviale, il est indécidable de dire si la fonction calculée par un programme aura la propriété ou non. Par conséquent, la question ici est indécidable