Undecidability of Liskov Substitution Principle

On 26 Mar 2007 02:08:51 -0700, Mark Nicholls wrote:

> On 25 Mar, 16:56, "Dmitry A. Kazakov" <mail...{}dmitry-kazakov.de>
> wrote:

>> It is imprecise. Actually [absolute] LSP-conformity is a sufficient but not
>> necessary condition of substitutability.
>
> Can you clarify....what do you mean by "absolute"....(I tend to use it
> to mean effectively behaviourally indistinguishable...but I don't
> think you mean this.)

I meant "absolute" = in any possible legal program.

> Can you give an example of something that does not satisfy LSP but is
> substitutable....I'm not picking holes....it's an interesting
> subject....and I know it's at the mercy of everyone using the same
> words to mean something slightly different.

2 + 2.

Assuming: "+" is an operation of the type Integer. 2 is a constant of an
immutable subtype of Integer. Clearly, constant Integer is not an
LSP-subtype of the Integer type. Yet 2 is perfectly substitutable in
addition. You don't need to re-write 2+2 as:

X : Integer := 2;
Y : Integer := 2;

X + Y -- Here X and Y are of Integer [mutable]

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

On 26 Mar, 10:39, "Dmitry A. Kazakov" <mail...{}dmitry-kazakov.de>
wrote:
> On 26 Mar 2007 02:08:51 -0700, Mark Nicholls wrote:
>
> > On 25 Mar, 16:56, "Dmitry A. Kazakov" <mail...{}dmitry-kazakov.de>
> > wrote:
> >> It is imprecise. Actually [absolute] LSP-conformity is a sufficient but not
> >> necessary condition of substitutability.
>
> > Can you clarify....what do you mean by "absolute"....(I tend to use it
> > to mean effectively behaviourally indistinguishable...but I don't
> > think you mean this.)
>
> I meant "absolute" = in any possible legal program.

OK

>
> > Can you give an example of something that does not satisfy LSP but is
> > substitutable....I'm not picking holes....it's an interesting
> > subject....and I know it's at the mercy of everyone using the same
> > words to mean something slightly different.
>
> 2 + 2.
>
> Assuming: "+" is an operation of the type Integer. 2 is a constant of an
> immutable subtype of Integer. Clearly, constant Integer is not an
> LSP-subtype of the Integer type. Yet 2 is perfectly substitutable in
> addition. You don't need to re-write 2+2 as:

hmmmm....mutability is always a difficult example......my brain works
largely in immutable semantics.

It depends how you've set your types up.

Clearly '+' is thus a member of an ('implicit') type that is a
supertype of integer.

i.e. by specifying 'int' when you only need '+' is over specification.

So OK...I think I buy what you're saying....the example is not LSP
compliant wrt to the explicit type specification (but it is LSP
compliant to the implicit type specification).

Does that add up for you?

>
> X : Integer := 2;
> Y : Integer := 2;
>
> X + Y -- Here X and Y are of Integer [mutable]
>

On Mar 21, 8:46 pm, 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")

Your summary is wrong.

Evaluating types for Liskov/Wing subtyping is highly trivial, and not
error-prone
at all. The evaluation can be done statically (proof tools) or
dynamically (Design
by Contract execution etc).

What is "highly non-trivial and error-prone" is the (in)ability of the
great
majority of s/w developers to precisely define the semantics of their
programs
(pre/post/invariant conditions etc) such that an evaluation can be
attempted.

Similarly "highly non-trivial" is the limit on current proof tools to
execute
proofs of a certain complexity in reasonable times (although AFAIK
those limits
are far from basic) .

Regarding the cited article and undecidability, general evaluation of
Liskov/Wing
subtype conformance is indeed undecidable.

However, given that in the near 20 years I have been working in
industry (telecoms
primarily) , I have yet to define types with semantics akin to
Russells' Paradox or
the Halting problem. Have you ??

Therefore undecidability in practical terms is irrelevant. It is IMHO
only a reminder
to those ignorant enough to make particular claims regarding the power
and ability
of particular tools.

Finally, after yet another perennial comp.object hash by one and all
to explain
even the most basic concepts of the inheritance + substitutabilty +
Liskov/Wing
subtyping relationship :

<BluePeter demo = "here's one I made earlier" >

http://groups.google.com/group/comp....f843524b98522b

</BluePeter>


Regards,
Steven Perryman

On 26 Mar, 11:05, ggro...{}bigfoot.com wrote:
> On Mar 21, 8:46 pm, 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")

