New Techniques for the Analysis and Implementation of Functional Programs
10:00 a.m., Monday, May 24, 1993
12th floor conference room, 719 Broadway
Functional programming languages provide programmers with clean semantics and side-effect free computation, which make easier the tasks of designing programs and reasoning about them. Efficient implementations of purely functional programs, however, can pose certain challenges. Our purpose in this dissertation is to develop new techniques for the efficient analysis and implementation of functional programs.
Our first goal is to investigate a syntactic approach, contrary to the usual semantic approaches, of finding the least fixed points of higher-order functions over finite domains. The second objective is to develop implementation techniques for aggregate data structures for functional programs such that accesses to aggregates are both efficient and side-effect free.
Finding the least fixed point of a monotonic function over a finite domain is an essential task when analyzing a functional program in the framework of abstract interpretation. Previous methods for least fixed point finding have primarily used semantic approaches, which often traverse large portions of the semantic domain and may be very inefficient even for simple programs. We propose a syntactic method based on an augmented simply typed lambda calculus. It is shown that, for finite domains, the syntactic method is both sound and complete with respect to the semantics. Moreover, we demonstrate that the proposed syntactic method can be quite effective in cases where the usual semantic method is very inefficient.
Efficient implementations of aggregate data structures for functional
programs has been an active research topic. The problem arises
because once an aggregate is updated, both the old version and newly
updated copy must be preserved to maintain the side-effect free
semantics of functional languages. We modify the shallow binding
scheme of Baker to implement functional arrays for efficient
incremental updates and voluminous reads. The scheme, however, uses
side-effects and cannot be implemented in purely functional
languages themselves. We then investigate the possibility of
implementing efficient aggregates without using side-effects, and
show that real-time deques can be implemented in a purely functional
way. We describe several interesting applications of this