1
$\begingroup$

What is the name of the property of a Programming Language that says that extracting a subprogram into a subroutine and using that subroutine instead of the subprogram should not change the meaning of the program?

I could swear that this exists and that it has a well-known name, but I can't for the life of me remember it. My efforts to search for the name have been thwarted by being swamped with results for the Liskov Substitution Principle or Referential Transparency.

What I am looking for is the property that I should be able to replace

printf("Hello");

with

void hello() {
    printf("Hello");
}

hello(); 

without changing the meaning of the program.

I think it is named after the person who coined it, but I am not sure. Something like XYZ Equivalence or XYZ Principle where XYZ is the name of a well-known Computer Scientist. I want to say Strachey, but I couldn't find a mention of anything similar in Fundamental Concepts in Programming Languages.

$\endgroup$
4
  • $\begingroup$ Isn’t it definition of subroutine rather than PL’s property? $\endgroup$ Commented Jan 10, 2020 at 10:46
  • 1
    $\begingroup$ Compositionality? $\endgroup$ Commented Jan 10, 2020 at 14:23
  • $\begingroup$ Instead of "extracting a subroutine", you can look at the reverse direction of this notion: "definition unfolding". It says that the meaning of a program does not change if you replace a name with the body of its definition. It is one of the reduction rules for extended variants of lambda calculus. It is rarely mentioned though, and it is hard to find its formal definition. $\endgroup$
    – beroal
    Commented Feb 26, 2020 at 18:03
  • $\begingroup$ Err... correctness? :-) $\endgroup$ Commented Mar 9, 2021 at 20:53

2 Answers 2

2
$\begingroup$

I believe you are looking for Morris style Contextual Equivalence. Which says that the meaning of a term (in your case a subroutine) should not change in any context.

If, $⟦ \cdot ⟧ : term \to \mathcal{D}$, is the meaning function then $$\forall C. ⟦C[t]⟧ = ⟦ C ⟧ \circ ⟦ t ⟧ $$ Where $C[\cdot]$ is a context with a hole in it.

$\endgroup$
1
$\begingroup$

Purely by accident, I found the answer to my question as well as the fact that my question is wrong.

What I was thinking of was Tennent's Correspondence Principle, which I read about in the context of Java Lambdas and today re-discovered in the context of do-expressions for ECMAScript.

foo

should be equivalent to

(fn { foo })()

for any expression foo, i.e. that I can wrap an expression in a closure without changing the meaning of the expression.

Except it turns out that this is not the Principle of Correspondence, it was misquoted by Neal Gafter and seems to have taken on a life of its own after that.

This is actually the Principle of Qualification.

The actual Principle of Correspondence talks about variable definitions and function parameters and says that for every mechanism of parameters, there should be an equivalent mechanism of definitions and vice-versa. The example he gives is the following Pascal block:

var i : integer;
begin
  i := -j;
  write(i)
end

which is equivalent to the following procedure and vice versa:

procedure p(i : integer);
  begin
    write(i)
  end;

begin
  p(-j)
end

And he points out that there is no mechanism for variable definitions that is equivalent to var parameters (i.e. pass-by-reference) in Pascal, meaning that Pascal does not obey the Principle of Correspondence.

References:

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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