# Sharing Equality is Linear

## TL;DR

This paper introduces the first linear-time algorithm for checking equality of shared lambda-terms, significantly improving previous polynomial bounds by leveraging DAG representations and bisimulation techniques.

## Contribution

It presents a novel linear-time algorithm for sharing equality of lambda-terms, enhancing efficiency over existing polynomial-time methods.

## Key findings

- First linear-time sharing equality algorithm for lambda-terms
- Uses DAG representation and bisimulation techniques
- Improves computational bounds from polynomial to linear

## Abstract

The $\lambda$-calculus is a handy formalism to specify the evaluation of higher-order programs. It is not very handy, however, when one interprets the specification as an execution mechanism, because terms can grow exponentially with the number of $\beta$-steps. This is why implementations of functional languages and proof assistants always rely on some form of sharing of subterms. These frameworks however do not only evaluate $\lambda$-terms, they also have to compare them for equality. In presence of sharing, one is actually interested in the equality---or more precisely $\alpha$-conversion---of the underlying unshared $\lambda$-terms. The literature contains algorithms for such a sharing equality, that are polynomial in the sizes of the shared terms. This paper improves the bounds in the literature by presenting the first linear time algorithm. As others before us, we are inspired by Paterson and Wegman's algorithm for first-order unification, itself based on representing terms with sharing as DAGs, and sharing equality as bisimulation of DAGs.