What is the definition of the term "substitution" in the Scala Language Specification?

Question

In the Scala Language Specs (version 2.9 - June 11, 2014), in the section about existential types the term "substitution" is used, however, the meaning of substitution does not seem to be defined in the Scala Language Specification.

Could someone explain what substitution means in this context ?

Does it mean that a type variable in a type expression is substituted with an other concrete type or type variable or type constructor ?

If the substitution is meant to be a concrete type, then what is concrete types are considered? The ones which are in scope as a simple name ?

What would be a meaningful definition for the concept "substitution" in this context ?

What is being substituted with what ?

Answer 1

It refers to the substitution concept of lambda-calculus. From a practical point of view, it is a replacement of free variables with bounded ones. For a more formal definition, you can look at the theory of lambda calculus.