MESEGUER@SRI-AI.ARPA (03/01/84)
[Forwarded from the CLSI bboard by Laws@SRI-AI.]
REWRITE RULE SEMINAR AT SRI-CSL
Wednesday March 7, 3:00 pm
A Model of Computation
Theory and application to LISP-like systems
Carolyn Talcott
Stanford University
The goal of this work is to provide a rich context in which a
variety of aspects of computation can be treated and where new
ideas about computing can be tested and developed. An important
motivation and guide has been the desire to understand the construction
and use of LISP like computation systems.
The first step was to define a model of computation and develop the
theory to provide basic tools for further work. The main components are
- basic model and notion of evaluation
- equivalence relations and extensionality
- an abstract machine as a subtheory
- formalization of the metatheory
Key features of this theory are:
- It is a construction of particular theories uniformly
from given data structures (data domain and operations).
- Focus is on control aspects of computation
- A variety of objects
Forms -- for describing control aspects of computation
Pfns -- abstraction of form in an environment
-- elements of the computation domain
-- computational analogue of partial functions
Carts -- for collecting arguments and values
Envs -- intepretation of symbols appearing in forms
cTrees -- objects describing particular computations
Applications of this theory include
- proving properties of pfns
- implementation of computation systems
- representing and mechanizing aspects of reasoning
In this talk I will describe RUM - the applicative
fragment (flavor). RUM is the most mathematically
developed aspect of the work and is the foundation
for the other aspects which include implementation
of a computation system called SEUS.