Re: Proposal: 6NF

Marshall wrote:
> On Oct 15, 7:39 am, "Jan Hidders" <hidd..._at_gmail.com> wrote:
> >
> > Note that Liskov and Wong themselves defined the principle
> > as:
> >
> > Let q(x) be a property provable about objects x of type T. Then q(y)
> > should be true for objects y of type S where S is a subtype of T.
>
> Um, I'm on shaky ground here, but it seems to me that given Rice's
> theorem, you're not going to be able to use the above to prove
> a subtyping relationship; only disprove it. Am I way off?

Rice's theorem says something about decidability, not provability. But whether this is provable and / or decidable depends very much on the particular formalism you are using. Note that this is exactly what subtyping algorithms do, which in many cases are quite simple.

• Jan Hidders