[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Issue: SUBTYPEP-TOO-VAGUE (Version 4)
- To: cl-cleanup@sail.stanford.edu
- Subject: Issue: SUBTYPEP-TOO-VAGUE (Version 4)
- From: Jon L White <jonl@lucid.com>
- Date: Thu, 3 Nov 88 13:31:15 PST
- Cc: eb@lucid.com, jlm@lucid.com, jeb@lucid.com, fy@lucid.com
- In-reply-to: KMP's message of Thu, 13 Oct 88 19:28 EDT
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 --