Does the concept of subtype require dynamic method binding? https://en.wikipedia.org/wiki/Subtyping says


  In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype.


In the concept of "subtype", when explaining "substitutability" as "program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype", does it assume/require dynamic method binding (e.g. the one specified as virtual functions in C++)?

Specifically, given a type B with a method m(), a function

void f(B b){
    b.m();
}


and a subtype S of B which redefines m() method,  which does S being a subtype of B according to the meaning of "substitutability" in the wikipedia article mean:


either if calling f() with an instance s of S, then b.m() in f() will invoke S.m() instead of invoking B.m(), (this case   requires dynamic method binding.)
or if replace B with S in the definition of f(), 

void f(S s){
    S.m();
}


still work, i.e. f() can operate with both B and S, i.e. "subtype" only requires  thatS also has a method m() with the same signature as B.m()? (This case doesn't require dynamic method binding.)


Thanks.
No. It doesn't even require a notion of "method" at all. Even if you have objects and methods, it doesn't necessarily require a notion of dynamic dispatch. Indeed, dynamic dispatch is only relevant if you can "override" methods (where, here, I'm [atypically] including implementing an interface as "overriding" [abstract] methods).

All subtyping states is if $t$ is a term of type $S$ then $t$ is also a term of type $T$ if $S\operatorname{\mathtt{&lt;:}}T$. There are a variety of ways to implement this. For structural subtyping, usually the idea is that the sub-type is representationally compatible with the super-type so that their common interface literally refers to the same code. For example, if the 3-tuple $(A,B,C)$ is represented by contiguously storing a representation of $A$, $B$, and $C$, and similarly for a 2-tuple, then a 3-tuple literally is a 2-tuple that just happens to have a representation of $C$ following it. This is represented by $(A,B,C)\operatorname{\mathtt{&lt;:}}(A,B)$. As another example, a sum/variant type $A+B+C$ could be represented as a tag indicating the variant and a representation of $A$, $B$, or $C$ as appropriate. If the tags are compatible, then a value of type $A+B$ literally is a value of $A+B+C$ leading to $A+B\operatorname{\mathtt{&lt;:}}A+B+C$. Something like dynamic dispatch could be used internally to avoid relying on representational compatibility if desired by the language implementer.

Another approach would be to have subtyping imply the implicit insertion of coercions from sub-types to super-types. Dynamic dispatch is just completely irrelevant to subtyping in this context.

Common object oriented languages tend to conflate subtyping and subclassing, but they are fairly different concepts. Many (most?) programming languages that have some degree of "subtyping" fail to satisfy various notions of "substitutability", so the baseline is usually just that using a sub-type as a super-type typechecks and (usually) doesn't crash. (Even that low bar fails to be met by e.g. Java and C# and certainly C++.)

You could have a language that supports dynamic dispatch which doesn't have a notion of subtyping. For example, conversions to "super-types" could be explicit.