Maximal sharing in the lambda calculus with letrec

DOI10.1145/2628136.2628148MaRDI QIDQ2819667zbMATH OpenOpenAlexFDO

Authors Clemens Grabmayer, Jan Rochel

Publication date 29 September 2016

Published in Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.1460

zbMATH Keywords

higher-order term graphslambda calculus with letrecmaximal sharingsubterm sharingunfolding semantics

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Abstract: Increasing sharing in programs is desirable to compactify the code, and to avoid duplication of reduction work at run-time, thereby speeding up execution. We show how a maximal degree of sharing can be obtained for programs expressed as terms in the lambda calculus with letrec. We introduce a notion of `maximal compactness' for lambda-letrec-terms among all terms with the same infinite unfolding. Instead of defined purely syntactically, this notion is based on a graph semantics. lambda-letrec-terms are interpreted as first-order term graphs so that unfolding equivalence between terms is preserved and reflected through bisimilarity of the term graph interpretations. Compactness of the term graphs can then be compared via functional bisimulation. We describe practical and efficient methods for the following two problems: transforming a lambda-letrec-term into a maximally compact form; and deciding whether two lambda-letrec-terms are unfolding-equivalent. The transformation of a lambda-letrec-term $L$ into maximally compact form $L_0$ proceeds in three steps: (i) translate L into its term graph $G=[[L]]$; (ii) compute the maximally shared form of $G$ as its bisimulation collapse $G_0$; (iii) read back a lambda-letrec-term $L_0$ from the term graph $G_0$ with the property $[[L_0]]=G_0$. This guarantees that $L_0$ and $L$ have the same unfolding, and that $L_0$ exhibits maximal sharing. The procedure for deciding whether two given lambda-letrec-terms $L_1$ and $L_2$ are unfolding-equivalent computes their term graph interpretations $[[L_1]]$ and $[[L_2]]$, and checks whether these term graphs are bisimilar. For illustration, we also provide a readily usable implementation.

Recommendations

• A general theory of sharing graphs
• scientific article; zbMATH DE number 1523048
• Repetitive reduction patterns in lambda calculus with \texttt{letrec} (work in progress)
• scientific article; zbMATH DE number 1088036
• A unified approach to fully lazy sharing

Cited in

(8)

• Expressibility in the lambda calculus with
• Term graph representations for cyclic \(\lambda\)-terms
• Repetitive reduction patterns in lambda calculus with \texttt{letrec} (work in progress)
• Nested term graphs (work in progress)
• Modeling terms by graphs with structure constraints (two illustrations)
• scientific article; zbMATH DE number 7456061 (Why is no real title available?)
• Properties of a first-order functional language with sharing
• From compactifying lambda-letrec terms to recognizing regular-expression processes (extended abstract and literature)

This page was built for publication: Maximal sharing in the lambda calculus with letrec

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819667)