From: Pascal Hitzler <hitzler@aifb.uni-karlsruhe.de>

Date: Fri, 09 Dec 2005 20:52:18 +0100

Message-ID: <4399E072.7090203@aifb.uni-karlsruhe.de>

To: Hassan Aït-Kaci <hak@ilog.com>

CC: Jim Hendler <hendler@cs.umd.edu>, Enrico Franconi <franconi@inf.unibz.it>, Uli Sattler <Ulrike.Sattler@manchester.ac.uk>, public-rif-wg@w3.org

Date: Fri, 09 Dec 2005 20:52:18 +0100

Message-ID: <4399E072.7090203@aifb.uni-karlsruhe.de>

To: Hassan Aït-Kaci <hak@ilog.com>

CC: Jim Hendler <hendler@cs.umd.edu>, Enrico Franconi <franconi@inf.unibz.it>, Uli Sattler <Ulrike.Sattler@manchester.ac.uk>, public-rif-wg@w3.org

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.orgReceived on Friday, 9 December 2005 19:52:57 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:47:36 UTC
*