Optimal Reduction without Oracle?

TL;DR

This paper presents a new interaction net approach for optimal reduction of untyped lambda calculus that does not rely on an oracle, supporting more lambda terms and reducing interactions compared to previous methods.

Contribution

It introduces an oracle-free interaction net implementation that handles a broader class of lambda terms and improves efficiency over existing closed reduction methods.

Findings

Supports a wider class of lambda terms

Reduces total interactions compared to previous implementations

Eliminates the need for an oracle in optimal reduction

Abstract

We suggest an approach to solve the problem of matching fans in interaction net implementations of optimal reduction for the pure untyped lambda calculus without use of any additional agent types. Our implementation supports a wider class of lambda terms than the abstract version of Lamping's algorithm and beats the interaction net implementation of closed reduction by the total number of interactions.