long time no talk.

>
> Your summary is wrong.
>
> Evaluating types for Liskov/Wing subtyping is highly trivial, and not
> error-prone
> at all. The evaluation can be done statically (proof tools) or
> dynamically (Design
> by Contract execution etc).

you claim it to be trivial then below accept it to being
undecidable....?

>
> What is "highly non-trivial and error-prone" is the (in)ability of the
> great
> majority of s/w developers to precisely define the semantics of their
> programs
> (pre/post/invariant conditions etc) such that an evaluation can be
> attempted.

I completely agree.

>
> Similarly "highly non-trivial" is the limit on current proof tools to
> execute
> proofs of a certain complexity in reasonable times (although AFAIK
> those limits
> are far from basic) .

They are unbounded in general....but in most constrained OO
environments they should be bounded.

>
> Regarding the cited article and undecidability, general evaluation of
> Liskov/Wing
> subtype conformance is indeed undecidable.

slightly confused with respect to the opening remarks.

>
> However, given that in the near 20 years I have been working in
> industry (telecoms
> primarily) , I have yet to define types with semantics akin to
> Russells' Paradox or
> the Halting problem. Have you ??

I agree again but the compiler doesn't know that....so the compiler
designer doesn't know that.

(I'm not sure about the example of Russels paradox....but lets leave
it)

>
> Therefore undecidability in practical terms is irrelevant.

Is it?

> It is IMHO
> only a reminder
> to those ignorant enough to make particular claims regarding the power
> and ability
> of particular tools.
>

Thank you.

> Finally, after yet another perennial comp.object hash by one and all
> to explain
> even the most basic concepts of the inheritance + substitutabilty +
> Liskov/Wing
> subtyping relationship :
>

Thank you again.

> <BluePeter demo = "here's one I made earlier" >
>
> http://groups.google.com/group/comp....d/thread/f612f...
>
> </BluePeter>
>
> Regards,
> Steven Perryman

On 26 Mar, 11:05, ggro...{}bigfoot.com wrote:
> On Mar 21, 8:46 pm, 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")
>
> Your summary is wrong.
>
> Evaluating types for Liskov/Wing subtyping is highly trivial, and not
> error-prone
> at all. The evaluation can be done statically (proof tools) or
> dynamically (Design
> by Contract execution etc).
>
> What is "highly non-trivial and error-prone" is the (in)ability of the
> great
> majority of s/w developers to precisely define the semantics of their
> programs
> (pre/post/invariant conditions etc) such that an evaluation can be
> attempted.
>
> Similarly "highly non-trivial" is the limit on current proof tools to
> execute
> proofs of a certain complexity in reasonable times (although AFAIK
> those limits
> are far from basic) .
>
> Regarding the cited article and undecidability, general evaluation of
> Liskov/Wing
> subtype conformance is indeed undecidable.
>
> However, given that in the near 20 years I have been working in
> industry (telecoms
> primarily) , I have yet to define types with semantics akin to
> Russells' Paradox or
> the Halting problem. Have you ??

Have you ever used arithmetic?

(in fact you may not have done).

But that would (technically) be subject to the same problem.

"Dmitry A. Kazakov" <mailbox{}dmitry-kazakov.de> wrote:
> On 26 Mar 2007 02:08:51 -0700, Mark Nicholls wrote:
>
> > Can you give an example of something that does not satisfy LSP
> > but is substitutable....I'm not picking holes....it's an
> > interesting subject....and I know it's at the mercy of everyone
> > using the same words to mean something slightly different.
>
> 2 + 2.
>
> Assuming: "+" is an operation of the type Integer.

If one makes such an assumption, then one has no reason to assume that
"+" does what it does in standard mathmatics, and thus no reason to
assume that passing two immutable objects to it will work.

On Mar 26, 12:13 pm, "Mark Nicholls" <Nicholls.M...{}mtvne.com> wrote:

> On 26 Mar, 11:05, ggro...{}bigfoot.com wrote:

> > On Mar 21, 8:46 pm, 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")

> long time no talk.

Who are you talking to ?? Not me (according to netiquette) .


>> Evaluating types for Liskov/Wing subtyping is highly trivial, and not
>> error-prone at all. The evaluation can be done statically (proof tools) or
>> dynamically (Design by Contract execution etc).

> you claim it to be trivial then below accept it to being undecidable....?

You appear to equate triviality with decidability.
Last time I looked they are not the same thing.

