When programming with sublinear space constraints one often needs to use special implementation techniques even for simple tasks, such as function composition. In this paper, we study how such implementation techniques can be supported in a functional programming language. Our approach is based on modelling computation by interaction using the Int construction of Joyal, Street & Verity. We apply this construction to a term model of a first-order programming language and use the resulting structure to derive the functional programming language intml. Intml can be understood as a programming language simplification of Stratified Bounded Affine Logic. We formulate intml by means of a type system inspired by Baillot & Terui's Dual Light Affine Logic. We show that it captures the complexity classes flogspace and nflogspace. We illustrate its expressiveness by showing how typical graph algorithms, such a test for acyclicity in undirected graphs, can be represented.
Computation by interaction for space-bounded functional programming / Dal Lago, Ugo; Schöpp, Ulrich. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - ELETTRONICO. - 248:(2016), pp. 150-194. [10.1016/j.ic.2015.04.006]
Computation by interaction for space-bounded functional programming
DAL LAGO, UGO;
2016
Abstract
When programming with sublinear space constraints one often needs to use special implementation techniques even for simple tasks, such as function composition. In this paper, we study how such implementation techniques can be supported in a functional programming language. Our approach is based on modelling computation by interaction using the Int construction of Joyal, Street & Verity. We apply this construction to a term model of a first-order programming language and use the resulting structure to derive the functional programming language intml. Intml can be understood as a programming language simplification of Stratified Bounded Affine Logic. We formulate intml by means of a type system inspired by Baillot & Terui's Dual Light Affine Logic. We show that it captures the complexity classes flogspace and nflogspace. We illustrate its expressiveness by showing how typical graph algorithms, such a test for acyclicity in undirected graphs, can be represented.File | Dimensione | Formato | |
---|---|---|---|
intml2_singlespaced.pdf
accesso aperto
Tipo:
Postprint
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione - Non commerciale - Non opere derivate (CCBYNCND)
Dimensione
1.28 MB
Formato
Adobe PDF
|
1.28 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.