Czy można obliczyć, czy dwie funkcje są równe ekstensywne?

Jeśli masz dwie funkcje implementujące inny algorytm sortowania, to czy można na podstawie kodu źródłowego wnioskować, że obie mają takie same właściwości zewnętrzne? Czy to znaczy, że oboje będą mieć możliwą nieposortowaną sekwencję jako dane wejściowe i posortowaną sekwencję jako dane wyjściowe? W jaki sposób te właściwości zewnętrzne mogą być określone przez kod źródłowy? A jak opisałbyś te właściwości zewnętrzne? Jaka notacja zostanie zastosowana?

Zewnętrzne właściwości można podać, definiując je jawnie, na przykład w systemie typów, ale zastanawiam się, czy można to zrobić niejawnie. Czy też teoretycznie niemożliwe jest wnioskowanie o tego rodzaju semantyce? Interesuje mnie, czy jest to możliwe w przypadku dowolnych funkcji, a nie tylko algorytmów sortowania, zakładając, że takie funkcje jak zawsze będą się zatrzymywać i nie będą miały żadnych skutków ubocznych.

Czy powinienem patrzeć na semantykę denotacyjną, czy też nie jest ze sobą powiązany?

Interesują mnie wskaźniki do badań w tej dziedzinie oraz różne terminy używane do opisania tematu, które mogą pomóc w wyszukiwaniu literatury.

Tak. Jeśli możesz sprawdzić, czy są one takie same, komputer może to zrobić.

Oto krótka specyfikacja sortowania liczb całkowitych w 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).

Specyfikacja może być bezpośrednio zakodowana w deklaracji sortowania przy użyciu typów zależnych.

W przypadku tego konkretnego problemu John Darlington wykazał w latach 70., że 6 rodzin algorytmów sortowania można uzyskać poprzez mechaniczne przekształcenie specyfikacji rodzaju w implementację; Uważam, że pod nazwą „pochodna programu oparta na semantyce”.

W świecie inżynierii oprogramowania znalezienie dodatkowych równoważnych funkcji jest znane jako „wykrywanie klonów semantycznych”.

Dave Clarke udzielił również dobrej odpowiedzi na to pytanie w CS StackExchange: /cs/2059/how-do-you-check-if-two-algorithms-return-the-same-result -dla dowolnego wejścia

Wszystko to należy do metod formalnych i języków programowania . Semantyka denotacyjna to jedna z klas technik modelowania semantyki, ale popadła w niełaskę, ponieważ jest trudna w użyciu w porównaniu do semantyki operacyjnej.

Ekstensywna równość w kompletnych językach programowania Turinga jest w ogólności nierozstrzygalna, ale nie powinno to powstrzymywać cię przed możliwością weryfikacji lub sfałszowania, czy dowolne dwie konkretne funkcje są w równym stopniu rozszerzone.

Weryfikacja może przebiegać w wielu formach, na przykład można uzasadnić teorię zbiorów ZFC za pomocą semantyki operacyjnej. Byłoby to jednak bolesne. Jeśli istnieje semantyka denotacyjna, można jej również użyć, ale dobra semantyka denotacyjna istnieje tylko dla kilku języków. Zwykle używa się logiki programu, np. Logiki Hoare'a , do pokazania ekstensywnej równości programów. Aby to zrobić, logika Hoare'a dla języków z funkcjami zazwyczaj wymaga aksjomatu, który to określa$f = g \Leftrightarrow \forall x^{\alpha}. f(x) = g(x)$, przy założeniu, że $f$ i $g$ są funkcjami typu $\alpha \rightarrow \beta$ (szczegóły wariantu aksjomat ze szczegółami wybranego podejścia do logiki Hoare'a).

Szybka odpowiedź (przyznaję, że nie spędziłem dużo czasu ...) Twierdzenie Rice'a mówi, że w przypadku każdego nietrywialnego pytania nierozstrzygalne jest stwierdzenie, czy funkcja obliczona przez program będzie miała właściwość, czy nie. Dlatego pytanie tutaj jest nierozstrzygalne