If this is not the case, feel free to educate me beyond my point of
ignorance.


>> Similarly "highly non-trivial" is the limit on current proof tools to
>> execute proofs of a certain complexity in reasonable times (although AFAIK
>> those limits are far from basic) .

> They are unbounded in general....but in most constrained OO
> environments they should be bounded.

Define "constrained OO environment" .


>> Regarding the cited article and undecidability, general evaluation of
>> Liskov/Wing subtype conformance is indeed undecidable.

> slightly confused with respect to the opening remarks.

Probably so depending on your understanding of triviality and
decidability.


>> However, given that in the near 20 years I have been working in
>> industry (telecoms primarily) , I have yet to define types with semantics akin to
>> Russells' Paradox or the Halting problem. Have you ??

> I agree again but the compiler doesn't know that....so the compiler
> designer doesn't know that.

What the "compiler" (and its "designer" ) "knows" are moot.

A proof system is expected to give a yes/no answer to a question.

If such an answer cannot be given, it is either because of a
deficiency in the
proof system (proof complexity etc) , or because the question really
is undecidable.

Either way that system will be able to tell us what aspect of the
question it is
having problems with.


> (I'm not sure about the example of Russels paradox....but lets leave it)

No, lets' *not* leave it. Because it is the crux of theory vs
practicality.

In 20-odd years I have never written any type semantics that have not
been
able to verified either at run-time or statically by a proof tool.

Therefore in all the systems I have been involved with (which underpin
much of the
world you live in today) , things are *very much decidable*
(fortunately) .

Should you not have telecommunications in your world because
regardless of the
above, the general ability to verify the semantic correctness of a
system is
undecidable ??


>> Therefore undecidability in practical terms is irrelevant.

> Is it?

Of course.

Decidability is a theoretical concept that defines *boundaries* .
The real world gets on with pushing things to such boundaries as best
(economically etc) as possible (ie practicality) .


Regards,
Steven Perryman

On 26 Mar 2007 02:59:20 -0700, Mark Nicholls wrote:

> On 26 Mar, 10:39, "Dmitry A. Kazakov" <mail...{}dmitry-kazakov.de>
> wrote:
>>
>> 2 + 2.
>>
>> Assuming: "+" is an operation of the type Integer. 2 is a constant of an
>> immutable subtype of Integer. Clearly, constant Integer is not an
>> LSP-subtype of the Integer type. Yet 2 is perfectly substitutable in
>> addition. You don't need to re-write 2+2 as:
>
> hmmmm....mutability is always a difficult example......my brain works
> largely in immutable semantics.

It is not mutability. We should really talk about substitution of the sets
bound by universal and existential quantifiers. You cannot get rid of it
when you describe semantics of a subprogram in terms of types. Mutability
of arguments plays here little role.

> It depends how you've set your types up.

Actually no. There is a full dualism between generalization and
specialization, you can take either end, the result will be same. Think of
it in "immutable" (:-)) way: the order of types construction is irrelevant
for the relation between them. Right?

> Clearly '+' is thus a member of an ('implicit') type that is a
> supertype of integer.
>
> i.e. by specifying 'int' when you only need '+' is over specification.

Yes, but you don't know what else + relies on. You don't see it from the
contracts. That is the whole idea of types (and generally mathematical
structures). + stands for the types of its arguments. You cannot look into
it and say, no, it is not Integer, I needed only a group here. That's too
late for the object 2.

> So OK...I think I buy what you're saying....the example is not LSP
> compliant wrt to the explicit type specification (but it is LSP
> compliant to the implicit type specification).

Ah, we can always take one subprogram from a type and invent a fully
LSP-conform freak. It is a consequence of the following universal theorem:

forall P, a program, exists some semantics P fulfills.

(it is easy, if the program does not correspond to specifications, change
the latter... (:-))

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

On Mon, 26 Mar 2007 12:37:27 GMT, Daniel T. wrote:

> "Dmitry A. Kazakov" <mailbox{}dmitry-kazakov.de> wrote:
>> On 26 Mar 2007 02:08:51 -0700, Mark Nicholls wrote:
>>
>>> Can you give an example of something that does not satisfy LSP
>>> but is substitutable....I'm not picking holes....it's an
>>> interesting subject....and I know it's at the mercy of everyone
>>> using the same words to mean something slightly different.
>>
>> 2 + 2.
>>
>> Assuming: "+" is an operation of the type Integer.
>
> If one makes such an assumption, then one has no reason to assume that
> "+" does what it does in standard mathmatics, and thus no reason to
> assume that passing two immutable objects to it will work.

