9
$\begingroup$

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.

|cite|improve this question
$\endgroup$
8
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Thanks for the answer! This is exactly what I was searching for. $\endgroup$ – Matthijs Steen Oct 31 '12 at 11:28
  • 4
    $\begingroup$ I strongly disagree with the statatement that denotational semantics have "fallen out of favor". That depends largely on whom you ask. $\endgroup$ – Andrej Bauer Nov 3 '12 at 4:11
5
$\begingroup$

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).

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Thanks for the answer. I will look into Hoare logic. Are denotational semantics hard to define compared to Hoare logic, or is it just less suitable for most languages? Is extensional equality undecidable in general because of the Halting Problem? Then if functions were to always halt, like in total functional languages, wouldn't it be decidable in general? Or are there other reasons for being undecidable in general? $\endgroup$ – Matthijs Steen Oct 31 '12 at 18:04
  • $\begingroup$ @ Matthijs Steen: Good denotational semantics for programming languages with interesting features seem to be hard to come by. Hoare logic in contrast has blossomed in the last decade, and we can construct them for just about any programming language now. Extensional equality is undecidable because (simplifying a bit) otherwise you could check if an arbitrary program $P$ is contextually equivalent to $0$, the always terminating program, which is a variant of the halting problem. If you throw enough finiteness conditions on a language you'll eventually end up with something that ... (cont.) $\endgroup$ – Martin Berger Nov 2 '12 at 12:04
  • $\begingroup$ ... has a decidable contextual equality. But note that R. Loader showed that even finitary PCF has an undecidable contextual equivalence. $\endgroup$ – Martin Berger Nov 2 '12 at 12:05
-2
$\begingroup$

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

|cite|improve this answer
$\endgroup$
  • 1
    $\begingroup$ Does it not state that "... for any non-trivial property of partial functions ...", so would it not be possibly be decidable for total functions? $\endgroup$ – Matthijs Steen Oct 30 '12 at 21:35

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.