# What is the property of a PL that extracting a subroutine should not change the meaning?

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.

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

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.