- From: Drew McDermott <drew.mcdermott@yale.edu>
- Date: Thu, 21 Dec 2000 13:19:30 -0500 (EST)
- To: connolly@w3.org
- CC: drew.mcdermott@yale.edu, www-rdf-logic@w3.org
> It's not obvious that serializing graphs is a key goal. OK... I guess my argument is reduced to: your proposal doesn't layer neatly on a bunch of RDF software in development that is all based on graphs/triples. I'm not sure if it does or doesn't. If you supply an encoding of language L in RDF, the tools will then work on language L. Of course, what the tools tell you may be of limited value. But all that software doesn't grok functional terms, negation, nor universal quantification, which are things I want, and after looking at your proposal again, it seems more feasible to write the sort of software I'm interested in (proof checkers) to support this syntax than to support a strictly triple-based approach. Yes. > In the meantime, it seems to me there is a need for an XML-based > notation for logical statements. I don't think it needs to look > radically different from RDF, but it does need to give up the graph > model. OK... here are my comments on your proposal, as I read it. I think the main thing I don't understand is how MP/MT bottom out; i.e. how lookup(c, propName) and denotation(URI) work. I'd like to see a worked-out example of how MP and MT work; i.e. start with a fairly complex formula and show the results of evaluating MP on it. denotation is assumed given. I.e., someone else has to provide a theory of what URIs denote. For now, you can just pretend this is a big table. Here's an example (comments preceded by //): MP(global_env, // At top level the variable bindings are just // whatever is in the various namespaces. <rdf:Description about="people:citizen/0035702"> <x:fullname> <rdf:Term op="x:person_name"> <x:last>Foobar</x:last> <x:first>Sally</x:first> </rdf:Term> </x:fullname> </rdf:Description>) = MP((global_env + [*=denotation("people:citizen/0035702")]), x:fullname>...</x:fullname>) // Now I'm going to abbreviate the denotation of //"people:citizen/0035702" with the symbol "SF". // I'll also asume that when we look up things like // "x:fullname" we get relations that just happen to // have names in English that look very similar to the strings // that denote them in XML. If that's confusing, translate // all the non-parenthesized occurrences of fullname into // some other language. = lookup((global_env + [*=SF)]), "x:fullname") (lookup((global_env + [*=SF]), *), MT((global_env + [*=SF]), <rdf:Term>...</rdf:Term>)) = full_name(SF, MT((global_env + [*=SF]), "x:person_name) (<"x:last", MT((global_env + [*=SF]), <x:last>Foobar</x:last>)>, <"x:first", MT((amespace + [*=SF]), <x:first>Sally</x:first>)>)) // The outer angle brackets indicate tuples; we're not in // XML any more = full_name(SF, person_name(<"x:last", "Foobar">, <"x:first", "Sally">)) | The disadvantage is that we can't assert a complex | expression without asserting its parts. That's true enough; there's no syntactic sugar for quoting, but... | I have an alternative proposal, which does little violence to most | uses of RDF, but does away with the ability to assert an arbitrary | piece of an expression just by referring to it. Which ability is that? Just referring to the parts of a statement doesn't assert it. I guess I should have said, "Just by virtue of its being explicitly expressed." | Within the scope of a variable binder such as Forall, ref="name" | is like resource="#name", except that the link "#name" and the | resource pointer are global, whereas var and ref set up a purely | local link. (So we can reuse them without fear of ambiguity.) Example: I don't see this. The string "xyz" is 'global' in the sense that it's the same string everywhere in the world. A use of a symbol as a variable can be scoped regardless of the spelling of the symbol name; I see no reason not to use "#name", an abbrevaiation for http://...address-of-this-document#name, as a variable symbol name. But... hmm... there's not much reason *to* use #name either. It doesn't matter. I thought the sharp sign had a meaning to XML. I'm trying to avoid that meaning. | <rdf:Type resource="http://social.org/categ-ns#Vote"> "type" is spelled with a lowercase "t" in RDF-of-Jan'99. I assume you don't mean anything by the capitalization. No. | With no explicit ID, var, or about, the description behaves like #1, | but there's no constant to refer to. Perhaps it's more straightforward to say that with no explicit ID, it's short for a <rdf:Exists> construct? Yes, I think so. | We interpret a Description/ID at the top level as declaring that an entity exists. I don't know what an "entity" is. If that's a term you're introducing in this document, that's very well, but if it refers to something in "traditional logic-based tools", please explain. By "entity" I just meant an individual of some sort. I know it has a technical meaning in XML; maybe I shold have said "thing" to avoid confusion. | The expression const="ont:action" uses a new notational idea, that of a constant. | This is simply a name (in the namespace sense) used to refer to something. | Perhaps RDF already allows this, but if so it isn't obvious. No, the RDF syntax doesn't have a way of using qnames (prefix:localname) as the objects of statements. The reason why not is historical and has gone away, though, I think. It seems to me to be something that's obviously needed: constants that are scoped at the level of namespaces. However, I think the way I treat this is currently buggy. I didn't allow for Descriptions to be about new constants, so it's not clear how the properties of these constants get recorded. This is very interesting... | There may be a need for pointers to pieces of RDF considered as data objects, | or considered as places in cyberspace. We should introduce an alternative | field, perhaps 'expID,' for this purpose. TimBL has tried to convince me that there's some fundamental confusion around whether ID="foo" can be used for both "this piece of RDF/XML syntax, in case you are, for example, styling it for display" and "the subject of this bunch of assertions." He hasn't managed to convince me, but I expect he would be happy with expID, as it seems to address his concern. Unfortunately, it turns out to be a tease: | I will ignore | expID's in the rest of this proposal. Oh well... I'll try to find a use case/test case where it matters... I think the distinction clearly matters. The cases where it's obvious are where a Description is scoped in a context that makes it meaningless to refer to it from afar. I'm having trouble thinking of an example because of another bug in the proposal as it stands: I said at one point that IDs could be hypothetical, meaning that they denote something only relative to a context. But I didn't actually reflect that in the formal semantics. So I can't really do more than hand-wave about this remote-reference issue. | propertyElt ::= '<' propName refAttr '/>' | | '<' propName '>' term '</' propName '>' | | '<' propName '>' string '</' propName '>' RDF has this parseType="literal" mechanism for using arbitrary XML content, rather than just a string, as the value of a property. You don't seem to have captured that (though it looks easy to add). Okay, but I'm leery of "arbitrary XML content" in a formal language. If we have such an escape mechanism, then we're giving up on the semantics at that point. I suppose there might be some value in declaring that a certain string, although meaning nothing in the formal framework, is guaranteed to be parseable as XML. | MP is defined by the following equations: Hmm... this reminds me of the XSLT-based RDF parser I hacked up... I wonder if I could hack up MP in XSLT... Don't know much about XSLT. (Sounds like a hit song in the making....) | where g is a new symbol. Huh? I don't see any g. Crud arising after several revisions; ignore. | MP(c + [* = v] What's this [* = v] notation? Is * just a regular variable name? I assume so... Yes, as in the example above. It's just used to get the subject of the relation distributed around in the right way. | If the typeSpec is missing, it defaults to <rdf:Type const="Something">. Hmm... the syntax allows just one type... types seem to be integrated into the syntax, rather than just being regular assertions about things. I'm not sure I understand... I tried to allow both general types and concise types. So the unabbreviated syntax has <rdf:type>arbitrary term denoting a type</rdf:type> But most types are just symbols, so they can be moved into the brackets. Anyway... Something should be grounded globally, no? i.e. rdf:Something? Yes, in the global_env. Er... the definitions seem to bottom out at: | MP(c, '<' propName refAttr '/>') | | = lookup(c, propName)(lookup(c, *), | MT(c, refAttr)) I don't have a good feel for what lookup(c, propName) means. I don't see how c could contain a binding for propName... unless the algorithm is sort of itialized with c containing the mapping from all URIs in the world (or at least: some relevant set of the URIs in the world) to what they mean. Hmm... I guess I could get my head around that; is that what you meant? Yes. As with other applications of formal semantics, you have to buy the premise to buy the bit. It's actually not so foolish: when specifying the formal semantics of a language, you don't also have to specify how names get connected to the world. | MT(c, a) = MP(c, a) if a is an Assertion or Description Er... is that going to end up with the meaning of such a term being 'true' or 'false', or with the meaning of such a term being a forumula? Good question. Obviously, it doesn't make sense the first way. The second requires some sort of modal approach. This is insufficiently clarified in my proposal (and likely to remain so). | Note that the op applies to the inside of the lambda expression | in this case, as opposed to the outside for the similar | Description. If this is too inconsistent, we could change it. I'm confused about terms with variables... what are they for? was there an example? They're for referring to bound variables. Example: Anyone who serves as his own lawyer has a fool for a client. <rdf:Forall var="p" type="x:Person"> <rdf:If> <rdf:Description about="p"> <x:has_lawyer ref="p"/> </rdf:Description> <rdf:Description var="c"> <x:client_of ref="p"/> <x:foolishness const="x:high"/> </rdf:Description> </rdf:If> </rdf:Forall> | MT(c, 'resource=' URI) = denotation(URI) Er... what does denotation(URI) mean? Why didn't you use lookup(c, URI) as before, in the propName case? Could have. I just see URIs as being in a different "name space" than what XML calls namespaces. | MT(c, 'const=' s) = lookup(c, s) [which searches the appropriate namespace] I'm confused... I assumed you were just using qnames as short-hand for URIs, independent of this lookup() thing; but now it seems you're using lookup() both for the c + [var=val] bindings that you introduce and for the syntactic xmlns= bindings. ??? Yes. Maybe const and var are the same thing?? (A const being a globally-scoped var.) | 1.If an Assertion uses a standard operator o (rdf:And, rdf:Or, etc., What does etc. mean here? it means rdf:Not, rdf:If, or rdf:Iff . | 4.If all the arguments of a Term have label rdf:Arg, as opposed to...? Oh! I get it... arguments are labelled, rather than positional... and labelling them all rdf:Arg says the order doesn't matter. nifty. Right. I should produce a revised version to get rid of some of the bugs I mentioned, and hide the others better. -- Drew
Received on Thursday, 21 December 2000 13:19:47 UTC