Space improvements and equivalences in a polymorphically typed functional core language: context lemmas and proofs
- We explore space improvements in LRP, a polymorphically typed call-by-need functional core language. A relaxed space measure is chosen for the maximal size usage during an evaluation. It Abstracts from the details of the implementation via abstract machines, but it takes garbage collection into account and thus can be seen as a realistic approximation of space usage. The results are: a context lemma for space improving translations and for space equivalences; all but one reduction rule of the calculus are shown to be space improvements, and the exceptional one, the copy-rule, is shown to increase space only moderately. Several further program transformations are shown to be space improvements or space equivalences, in particular the translation into machine expressions is a space equivalence. These results are a step Forward in making predictions about the change in runtime space behavior of optimizing transformations in callbyneed functional languages.
Author: | Manfred Schmidt-SchaußORCiDGND, Nils DallmeyerGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-437660 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-57.pdf |
Parent Title (English): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 57 |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (57) |
Publisher: | Goethe-University |
Place of publication: | Frankfurt |
Document Type: | Working Paper |
Language: | English |
Year of Completion: | 2017 |
Year of first Publication: | 2017 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2017/08/01 |
Issue: | 2017 July, 20 |
Page Number: | 37 |
First Page: | 2 |
Last Page: | 37 |
HeBIS-PPN: | 415275598 |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Licence (German): | Deutsches Urheberrecht |