[Top] [All Lists]

Re: [ontolog-forum] Role of definitions (Remember the poor human)

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 13 Feb 2007 14:22:17 -0600
Message-id: <063EB472-17EA-4DF1-A0BB-2447F0E2FA50@xxxxxxxx>
On Feb 13, 2007, at 1:49 PM, Kathryn Blackmond Laskey wrote:
>> ...I think it is potentially confusing, and at
>> the least out of keeping with standard usage in logic, to call
>> anything proof theoretic "semantics".
> In computer science, programs have operational semantics.  I read a
> paper a few years ago describing an inference engine the author
> wrote, which said "The semantics of our engine is what it computes."
> A proof theory for a logic would correspond to operational semantics
> for a theorem prover based on that proof theory.    (01)

I'm not sure that's the right way to think about it, though there are  
analogies due to the nature of the languages in question.  In my  
view, operational semantics is *definitely* a semantics in the model  
theoretic sense, only it is a semantics appropriate for computer  
languages, which contain procedural commands that dictate what a  
system should *do* rather than declarative statements saying the way  
certain things in the world *are*.  Thus, the appropriate semantics  
for such languages involves a model of computation:  the semantics of  
a program written in a computer language language will be expressed  
as a mathematical model of the transitions of a system, starting in  
some initial state, as it moves from state to state in accordance  
with the program.  Because of this, certain proof theoretic  
techniques might be useful for describing state transitions, but it  
is a mistake, I think, to conclude that the semantics is therefore a  
type of proof theory.  It's a different type of semantics,  
structurally speaking, for sure, but it's the same general idea of  
providing mathematical models of meaning for formal languages.    (02)

> Logicians might not use the word "semantics" for this,    (03)

They do.    (04)

> but computer scientists do.    (05)

Many of whom are superb logicians, e.g., Gordon Plotkin, Vaughn  
Pratt, Dana Scott, Tony Hoare, etc.    (06)

Chris Menzel    (07)

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (08)

<Prev in Thread] Current Thread [Next in Thread>