| Lambda-calculus and term rewriting are models of computation that lie at the basis functional programming languages. Both possess syntactic meta-theories that are based on the combinatorial analysis of rewrite steps. Unfortunately, naive implementations of both lambda-calculus and term rewriting are inefficient: subterms are frequently copied, and thus work is multiplied. To overcome this problem in both theoretical systems and actual implementations, duplicate work is avoided by moving from term-based representations to graph-based representations, in which identical subterms can be (but are not always) shared. The question which arises is in what respect such representations and their reductions are optimal in a theoretical sense and can be practical from an implementor's point of view. Unfortunately, thus far it is unclear whether nice theoretical ideas combine well with existing methods for implementing functional languages, and the overall-goal of this project is to answer this question. Starting point of this proposal is on the one hand recent work on the optimal Lambdascope implementation based on context sharing (van Oostrom et al, 2004), and, on the other hand, the Haskell implementation developed at Utrecht University (Dijkstra, 2004). One of the open problems is whether the Lambdascope framework can be extended to efficiently represent and manipulate sets of mutually recursive definitions. A second problem we want to investigate is whether global program analysis can discover where Lambdascope-based approaches solve problems due to insufficient sharing (Hudak and Liu, 2007). Assuming that both questions can be solved, we also want to investigate how the Lambdascope-based implementations can be combined with more conventional frameworks, and how efficient the resulting implementations can be. The unique combination of the theoretical depth from the Logic department and the implementation skills and compiler infrastructure from the Computer Science department make Utrecht University the optimal surroundings for such a project. |
