Undecidability of Liskov Substitution Principle

Esdger Dijkstra allegedly said "Object-oriented programming is an
exceptionally bad idea which could only have originated in
California." :-)

I found this paper a while ago, and have been thinking about it often
in my daily programming (in C++):

http://okmij.org/ftp/Computation/Subtyping/

My summary of it would be: While the Liskov Substitution Principle can
be used to determine when a subclass is a subtype, applying the
principle is highly non-trivial and error-prone (the author says
"undecidable"). This fact leads to OO code being fragile.

I'm wondering what people thought about it (beyond cowboy coder's "I
don't care about composability or fragility")

n.torrey.pines{} wrote:

> Esdger Dijkstra allegedly said "Object-oriented programming is an
> exceptionally bad idea which could only have originated in
> California." :-)
>
> I found this paper a while ago, and have been thinking about it often
> in my daily programming (in C++):
>
> http://okmij.org/ftp/Computation/Subtyping/
>
> My summary of it would be: While the Liskov Substitution Principle can
> be used to determine when a subclass is a subtype, applying the
> principle is highly non-trivial and error-prone (the author says
> "undecidable"). This fact leads to OO code being fragile.

Nonsense. I knew where his problem was as soon as I read:

Suppose you are tasked with implementing a Set package. Your boss
defined a set as an unordered collection where each element has a
single occurrence. In fact, your boss even said that a set is a bag
with no duplicates...

If a set can't do everything a bag can do, then it can't derive from bag.

> I'm wondering what people thought about it (beyond cowboy coder's "I
> don't care about composability or fragility")

Another issue: "All base classes should be abstract." Riel wrote that
back in 1996.

On 21 Mar 2007 12:46:23 -0700, n.torrey.pines{} wrote:

> Esdger Dijkstra allegedly said "Object-oriented programming is an
> exceptionally bad idea which could only have originated in
> California." :-)

What's wrong with California? I bet the weather is great there. (:-))

> I found this paper a while ago, and have been thinking about it often
> in my daily programming (in C++):
>
> http://okmij.org/ftp/Computation/Subtyping/

[I guess this page is well known to all permanent members of comp.object.]

> My summary of it would be: While the Liskov Substitution Principle can
> be used to determine when a subclass is a subtype, applying the
> principle is highly non-trivial and error-prone (the author says
> "undecidable"). This fact leads to OO code being fragile.

That depends on how LSP is defined. If it is in terms of [decidable]
pre-/postconditions and invariants, then I don't see why it should be
undecidable. The actual problem with [absolute] LSP is that it is too
constraining to be any useful.

> I'm wondering what people thought about it (beyond cowboy coder's "I
> don't care about composability or fragility")

LSP was discussed in comp.object on countless occasions. I suggest you just
browse the archives.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

On 21 Mar, 19:46, n.torrey.pi...{} wrote:
> Esdger Dijkstra allegedly said "Object-oriented programming is an
> exceptionally bad idea which could only have originated in
> California." :-)
>
> I found this paper a while ago, and have been thinking about it often
> in my daily programming (in C++):
>
> http://okmij.org/ftp/Computation/Subtyping/
>
> My summary of it would be: While the Liskov Substitution Principle can
> be used to determine when a subclass is a subtype, applying the
> principle is highly non-trivial and error-prone (the author says
> "undecidable"). This fact leads to OO code being fragile.
>
> I'm wondering what people thought about it (beyond cowboy coder's "I
> don't care about composability or fragility")

I broadly agree it is in general undecidable....but that doesn't
render the approach futile.

The fragility is probably more due to a lack of formality rather than
the limitations of that formality.

The reason for the lack of formality is an open question, the cost in
many cases (currently) may be prohibitive.

Responding to N.torrey.pines...

