# Crumbling Abstract Machines

## TL;DR

This paper investigates how sharing-based term representations in lambda-calculus influence the design and efficiency of call-by-value abstract machines, demonstrating no slowdown and scalability to open terms.

## Contribution

It introduces a sharing-based term representation that simplifies machine design and proves it scales efficiently to open terms, unlike continuation-passing style transformations.

## Key findings

- No slowdown in evaluation performance.
- Simplifies abstract machine design by removing environment structures.
- Scales effectively to open terms used in proof assistants.

## Abstract

Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where applications have only values as immediate subterms. This work studies how such a crumbled representation of terms impacts on the design and the efficiency of abstract machines for call-by-value evaluation. About the design, it removes the need for data structures encoding the evaluation context, such as the applicative stack and the dump, that get encoded in the environment. About efficiency, we show that there is no slowdown, clarifying in particular a point raised by Kennedy, about the potential inefficiency of such a representation. Moreover, we prove that everything smoothly scales up to the delicate case of open terms, needed to implement proof assistants. Along the way, we also point out that continuation-passing style transformations--that may be alternatives to our representation--do not scale up to the open case.