Is it possible to compute whether two functions are extensional equal? 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.
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 =&gt; true
    |  (cons x nil) =&gt; true
    |  (cons x (cons y r)) =&gt; if x &lt;= 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.