Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 98: | Line 98: | ||
* Concrete definition (generative grammar) placing successive sets of alternate terms in bijection with the ordinals | * Concrete definition (generative grammar) placing successive sets of alternate terms in bijection with the ordinals | ||
===Semantics=== | ===Semantics=== | ||
Pierce describes three techniques of formalizing semantics: | |||
* ''Operational'' semantics define one or more formal abstract machines, and attempt to exhaustively describe the language constructs in these machines' terms. Emphasis is on proof of various abstract machines' equivalence (and correspondence to actual implementations), and thus proof of an implementation's correctness. When finite state machines are used (this is only possible for simple languages), this is Plotkin's ''small-step'' or ''structural'' operational semantics; more powerful languages might make use of Kahn's ''big-step'' or ''natural'' semantics. | |||
* ''Denotational'' semantics map between different ''semantic domains'' (the investigation of which constitutes [http://en.wikipedia.org/wiki/Domain_theory domain theory]) using ''interpretation functions''. Domains are interesting if results have been proven for their properties, such as termination and safety results. Denotational semantics can thus lead to proof schemas for a language, but meaningful interpretation functions seem to largely require domain-driven language design. | |||
* While operational and denotational semantics define the behaviors of programs, and then prove laws about them, ''axiomatic'' semantics define the behavior of the language in terms of these laws themselves. As Pierce says: "The meaning of a term is just what can be proved about it." | |||
==Sources== | ==Sources== | ||