This thesis is about the theory and practice of intensional semantics. Traditional denotational models of programming languages are usually extensional in that they concern themselves only with input/output properties of programs. The meaning of a program is typically taken to be a function from input to output containing no information about the way that function computes its result. In an intensional denotational semantics, the meaning of a program is an object embodying aspects of the computation strategy. The structure of the object varies, depending on the language one models and the intended usage. For instance, previous intensional semantics have been developed using functions on richer domains, pairs of a function and a computation strategy, and sequential algorithms, and they were used to reason about efficiency, complexity, order of evaluation, degrees of parallelism, efficiency-improving program transformations, and so on.

In the first part of this thesis, we develop an intensional semantics based on abstract circuits. A program is mapped to a circuit, whose dimensions tell us how much parallel work and time is required to execute the program. We relate the circuit dimensions to various execution strategies, and to more traditional models of parallel execution, such as the PRAM. Our main application for circuit semantics is the establishment of relative intensional expressiveness results. Extensional expressiveness is concerned with whether a construct enables us to compute new functions. Since most programming languages are Turing-complete this is usually not very interesting. On the other hand, intensional expressiveness is concerned with whether a construct enables us to write more efficient programs. Utilizing a somewhat surprising connection with the field of circuit complexity, we study the relative intensional expressive power of various deterministic and nondeterministic parallel extensions of PCF.

Although most of our results have to do with parallel programming languages, we also study relative intensional expressiveness in a sequential setting. Using techniques different from circuit semantics, we compare Colson's primitive recursive algorithms to Berry and Curien's sequential algorithms, in the area of efficient expressibility of a function that computes the minimum of two lazy natural numbers.

In the second part of this thesis, we establish the practical utility of intensional semantics, by taking an existing semantics, that of sequential algorithms on concrete data structures, and using it to develop a refinement type inference system. The system features recursive types, subtyping, intersection types, polymorphism, and overloading. The types are the concrete data structures, and the terms are expressions in a lazy, higher-order, polymorphic, functional language, which are compiled to categorical combinators represented by sequential algorithms. A type may be refined by several subtypes (for instance, bool can be refined by true and false). The type always differs from its refinements at a finite number of points. If a term has a regular type, then the system enters into an interrogative abstract interpretation session with it, seeking to evaluate it only at those points relevant from the point of view of refinement type inference. Sequential algorithms provide very precise information about the dependence of pieces of output on pieces of input, and we can use this intensional information to generate a refinement type. We prove soundness of both the type inference and refinement type inference, and we show several examples from our prototype implementation.

180 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu