User loginNavigation 
Semantics: Logic vs. PLThe famous three approaches to programming language semantics are axiomatic, operational and denotational semantics. The famous two approaches to logic semantics are proof theory and model theory. I find denotational semantics similar to model theory, and operational semantics similar to proof theory. However, I find no analogue to axiomatic semantics, and I wonder if there is one, and if not, why? In model theory, one takes an abstract logical language and defines its meaning within an existing theory: classical logic is interpreted in set theory (models are simple sets), intuitionistic logic in Kripke Scenarios (or Heyting Algebras), etc. In essence, we define the meaning of the new language in terms of existing, familiar languages. This is no other than denotational semantics, where our programs denote structures in existing, welldefined structures. In proof theory, we associate no inner meaning with the language. Rather, the meaning emerges out of the symbol pushing that is the proofs. Operational semantics operates along the same lines, mechanically manipulating program text, and the meaning emerges out of the textual juggling. Moreover, many modern operational semantics are actually given as a proof system, the theorems being the valid executions of the language. However, I do not recognise a similar analogy for axiomatic semantics. Am I missing something? Or is it simply because we do not want to explain one logic with another? Or perhaps the power of axiomatic semantics is the augmentation of the computable language with uncomputable/high complexity constructs, something that does not always interest logicians? By Ohad Kammar at 20090612 10:24  LtU Forum  previous forum topic  next forum topic  other blogs  158045 reads

Browse archivesActive forum topics 
Recent comments
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago