Is it possible to compute whether two functions are extensional equal?

Question

If you have two functions implementing a different sorting algorithm, is it then possible to infer by source code that they both have the same external properties? Meaning that they both will have a possible unsorted sequence as their input and have a sorted sequence as their output? In what way could these external properties be determined by the source code? And how would you describe these external properties? What notation would be used?

The external properties could be made known by defining them explicitly, for example within a type system, but I am wondering whether this could be done implicitly. Or is it somehow theoretically impossible to infer this kind of semantics? I am interested in whether this is possible for arbitrary functions, not just for sorting algorithms, assuming things like functions will always halt and have no side-effects.

Should I look at denotational semantics, or is unrelated?

I'm interested in pointers to research in this area and to different terms used to describe the subject that might help my literature search.

Answer 1

Yes. If you can verify that they are the same, then so can a computer.

Here's a quick specification for an integer sort in 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).

A specification can be directly encoded into the declaration of sort using dependent types.

For this particular problem, John Darlington demonstrated in the 70s that 6 families of sorting algorithms can be derived by mechanically transforming the specification of a sort into an implementation; I believe this goes under the name "semantics-based program derivation."

In the software-engineering world, finding extensionally equivalent functions is known as "semantic clone detection."

Dave Clarke also gave a good answer to this question on the CS StackExchange: https://cs.stackexchange.com/questions/2059/how-do-you-check-if-two-algorithms-return-the-same-result-for-any-input

This all falls under the umbrellas of formal methods and programming languages. Denotational semantics are one class of techniques for modeling semantics, but they've fallen out of favor for being difficult to use compared to operational semantics.

Answer 2

Extensional equality in Turing complete programming languages is undecidable in general, but that shouldn't stop you from being able to verify or falsify that any two specific functions are extensionally equal.

Verification can proceed in many forms, you could for example reason in ZFC set-theory using the operational semantics. However, that would be painful. If denotational semantics exist, they could also be used, but good denotational semantics exist only for a few languages. Usually one uses program logics, e.g. Hoare logic, for showing the extensional equality of programs. In order to be able to do this, Hoare logics for languages with functions typically require an axiom stating that $f = g \Leftrightarrow \forall x^{\alpha}. f(x) = g(x)$, assuming that $f$ and $g$ are functions of type $\alpha \rightarrow \beta$ (details of the axiom variy with the details of the chosen approach to Hoare logics).

Answer 3

A quick answer (I admit I did not spent much time...) Rice theorem says that for any non trivial question, it is undecidable to say wether the function computed by a program will have the property or not. Therefore the question here is undecidable