> Esdger Dijkstra allegedly said "Object-oriented programming is an
> exceptionally bad idea which could only have originated in
> California." :-)
>
> I found this paper a while ago, and have been thinking about it often
> in my daily programming (in C++):
>
> http://okmij.org/ftp/Computation/Subtyping/
>
> My summary of it would be: While the Liskov Substitution Principle can
> be used to determine when a subclass is a subtype, applying the
> principle is highly non-trivial and error-prone (the author says
> "undecidable"). This fact leads to OO code being fragile.

LPS is about type substitution. Classes are not types. So the notion of
determining whether one has a subclass or a subtype using LSP seems both
undecidable and meaningless.

As far as the paper is concerned, the author postulates that a set is a
bag without duplicates. That's fine. But then the author proceeds to
provide other unrelated properties, implementation inheritance,
overloading, and whatnot for the types without regard to LSP. Then when
LSP is broken the author complains OO subtyping is fragile.

I basically agree with Daniel T.: Don't Do That! If a developer provides
implementations within an OO subtyping context it is the responsibility
of the developer to ensure LSP is satisfied. If the developer can't
ensure that for the candidate implementation then the developer has
three choices: (A) change the implementation so that LSP is satisfied;
(B) change the client contract with the supertype so that LSP is
satisfied for the implementation; or (C) provide the implementation
elsewhere (i.e., use delegation outside the subtyping tree). What the
developer can't do is throw a new implementation into the subtype and
walk away.

As far as applying LSP is concerned, one needs to distinguish between
recognizing LSP problems and resolving them. Recognizing LSP problems is
a matter of DbC contracts with the supertype. If those are properly
defined it is usually fairly easy to determine if a candidate
implementation violates them. (Though properly defining those contracts
can be a tad tedious.)

The tricky part is fixing a candidate implementation when it does not
satisfy LSP. LSP is a very strong constraint so it is often not possible
to satisfy it with a given implementation (i.e., (A) above is not
feasible). That, however, does not make OO development fragile. Quite
the contrary, the strength of the constraint ensures OO applications
will be robust because one can't use the wrong tool for the job in hand.


*************
There is nothing wrong with me that could
not be cured by a capful of Drano.

H. S. Lahman
hsl{}pathfindermda.com
Pathfinder Solutions
http://www.pathfindermda.com
blog: http://pathfinderpeople.blogs.com/hslahman
"Model-Based Translation: The Next Step in Agile Development". Email
info{}pathfindermda.com for your copy.
Pathfinder is hiring:
http://www.pathfindermda.com/about_us/careers_pos3.php.
(888)OOA-PATH

"H. S. Lahman" <h.lahman{}verizon.net> wrote:

> As far as applying LSP is concerned, one needs to distinguish between
> recognizing LSP problems and resolving them. Recognizing LSP problems is
> a matter of DbC contracts with the supertype. If those are properly
> defined it is usually fairly easy to determine if a candidate
> implementation violates them. (Though properly defining those contracts
> can be a tad tedious.)

Funny that some people are claiming that LSP is undecidable, while
others (HS and I) are saying that it is not only decidable, but rather
easy. Hell, in Eiffel, the system itself helps check that LSP is
satisfied. It can't be that hard to do if a computer can do it.

On Thu, 22 Mar 2007 20:21:41 GMT, Daniel T. wrote:

> "H. S. Lahman" <h.lahman{}verizon.net> wrote:
>
>> As far as applying LSP is concerned, one needs to distinguish between
>> recognizing LSP problems and resolving them. Recognizing LSP problems is
>> a matter of DbC contracts with the supertype. If those are properly
>> defined it is usually fairly easy to determine if a candidate
>> implementation violates them. (Though properly defining those contracts
>> can be a tad tedious.)
>
> Funny that some people are claiming that LSP is undecidable, while
> others (HS and I) are saying that it is not only decidable, but rather
> easy. Hell, in Eiffel, the system itself helps check that LSP is
> satisfied. It can't be that hard to do if a computer can do it.

