[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.