Yes.

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

On 26 Mar, 13:43, ggro...{}bigfoot.com wrote:
> On Mar 26, 12:13 pm, "Mark Nicholls" <Nicholls.M...{}mtvne.com> wrote:
>
> > On 26 Mar, 11:05, ggro...{}bigfoot.com wrote:
> > > On Mar 21, 8:46 pm, 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")
> > long time no talk.
>
> Who are you talking to ?? Not me (according to netiquette) .

I've spoken to you on many occasions!....or am I going mad?

>
> >> Evaluating types for Liskov/Wing subtyping is highly trivial, and not
> >> error-prone at all. The evaluation can be done statically (proof tools) or
> >> dynamically (Design by Contract execution etc).
> > you claim it to be trivial then below accept it to being undecidable....?
>
> You appear to equate triviality with decidability.
> Last time I looked they are not the same thing.
>
> If this is not the case, feel free to educate me beyond my point of
> ignorance.

no there are not, I am implying undecidable problems in the context of
computer science are more problematic than decidable ones.

>
> >> Similarly "highly non-trivial" is the limit on current proof tools to
> >> execute proofs of a certain complexity in reasonable times (although AFAIK
> >> those limits are far from basic) .
> > They are unbounded in general....but in most constrained OO
> > environments they should be bounded.
>
> Define "constrained OO environment" .

most OO environments get the programmer to inform the compiler of
substitutability issues.

class A:B....is implied to mean (in a weak sense) where you see a B
object you can use an A object...

the compiler then forces you to implement things required to satisfy
this weak condition, e.g... inheriting methods, or implementing
abstract ones.

>
> >> Regarding the cited article and undecidability, general evaluation of
> >> Liskov/Wing subtype conformance is indeed undecidable.
> > slightly confused with respect to the opening remarks.
>
> Probably so depending on your understanding of triviality and
> decidability.

OK...if it's undecidable you cannot write a program to resolve
it.....it makes writing programs problematic.

>
> >> However, given that in the near 20 years I have been working in
> >> industry (telecoms primarily) , I have yet to define types with semantics akin to
> >> Russells' Paradox or the Halting problem. Have you ??
> > I agree again but the compiler doesn't know that....so the compiler
> > designer doesn't know that.
>
> What the "compiler" (and its "designer" ) "knows" are moot.

The OP was asking about the algorithm to decide whether types
satisfied LSP.......this is the sort of question a compiler designer
asks.

>
> A proof system is expected to give a yes/no answer to a question.
>
> If such an answer cannot be given, it is either because of a
> deficiency in the
> proof system (proof complexity etc) , or because the question really
> is undecidable.

yes

>
> Either way that system will be able to tell us what aspect of the
> question it is
> having problems with.

Really!.....if it can't prove it in n minutes, does it then resort to
trying to prove whether the proof does not exists, and if it can't do
that does it then try to prove that the proof of the proof does not
exist....etc? When does it know that it knows what the problem is?

>
> > (I'm not sure about the example of Russels paradox....but lets leave it)
>
> No, lets' *not* leave it. Because it is the crux of theory vs
> practicality.

It is, but it is rather a special case, because no such model exists,
a better case would be arithmatic, we like to think of that as
'existing'.

>
> In 20-odd years I have never written any type semantics that have not
> been
> able to verified either at run-time or statically by a proof tool.

There in lies the crux.

run time, easy peasy (relatively)....proof tool...hmmmm.....more
problematic.

>
> Therefore in all the systems I have been involved with (which underpin
> much of the
> world you live in today) , things are *very much decidable*
> (fortunately) .

It is rather a philosophical aside, just because it's good enough for
the real world does not negate the logical restrictions on what is
being asked and not attempting to go further than them.

>
> Should you not have telecommunications in your world because
> regardless of the
> above, the general ability to verify the semantic correctness of a
> system is
> undecidable ??
>

No, but should one simply ignore questions of decidability on the
grounds that they haven't caused me (personally) any problems
recently.

> >> Therefore undecidability in practical terms is irrelevant.
> > Is it?
>
> Of course.

go and tell that to Whitehead and Russell.

>
> Decidability is a theoretical concept that defines *boundaries* .
> The real world gets on with pushing things to such boundaries as best
> (economically etc) as possible (ie practicality) .

It does, the practicality of the concept is not bothering trying to
push them further than those boundaries.