[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Issue: SUBTYPEP-TOO-VAGUE (Version 4)



Kent's notes summarizing the discussion at Fairfax were:

    X3J13 meeting:

     JonL: Thinks EB can prove that only SATISFIES mucks things up and
	   that OR, AND, etc. are safe.

     RWK: It couldn't be. You'd need more type cleanups before it could be.

     People generally doubted JonL's claim but said he was of course welcome
     to submit the proof.

Eric (EB) had intended to submit the "proof", but didn't send it out
before leaving for vacation.  In recent discussion here at Lucid, he,
Jim MacDonald, Jim Boyce, Frank Yellin and I were convinced of the "proof".

Before hinting at how the "proof" goes, I'll remark that RWK's claim is 
only partly true -- in the current state, an algorithm can easily be devised
for each implementation, once it is determined how that implementation
treats the disjointness of the primitive types on CLtL pp.33-35., and how 
it determines whether or not something is a defstruct name.  But in fact a
portable algorithm can be adduced if we added STRUCTURE-TYPE-P to the
language and if we required every implementation to follow a reasonable 
set of disjointness constraints. [It might also be necessary to add
UPGRADED-{ARRAY-ELEMENT,COMPLEX-PART}-TYPE.]

The "thumbnail" sketch of the proof goes like this.  First, completely
exclude SATISFIES; also, temporarily ignore type compositions using
AND, OR, and NOT.  Then, there is only a finite number of basic primitive 
types (CLtL, p.43); and there are only a few very simple rules for 
constructing more primitive types from them -- namely, numeric subranges,
array "specializations", and defstructs without the :type option.  Now,
considering the truly primitive types as "literals" in a propositional 
calculus language with AND/OR/NOT, one can produce a disjunctive normal 
form; thus type-equivalence and subtypeing are completely determined.  It 
doesn't matter that there is a infinite pool of "literals" -- in any given 
subtypep query, there will only be finitely many present; exactly the same 
situation is covered in college-level logic courses that talk about the 
decidibility of the propositional calculus.

Of course, an efficient implementation wouldn't follow such a "blind"
course, which might be NP-complete; one could do a lot better in the 
average cases.

Additionally, by my own previously set rules for such proposals, it would 
seem that Lucid (or somebody else) ought to go ahead and do the full 
non-satisfies SUBTYPEP first, before trying to impress it into the standard.


-- JonL --