- From: pat hayes <phayes@ai.uwf.edu>
- Date: Mon, 23 Jul 2001 17:27:26 -0700
- To: Graham Klyne <Graham.Klyne@Baltimore.com>
- Cc: w3c-rdfcore-wg@w3.org

>At 01:56 PM 7/16/01 -0500, Aaron Swartz wrote: >>I'm unclear on the difference between model theory and abstract >>syntax. Can someone clarify? > >I'll take a shot; I guess the real formal systems folks will put me right... > >I think they are clearly different, but related, issues. > >- Abstract syntax defines a language (i.e. a set of well formed >formulae, or wff) in terms of some set of terminal symbols. Given a >formula, it allows us to say whether or not it is a well formed >sentence (instance) of the language. It also provides us with an >annotation for the the structure of a wff that can be used as a >reference point for defining semantics for the various allowed >forms. In summary: abstract syntax is primarily about forms. > >- Model theory defines semantics for the various allowed forms, by >telling us how they can be interpreted in terms of some universe of >discourse. The elements of the language refer to members of the >universe, and statements can be interpreted to be true or false of >of such a universe. An "interpretation" of a formula is an >assignment of values from the domain of discourse to symbols in the >formula, such that the formula can be said to true or false. A >"model" of a formula is an interpretation for which the formula >evaluates to true. Hence "model theory". > >- A third related concept is "proof theory": a deductive apparatus >based on syntactic transformations of wffs that preserves truth. Pretty much right :-). I tend to think of an abstract syntax as the syntax abstracted away from the purely lexical details, and treated as a kind of algebra (the term is due to John McCarthy, and this is his way of thinking.) One way to state the relation between abstract syntax and model theory (AKA logical semantics, BTW) is that the abstract syntax specifies the syntax in just enough detail to make it possible to state the interpretation rules of the model theory, but no more. So for example, you need to know that a conjunction is a conjunction and has, say, a list of conjuncts; and that is really all you need to know in order to say that a conjunction is true (in I) iff all of its conjuncts are true in I and false otherwise. You don't really need to know that the conjunction is written by writing '&&' in between each conjunct, or by writing '(and' and then the conjuncts and then ')', or whatever; those are the concrete syntax details. You can have many different concrete syntaxes for the same abstract syntax, but if there is a 'canonical' concrete syntax then that will serve just as well. For us, the RDF graph is something like an abstract syntax and N-triples is the cononical concrete (lexical) syntax, I guess. Pat PS. You can do proof theory on the abstract syntax, by the way, and the result is often called 'natural deduction', though this term is also used for concrete proof theories. The overarching idea is that for each kind of statement (universal quantifications, conjunctions, whatever) there are two rules of inference, one which introduces it (ie has a conclusion of that form) and one which eliminates it (ie uses an antecendent of that form). --------------------------------------------------------------------- (650)859 6569 w (650)494 3973 h (until September) phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes

Received on Monday, 23 July 2001 20:27:25 UTC