Re: RIF vs Rule Language

Hassan,

I very much apprechiate your point - the term "formal semantics" is 
easily interpreted in too narrow a sense. But let me just add (and 
emphasize, as I assume that you agree with me on this) that procedural 
semantics alone is not satisfactory for a semantic web context, as it 
usually binds a language to a specific engine, and is thus not in the 
spirit of interoperability and interchange.

Best Regards,

Pascal.


Hassan Aït-Kaci wrote:
> 
> Jim Hendler wrote:
> 
>> well, that's true - but let's not forget there are a number of 
>> different kinds of semantics - I don't know of any programming 
>> language in major use that has anything other than operational 
>> semantics, and they seem to work pretty good (at least this email 
>> seems to be getting to you through a whole bunch of computers and 
>> routers and programs, and I suspect few if any have a model theory) --
> 
> 
> My point precisely.
> 
>>   this is not to advocate not doing a formal semantics, but just to 
>> remind people that an option is to do basically an operational semantics 
> 
> 
> But who said that an operational semantics may not be _formal_ ? Formal
> semantics of computational systems is, by far, not equivalent to a _model_
> semantics. Model theory has actually been decried among logicians that
> are proof theorists as a feature of a rather restricted class of logics.
> Because FOL has a model theory that coincides with its proof theory does
> not mean that this is the case for all logics. Models are convenient
> to caracterise immutable truth/falsity - which is what FOL formulas denote.
> In fact, any logic of change, while simple to express as a proof theory,
> will struggle (and generarally to little avail) to define appropriate
> models. In fact, one of the most expressive formal logic of change, Linear
> Logic (http://iml.univ-mrs.fr/~lafont/linear/), couldn't care less about a
> model theory. I remember an invited talk to ICLP back in the 90's by
> Jean-Yves Girard (the inventor of Linear Logic, as well as F_\omega, a
> second-order polymorphic type theory) where he made a forceful statement
> in reaction to the Association for Logic Programming's logo which is:
> "\vdash \equiv \models" (pardon my LaTeX). He proposed to replace it
> more appropriately with "\vdash \perp \models". In words, in general
> proof theory is not equivalent to model theory, but rather the two are
> orthogonal! The fact that MT and PT coincides for FOL (and its sublogics
> such as  like Horn, DLs, etc...) is a coincidence, not the general case,
> and surely not a requirement for defining any formal logic or computation
> system - be it inferential or evaluational. In fact, a successful formal
> semantics of Linear Logic has started to emerge - Game Semantics - where
> formulas are seen as games between two players. This has led to the
> formulation of a promising new logic - Computability Logic (please see
> http://www.cis.upenn.edu/~giorgi/cl.html) - based on the game-playing
> paradigm, that may be seriously argued to be the best formal adequation
> bewtween Logic and Computation.
> 
> All this to say that there is no formal ground upon which to substantiate
> the a priori adoption of one formalism over the other. The main criteria
> ought to be simplicity and intuitiveness - i.e., the formalization of a
> system must appeal to the intuition of its users so that they may relate
> to the benefits it brings them. (How many Prolog programmers care about
> its Model Theory ? - I did write "programmers" not "researchers").
> 
> Gordon Plotkins' SOS formalism is one rule-based (!) formalism that has
> been successfully used to express the operational semantics of 
> computational
> systems -
> http://citeseer.ist.psu.edu/cache/papers/cs2/461/http:zSzzSzhomepages.inf.ed.ac.ukzSzgdpzSzpublicationszSzSOS.pdf/plotkin81structural.pdf 
> 
> SOS has been the de facto standard formalism used by formalists designing
> programming languages (see most POPL papers during the last 20 years!).
> Building on Plotkin's idea, Gilles Kahn then proposed Natural Semantics
> (http://portal.acm.org/citation.cfm?id=696269) using Horn Logic to
> automate the actual generation of interpreters (or compilers) from
> formal SOS-like Horn specifications. This was the core of the Typol
> system implemented by Thierry Despeyroux at INRIA. Interestingly,
> Natural Semantics has been proposed for the Semantic Web - though I
> am not sure how relevant these ideas are to RIF, they look quite
> promising to me (http://www-rocq.inria.fr/~tdespeyr/papers/riao2000-2/,
> http://www-sop.inria.fr/croap/centaur/tutorial/main/section3_8.html).
> 
> Cheers,
> 
> -hak

-- 
Dr. Pascal Hitzler
Institute AIFB, University of Karlsruhe, 76128 Karlsruhe
email: hitzler@aifb.uni-karlsruhe.de    fax: +49 721 608 6580
web:   http://www.pascal-hitzler.de   phone: +49 721 608 4751
        http://www.neural-symbolic.org

Received on Friday, 9 December 2005 19:52:57 UTC