From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,29d8139471e3f53e X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Preventing type extensions Date: Fri, 24 Sep 2010 20:47:28 +0300 Organization: Tidorum Ltd Message-ID: <8g46hgFkfqU1@mid.individual.net> References: <87iq2bfenl.fsf@mid.deneb.enyo.de> <874odv9npv.fsf@ludovic-brenta.org> <87y6b7cedd.fsf@mid.deneb.enyo.de> <66a3704c-54f9-4f04-8860-aa12f516134b@t3g2000vbb.googlegroups.com> <87d3sib44t.fsf@mid.deneb.enyo.de> <134q4k2ly2pf4$.17nlv1q6q5ivo.dlg@40tude.net> <4c8dec8e$0$6990$9b4e6d93@newsspool4.arcor-online.net> <8f6cceFrv2U1@mid.individual.net> <135a7dc9-3943-45e4-884b-3cc6bce3db0a@q18g2000vbm.googlegroups.com> <10rutrnp4yp1b$.vxcbtginicg9.dlg@40tude.net> <1rwwxbzfj78eh.6l7isp9fciba$.dlg@40tude.net> <4c98e745$0$7667$9b4e6d93@newsspool1.arcor-online.net> <1qwl6jiun2mik$.s1k2xnzg8dv6$.dlg@40tude.net> <8g3nflFnruU1@mid.individual.net> <9d1804mxit9j$.wyo5zgwjxh71.dlg@40tude.net> Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net REeEiMM1dREg9KAslRccPQ2VtdfApLzWZeUjdkbICiQiiHsZKC Cancel-Lock: sha1:L088FAtI8i13rSmvNRoLKZICT7o= User-Agent: Mozilla-Thunderbird 2.0.0.24 (X11/20100328) In-Reply-To: <9d1804mxit9j$.wyo5zgwjxh71.dlg@40tude.net> Xref: g2news1.google.com comp.lang.ada:14241 Date: 2010-09-24T20:47:28+03:00 List-Id: Dmitry A. Kazakov wrote: > On Fri, 24 Sep 2010 16:30:29 +0300, Niklas Holsti wrote: > >> Dmitry A. Kazakov wrote: >>> On Tue, 21 Sep 2010 19:11:33 +0200, Georg Bauhaus wrote: >>> >>>> On 21.09.10 18:25, Dmitry A. Kazakov wrote: >>>> >>>>> horse /= animal >>>> It will help immensely, I think, at least those of us who do >>>> not do type theory on an every day basis, if we had a glossary >>>> of terms for interpreting expression like "horse /= animal". >>> Gosh, it was no more than just this: if horse is an animal that does not >>> imply they are interchangeable. Compare: "all horses have hoofs" and "all >>> animals have hoofs." >>> >>> is-a /= is >>> member /= set >>> >>> Moreover: >>> >>> is-a /= substitutable (greeting to the LSP!) >>> >>> Compare: "some animals have tentacles" and "some horses have tentacles." >> Those are not properties of "horses" and "animals", but properties of >> the *set* of horses and the *set* of animals. > > horses is set of horses. Incomprehensible. What do you mean? >> The property "all horses have hooves" expresses a universal property of >> horses: if X is a horse, then X has hooves. The statement "some horses >> have tentacles" says nothing about any given horse X. > > Both are predicates: No, they are formulas. "has_hooves(X)" is a predicate that can be true or false for a given object X. > forall x in horses, x has hooves That is a universally ("forall") quantified formula that uses the predicate has_hooves. The LSP "properties" are implicitly universally quantified. To quote http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-156.ps, with implicit quantification inserted in [] by me: "/Subtype Requirement/: Let phi(x) be a property provable about [all] objects x of type T. Then phi(y) should be true for [all] objects of type S where S is a subtype of T." The following paragraph makes universal quantification clearer: "We focus on two kinds of properties, /invariants/, which are properties true of all states, and /history properties/ which are properties true of all sequences of states." > exists x in animals, x has tentacles So far as I understand LSP, existentially quantified formulas are not considered. Continuing the quote above: "We do not address other kinds of safety properties of computations, e.g. the existence of an object in a state,...". > [ if you dropped existential quantification, you would not be able to > describe functions returning values ] I don't think the LSP model of computation tries to, or needs to, describe functions in that sense; it uses postconditions which simply assume the existence of a return value and state properties of all possible return values. By the way, note the inclusion of "history properties" in the LSP, this is an important point that (I think) has been ignored in this discussion. For example, in order to show that the class of Squares is not an LSP subtype of the class of Rectangles one must use history properties and consider what happens when the program changes the width of a Square, seen as a Rectangle, without also changing the height to the same new value. A consequence is that LSP depends not only on the static properties of objects (has_hooves) but also on the set of "mutating" operations. If we were to define a Rectangle class that did not allow independent setting of width and height, but only a uniform size scaling, Squares would be an LSP subtype of these Rectangles. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .