Computer Science Department
School of Computer Science, Carnegie Mellon University
Denis R. Dancanet
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.