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$
  • $\begingroup$ Isn’t it definition of subroutine rather than PL’s property? $\endgroup$ – Dmitri Urbanowicz Jan 10 at 10:46
  • $\begingroup$ Compositionality? $\endgroup$ – Andrej Bauer Jan 10 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 Feb 26 at 18:03
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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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