Operational Reasoning and Denotational Semantics. AIM-264
- Title:
- Operational Reasoning and Denotational Semantics. AIM-264
- Author:
- Gordon, Michael
- Author (no Collectors):
- Gordon, Michael
- Collector:
- Gordon, Michael
- Description:
-
"Obviously true" properties of programs can be hard to prove when meanings are
specified with a denotational semantics. One cause of this is that such a
semantics usually abstracts away from the running process - thus properties
which are obvious when one thinks about this lose the basis of their
obviousness in the absence of it. To enable process-based intuitions to
be used in constructing proofs one can associate with the semantics an
abstract interpreter so that reasoning about the semantic can be done by
reasoning about computations on the interpreter. This technique is used
to prove several facts about a semantics of pure LISP. First a denotational
semantics and an abstract interpreter are described. Then it is shown that
the denotation of any LISP form is correctly computed by the interpreter. This
is used to justify an inference rule - called "LISP-induction" which
formalises induction on the size of computations on the interpreter. Finally
LISP-induction is used to prove a number of results. In particular it is
shown that the function eval is correct relative to the semantics - i.e.
that it denotes a mapping which maps forms (coded asd S-expressions) on to
their correct values.
- Topic:
- Artificial intelligence
- Subject:
- Stanford Artificial Intelligence Laboratory and Memo (Stanford Artificial Intelligence Laboratory)
- Language:
- English
- Physical Description:
- 1 text file
- Publication Info:
- Stanford (Calif.) and cau
- Date:
- August 1975
- Place created:
- Stanford (Calif.)
- Imprint:
- Stanford (Calif.), August 1975
- Genre:
- memorandums
- Identifier:
- AIM-264
- Repository:
- Stanford University. Libraries. Department of Special Collections and University Archives
- Collection:
- Stanford Artificial Intelligence Laboratory records, 1963-2009
- Manuscript number:
- SC1041