@inproceedings(HowardPCF,
Author="Brian T. Howard and John C. Mitchell",
Title="Operational and Axiomatic Semantics of {PCF}",
Booktitle="ACM Conference on {\sc Lisp} and Functional Programming",
Year="1990",
Pages="298-306")
PCF, as considered in this paper, is a lazy typed lambda calculus with functions, pairing, fixed-point operators and arbitrary algebraic data types. The natural equational axioms for PCF include eta-equivalence and the so-called ``surjective pairing'' axiom for pairs. However, the reduction system pcfesp defined by directing each equational axiom is not confluent, for virtually any choice of algebraic data types. Moreover, neither eta-reduction nor surjective pairing seems to have a counterpart in ordinary execution. Therefore, we consider a smaller reduction system pcf without eta-reduction or surjective pairing. The system pcf is confluent when combined with any linear, confluent algebraic rewrite rules. The system is also computationally adequate, in the sense that whenever a closed term of ``observable'' type has a pcfesp normal form, this is also the unique pcf normal form. Moreover, the equational axioms for PCF, including (eta) and surjective pairing, are sound for pcf observational equivalence. These results suggest that if we take the equational axioms as defining the language, the smaller reduction system gives an appropriate operational semantics.
@phdthesis(HowardThesis,
Author="Brian T. Howard",
Title="Fixed Points and Extensionality in Typed Functional Programming
Languages",
School="Stanford University",
Year="1992",
Note="Published as Stanford Computer Science Department Technical
Report STAN-CS-92-1455")
We consider the interaction of recursion with extensional data types in several typed functional programming languages based on the simply-typed lambda calculus. Our main results concern the relation between the equational proof systems for reasoning about terms and the operational semantics for evaluating programs. We also present several results about the expressivity of the languages, compared according to both the functions and the data types definable in them. The methods used are those of classical lambda calculus and category theory.
The first language discussed is a variant of Scott and Plotkin's PCF, which adds to the simply-typed lambda calculus products, fixed points of functions, and algebraic data types specified by a signature and a set of equations. PCF is able to express all partial computable functions over the given basic types, but the corresponding reduction system is not confluent if we include the usual surjective pairing rule, which expresses the extensionality of products. Extensionality is necessary in the proof system for establishing many useful isomorphisms between types, but it does not seem to have an intuitive ``computational content.'' We show that a smaller reduction system without extensional rules is sufficient for computing the result of program execution, and that this smaller system is confluent whenever the algebraic rules are confluent and left-linear. If the algebraic rules are also terminating and left-normal then a leftmost reduction strategy is complete for finding normal forms.
We then consider a pair of languages, lambda-mu-nu and lambda-bottom-rho, which support the definition of structured data types through categorical means rather than via multi-sorted algebras. The first language, lambda-mu-nu, extends the types of the simply-typed lambda calculus with extensional products and sums, and least and greatest fixed points of positive recursive type expressions. By dropping the extensional rules as for PCF, we obtain a confluent and strongly normalizing reduction system, adequate for obtaining results of programs. It is easy to represent many common data types in this language, such as booleans, natural numbers, lists, trees, and (computable) streams, as well as many of the total functions over such structures. Indeed, we may define more functions over the natural numbers than are provably total in Peano arithmetic, hence the language is more expressive than Gödel's system T. It is no more expressive than the Girard/Reynolds system F in terms of definable functions; however, we are able to define algorithms that are not expressible in F, such as a constant-time predecessor function on the naturals.
The final language, lambda-bottom-rho, extends lambda-mu-nu by introducing lifted types, which contain a bottom element, signifying that evaluation of a term of such a type may not terminate. Lifted types allow us to find fixed points of mixed-variant recursive type expressions; for example, the solution of X = X -> X_bottom gives a type for expressions of an eager untyped lambda calculus, while the solution of X = (X -> X)_bottom is suitable as a type for expressions of a lazy untyped calculus. We again have a confluent operational semantics for the language, although of course it is not strongly normalizing. However, we show that a lazy reduction strategy will find normal forms for terms which have them. We also examine the relations among the three kinds of recursive type in lambda-bottom-rho, which we refer to as inductive (least), projective (greatest), and retractive (mixed-variant); in the natural cpo model of the language, we give conditions under which the different constructions will coincide.
@techreport(HowardIPR,
Author="Brian T. Howard",
Title="Inductive, Projective, and Retractive Types",
Institution="Department of Computer and Information Science,
University of Pennsylvania",
Number="MS-CIS-93-14",
Year="1993")
We give an analysis of classes of recursive types by presenting two extensions of the simply-typed lambda calculus. The first language only allows recursive types with built-in principles of well-founded induction, while the second allows more general recursive types which permit non-terminating computations. We discuss the expressive power of the languages, examine the properties of reduction-based operational semantics for them, and give examples of their use in expressing iteration over large ordinals and in simulating both call-by-name and call-by-value versions of the untyped lambda calculus. The motivations for this work come from category theoretic models.
@techreport(HowardSorting,
Author="Brian T. Howard",
Title="Another Iteration on Darlington's `A Synthesis of Several
Sorting Algorithms'",
Institution="Department of Computing and Information Sciences, Kansas
State University",
Number="KSU CIS 94-8",
Year="1994")
In ``A Synthesis of Several Sorting Algorithms'', Darlington showed how to use program transformation techniques to develop versions of six well-known sorting algorithms. The purpose of this note is to provide more evidence for the naturalness of the resulting taxonomy of algorithms by showing how it follows almost immediately from a consideration of the types of the objects involved. By exploiting the natural operations of iteration and coiteration over recursively defined data types, we may automatically derive the structure of each algorithm.
@techreport(HowardFCC,
Author="Brian T. Howard",
Title="Fixpoint Computations and Coiteration",
Institution="Department of Computing and Information Sciences, Kansas
State University",
Number="KSU CIS 95-1",
Year="1995")
Preliminary version of the next paper.
@inproceedings(HowardICFP,
Author="Brian T. Howard",
Title="Inductive, Coinductive, and Pointed Types",
Booktitle="Proceedings of the 1996 ACM SIGPLAN International
Conference on Functional Programming",
Year="1996",
Pages="102-109")
An extension of the simply-typed lambda calculus is presented which contains both well-structured inductive and coinductive types, and which also identifies a class of types for which general recursion is possible. The motivations for this work are certain natural constructions in category theory, in particular the notion of an algebraically bounded functor, due to Freyd. We propose that this is a particularly elegant core language in which to work with recursive objects, since the potential for general recursion is contained in a single operator which interacts well with the facilities for bounded iteration and coiteration.