Functional Programming in Sublinear Space
Ulrich Schoepp ( LMU Munich )
- 14:00 4th December 2009 ( week 8, Michaelmas Term 2009 )Lecture Theatre B
Functional Programming in Sublinear Space (joint work with Ugo Dal Lago)
We consider the problem of functional programming with data in external memory, in particular as it appears in sublinear space computation. Writing programs with sublinear space usage often
requires one to use special implementation techniques for otherwise easy tasks, e.g. one cannot compose functions directly for lack of space for the intermediate result, but must instead compute and recompute small parts of the intermediate result on demand. In this paper, we study how the implementation of such techniques can be supported by functional programming languages.
Our approach is based on modelling computation by interaction using the Int construction of Joyal, Street & Verity. We use the Int construction to capture computation with bidirectional data flow, as it appears in sublinear space computation. We derive functional programming constructs by applying the Int construction to a term model of a given functional language. The thus derived functional language is formulated by means of a type system inspired Baillot & Terui's Dual Light Affine Logic. We show that it captures LOGSPACE. In order to assess the expressiveness of the language, we consider how typical LOGSPACE-algorithms on graphs and words can be expressed; we consider a test for acyclicity in undirected graphs as well as Moeller-Neergaard's program for sublinear space iteration by computational amnesia.
We consider the problem of functional programming with data in external memory, in particular as it appears in sublinear space computation. Writing programs with sublinear space usage often
requires one to use special implementation techniques for otherwise easy tasks, e.g. one cannot compose functions directly for lack of space for the intermediate result, but must instead compute and recompute small parts of the intermediate result on demand. In this paper, we study how the implementation of such techniques can be supported by functional programming languages.
Our approach is based on modelling computation by interaction using the Int construction of Joyal, Street & Verity. We use the Int construction to capture computation with bidirectional data flow, as it appears in sublinear space computation. We derive functional programming constructs by applying the Int construction to a term model of a given functional language. The thus derived functional language is formulated by means of a type system inspired Baillot & Terui's Dual Light Affine Logic. We show that it captures LOGSPACE. In order to assess the expressiveness of the language, we consider how typical LOGSPACE-algorithms on graphs and words can be expressed; we consider a test for acyclicity in undirected graphs as well as Moeller-Neergaard's program for sublinear space iteration by computational amnesia.
Share this:
