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)
|