Re: RIF vs Rule Language

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
-- 
Hassan Aït-Kaci
ILOG, Inc. - Product Division R&D
tel/fax: +1 (604) 930-5603 - email: hak @ ilog . com

Received on Friday, 9 December 2005 16:21:18 UTC