- From: Dan Connolly <connolly@w3.org>
- Date: 19 Jun 2002 15:11:16 -0500
- To: "Peter F. "Patel-Schneider <pfps@research.bell-labs.com>
- Cc: www-webont-wg@w3.org
On Wed, 2002-06-19 at 13:45, Peter F. Patel-Schneider wrote: [...] > > > For example, what is the meaning of a malformed list, i.e., a list > > > 1/ where some list node does not have a rest, > > > 2/ where some list node does not have a first, > > > 3/ where some list node has two first[s], > > > 4/ where some list node has two rests, > > > > Those don't seem hard: the latter two are contradictions, > > and the former two just mean there aren't enough premises > > or whatever to come to interesting conclusions. > > Not true. The latter two are not contradictions unless the two firsts or > rests can be shown to be distinct. Well, yes, by "two firsts" I inferred that you meant first(L, X) and first(L, Y) where X<>Y. That's the conventional meaning of "two", no? > The former two may or may not lead to > interesting conclusions and may complicate the formal specification and > inference. For example, a oneOf on a list missing a rest has a meaning. I guess "complicated" is in the eye of the beholder. It doesn't look complicated to me. > > > 5/ that is circular, or > > > 6/ that is infinite. > > > > I see two options: > > > > (a) do without lists altogether, ala writing > > (and P (and Q (and R S)))) > > instead of (and P Q R S). > > How are you going to do this? All you have to work with are triples, and a > triple is not sufficient to atomically represent (and R S). I don't see how being atomic is relevant. I expect something like this would work: :C ont:intersectionLHS :R. :C ont:intersectionRHS :S. > > That would be tedious; oneOf would go from a simple > > binary relation to an ugly thing ala onProperty/hasValue. > > oneOf would certainly be difficult. well, tedious, but not difficult: :Stooges ont:oneOfFirstItem :Moe. :Stooges ont:oneOfRest _:C1. _:C1 ont:oneOfFirstItem :Larry. _:C1 ont:oneOfRest _:C2. _:C2 ont:oneOfFirstItem :Curly. _:C2 ont:oneOfRest ont:Nothing. > > (b) work thru the details of induction over lists. > > This would take us outside of FOL, which would > > make the formal aspects of our spec more complex, > > but most users would probably prefer it > > to the tedious option (a). > > Well, to make this work you would have to go through a lot of machinery to > even show that your specification is well-formed at all. Yes, we need to carefully review our spec. (or is there some technical sense of "well-formed specification" that you're using?) > You would also > probably have to do a lot more work to show that your specification was > realizeable. Hmm... that looks like another term of art that I'm not familiar with. > The kinds of things that could crop up include infinite lists > that cover everything in an otherwise-recognizable category, thus leading > to non-compactness. I'm sure there are lots of ways to get it wrong. > > Lots of practical systems do this: Larch > > and ACL2 call themselves 1st order systems, > > but they sneak in induction. > > > Well, ACL2 is much less sneaky... > > > > A Precise Description of the ACL2 Logic > > http://www.cs.utexas.edu/users/moore/publications/km97a.ps.Z > > > But Larch is pretty glib... > > > > "Except for the fact that it provides a rich set of notations for > > functions, LP is based on the syntax and semantics for first-order logic > > found in many textbooks." > > -- LP, the Larch Prover -- Logical syntax and semantics > > http://www.sds.lcs.mit.edu/Larch/LP/logic/logic.html > > > > (I still need to study Michael's stuff on ACL2 and OWL... > > http://lists.w3.org/Archives/Public/www-webont-wg/2002Mar/0301.html ) > > Well, I don't think that you are going to get what you want out of these > systems. I don't want anything out of them. > The induction in ACL2 is used, for example, to prove conjectures about > regular, i.e., finite and non-circular, lists. Proving conjectures about > infinite structures, i.e., infinite lists or the integers, is different. > > > > For example, what is the meaning of a malformed restriction, i.e., a > > > restriction > > > 1/ that is missing an onProperty element, > > > 2/ that has none of the other parts of a restriction, or > > > > again, it's just as if you have a rule that says > > IF: parent(X, Y) > > AND brother(Y, Z) > > THEN: uncle(X, Z) > > and you have brother(a, b) with no clues about > > who a is a parent of; you just can't come to any > > uncle(X, b) conclusions. > > How have you shown that no conclusions can arise? I haven't. I just made an analogy. > There are lots of > unusual cases to consider, including cases where there only a limited > number of classes or properties or individuals in any model. Yes, I'm sure there are lots of ways to get it wrong. > > > 3/ that has more than one of the other parts of a restriction. > > contradiction. > > > > > These are a problem for the DAML+OIL way of expressing the model-theoretic > > > semantics of triple KBs, but there is a solution there because the DAML+OIL > > > model theory keys off the (syntactic) triples, not the (semantic) IEXT. > > > > > > [...] > > > > > > > > M3 What is the formal meaning of an OWL KB? > > > > > > > > Whatever we specify it to be, no? > > > > > > [...] > > > > > > > > http://www-db.research.bell-labs.com/user/pfps/owl/translation.html > > > > > > > > There's also my proposal to do a model theory straight from > > > > the triple abstract syntax: > > > > > > > > * layering (5.3,5.10): a same-syntax model theory > > > > Dan Connolly (Thu, May 30 2002) > > > > http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0264.html > > > > > > Your proposal is not a model theory from the triple syntax but is instead a > > > model theory from RDFS interpretations. Your way of specifying semantics > > > for triple KBs is *much* harder than specifying semantics from the triple > > > syntax. In particular, it cannot handle malformed lists and restrictions > > > in the way that they are handled in the DAML+OIL semantics. > > > > Yes, specifying exactly how lists work is tricky. We could perhaps avoid > > that. But I think it's worth the effort, since the effort is over > > when we finish our spec, but the effort for users to deal with a klunky > > language lasts long after. > > Well then I suggest that you get to work. Is that sort of remark really necessary? I could sure live without it. > Until a specification is > presented I remain unconvinced that a specification is possible and, even > if it is possible, that it will result in a language that is less kluky > than one that avoids these issues. I'm pretty sure an existince proof of the possibility is easier than a proof that it's impossible. 1/2 ;-) -- Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Wednesday, 19 June 2002 16:11:09 UTC