[Prev][Next][Index][Thread]
Abstract for "Logic from Computer Science"
Date: Thu, 28 Sep 89 15:54:45 PDT
To: ynm@math.ucla.edu
Cc: types@theory.LCS.MIT.EDU
PCF considered as a programming language
John C. Mitchell
Computer Science Department
Stanford University
Talk Abstract
This talk is about reduction properties of a lazy typed lambda
calculus PCF with functions, pairing, and fixed-point operators at
all types. This language has been used as an example programming
language in past theoretical studies and, with the addition
of numerals and a few basic operations, it is sufficient to
define all partial recursive functions. The natural equational
axioms include eta-equivalence and the so-called "surjective
pairing" axiom for pairs. However, if we define reduction R by
directing each equational axiom, the resulting system is not
confluent. This raises the question: Is there a confluent set of
reduction rules which seems computationally sufficient? Moreover,
how do we characterize the sufficiency of this set of rules?
We are interested in answers which apply to PCF over common
algebraic data types such as natural numbers, booleans, lists,
trees, etc., rather than the pure calculus.
We show that the reduction system R- obtained by dropping eta
and surjective pairing has the following properties:
1. R- is confluent, in combination with any linear, confluent
algebraic rewrite rules.
2. If a closed term of "observable" type has an R normal form,
this is also the unique R- normal form.
3. The equational axioms for PCF (including eta and surjective
pairing) are sound for observational equivalence with respect
to R-.
4. Every PCF term has at most one R normal form. When it exists,
the R normal form may be found by reducing to R- normal form,
and then applying eta and surjective pairing in a straightforward
way.
We claim that these results summarize the "adequacy" of R-, in
combination with any linear, confluent algebraic rules, as an
operational semantics for PCF.
This is joint work with Brian Howard.