2
$\begingroup$

The set of lambda calculus expressions $Expr$ is generated by the grammar $$ Expr \ni e ::= x \mid \lambda x\ldotp e \mid e_1 e_2 $$

We can define an interpreter without explicit substitution by using environments and closures: $$ \begin{align*} Env &= Var \rightharpoonup Cl &\text{($\rightharpoonup$ is partial function space)}\\ Cl &= Env \times Expr \end{align*} $$

The evaluation function $eval : Env \times Expr \to Cl$ sends each expression in a given environment to an evaluated closure:

$$ \begin{align*} eval_\rho(x) =& \rho(x) \\ eval_\rho(\lambda x\ldotp e) =& (\rho, \lambda x\ldotp e) \\ eval_\rho(e_1 e_2) =& \mathrm{let~}eval_\rho(e_1) = (\rho', \lambda x\ldotp e_1') \\ & \mathrm{in~} eval_{\rho'[x \mapsto eval_\rho(e_2)]}(e_1') \end{align*} $$

Using substitution, a closure $(\rho, e) \in Cl$ can be expanded to yield the represented expression: $$F([x_1 \mapsto c_1, ..., x_n \mapsto c_n], e) = e[F(c_1)/x_1, ..., F(c_n)/x_n]$$ This however forgets all sharing. E.g., $F([x \mapsto ([], f)], x x) = f f$ duplicates the expression $f$, which might be very large. An alternative expansion retains sharing:

$$ G([x_1 \mapsto e_1, ..., x_n \mapsto e_n],e) = (\lambda x_1 \ldotp \cdots (\lambda x_n \ldotp e) \cdots) ~G(e_1)~\cdots ~ G(e_n) $$

This on the other hand repeats definitions in nested scopes, e.g.: $$ G([x\mapsto ([],f), y \mapsto ([x \mapsto ([],f)], g)], x y) \\ = (\lambda x\ldotp \lambda y\ldotp xy)~(f)~((\lambda x\ldotp g)~f) $$ An equivalent but more economical expansion that doesn't duplicate $g$ would be $$ (\lambda x\ldotp (\lambda y\ldotp xy) g)~f $$ For practical purposes, if one wants to "render" a closure as a plain expression, both $F$ and $G$ are unsatisfactory: The closure environments can be efficiently represented by pointer datastructures that takes avantage of sharing, but most of that sharing seems to be lost with either approach.

  • Do you know of any efficient data structures and algorithms related to this problem?
  • Is this problem called something more specific in the literature? I tried search for "lambda calculus closure expansion", but without much success.
$\endgroup$
  • $\begingroup$ I'm not sure but it sounds somewhat like you'd be interested in "optimal evaluation" e.g. Lamping's work and work that descended from it. These discussions might point you at other related topics: reddit discussion, StackOverflow question $\endgroup$ – Derek Elkins Dec 15 '17 at 9:24
  • $\begingroup$ This definitely seems relevant, I wasn't aware of this work. Thank you! $\endgroup$ – Ulrik Rasmussen Dec 16 '17 at 6:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.