Computation by interaction for space-bounded functional programming

Ugo Dal Lago 1, 2 Ulrich Schöpp 3
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We consider the problem of supporting sublinear space programming in a functional programming language. 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 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 core functional language intml is formulated by means of a type system inspired by Baillot & Terui's Dual Light Affine Logic. It can be understood as a programming language simplification of Stratified Bounded Affine Logic. We show that it captures the classes flogspace and nflogspace of the functions computable in deterministic logarithmic space and in non-deterministic logarithmic space, respectively. We illustrate the expressiveness of intml by showing how typical graph algorithms, such a test for acyclicity in undirected graphs, can be represented in it.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2016, 248, 〈10.1016/j.ic.2015.04.006〉
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01337724
Contributeur : Ugo Dal Lago <>
Soumis le : lundi 27 juin 2016 - 14:55:17
Dernière modification le : jeudi 11 janvier 2018 - 15:50:33

Fichier

intml2_singlespaced.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Ugo Dal Lago, Ulrich Schöpp. Computation by interaction for space-bounded functional programming. Information and Computation, Elsevier, 2016, 248, 〈10.1016/j.ic.2015.04.006〉. 〈hal-01337724〉

Partager

Métriques

Consultations de la notice

154

Téléchargements de fichiers

44