Because people have different definitions in mind. Substitutability is
undecidable, I guess, and LSP in the form such that LSP-conform =>
substitutable will be as well. Weaker forms of LSP can be decidable at the
cost of loosing the implication above (or by reducing LSP-conform to an
empty set). The most interesting forms of weak LSP, such that would loose
substitutability anywhere but in the program of interest could again be
undecidable.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

On Mar 22, 1:21 pm, "Daniel T." <danie...{}earthlink.net> wrote:
> "H. S. Lahman" <h.lah...{}verizon.net> wrote:
>
> > As far as applying LSP is concerned, one needs to distinguish between
> > recognizing LSP problems and resolving them. Recognizing LSP problems is
> > a matter of DbC contracts with the supertype. If those are properly
> > defined it is usually fairly easy to determine if a candidate
> > implementation violates them. (Though properly defining those contracts
> > can be a tad tedious.)
>
> Funny that some people are claiming that LSP is undecidable, while
> others (HS and I) are saying that it is not only decidable, but rather
> easy. Hell, in Eiffel, the system itself helps check that LSP is
> satisfied. It can't be that hard to do if a computer can do it.

The article says LSP is undecidable (although I didn't see any formal
proof - the author probably thinks it's self-evident). Assuming that
it is undecidable, this does not mean that you can never show the
subtyping relation or lack thereof, just that there does not exist a
general procedure that can be used to determine the subtyping.

Since you and H.S. say that this problem is decidable, I'd be curious
as to the general, always terminating procedure for solving the
subtype-or-not problem :-)

I suspect that what you mean is along the lines: "Termination is also
undecidable, but that does not prevent us from writing programs that
provably terminate". I would agree with such an opinion. However, I
believe most OO code contains nothing resembling such a proof, whereas
termination is typically obvious.

P.S. I didn't know about Eiffel's proof assistant - I'll look into
this. Thanks.

On 21 Mar 2007 12:46:23 -0700, n.torrey.pines{} wrote:

>Esdger Dijkstra allegedly said "Object-oriented programming is an
>exceptionally bad idea which could only have originated in
>California." :-)

http://en.wikipedia.org/wiki/Simula

Sweden.

>I found this paper a while ago, and have been thinking about it often
>in my daily programming (in C++):
>
>http://okmij.org/ftp/Computation/Subtyping/
>
>My summary of it would be: While the Liskov Substitution Principle can
>be used to determine when a subclass is a subtype, applying the
>principle is highly non-trivial and error-prone (the author says
>"undecidable"). This fact leads to OO code being fragile.

Computation is undecidable, shall we turn them all off?

>I'm wondering what people thought about it (beyond cowboy coder's "I
>don't care about composability or fragility")

Be careful with sharp tools.

J.

Daniel T. <daniel_t{}earthlink.net> wrote:
> Funny that some people are claiming that LSP is undecidable, while
> others (HS and I) are saying that it is not only decidable, but rather
> easy. Hell, in Eiffel, the system itself helps check that LSP is
> satisfied. It can't be that hard to do if a computer can do it.

Decidability is a poor perspective from which to approach the question.

Ultimately, it is correct to say that the LSP is undecidable. The same,
though, is true of ANY property of ANY sufficiently powerful language,
so clearly there's something fishy in this analysis. What is equally
important is what is not true; as you point out, there are languages
that check conservative approximations to this constraint.
Undecidability of the problem says nothing about whether good
conservative approximations exist.

In other words, there may be some bizarre code that fails validation but
actually doesn't fail in any relevant property. If such code is
relatively rare, and there's usually an easy way to rewrite it so that
it does pass validation, then this isn't a real problem. The entire
basis of type systems in programming languages rests on this idea, in
fact: useful type systems ALWAYS prove properties of code that are
undecidable for general-purpose untyped languages. They avoid the
undecidability problem by rejecting some valid code; they are actually
solving an easier problem that conservatively approximates the property
of interest.

--
Chris Smith