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 modeling computation by interaction using the Int construction of Joyal, Street & Verity. We derive functional programming constructs from the structure obtained 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 by Baillot & Terui’s Dual Light Affine Logic. We assess its expressiveness by showing that it captures LOGSPACE.
Titolo: | Functional Programming in Sublinear Space |
Autore/i: | DAL LAGO, UGO; U. Schoepp |
Autore/i Unibo: | |
Anno: | 2010 |
Titolo del libro: | Lecture Notes in Computer Science |
Pagina iniziale: | 205 |
Pagina finale: | 225 |
Abstract: | 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 modeling computation by interaction using the Int construction of Joyal, Street & Verity. We derive functional programming constructs from the structure obtained 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 by Baillot & Terui’s Dual Light Affine Logic. We assess its expressiveness by showing that it captures LOGSPACE. |
Data prodotto definitivo in UGOV: | 23-feb-2011 |
Appare nelle tipologie: | 4.01 Contributo in Atti di convegno |