Token-passing Optimal Reduction with Embedded Read-back

TL;DR

This paper presents a novel interaction net implementation of optimal reduction for untyped lambda calculus that guarantees reaching normal form regardless of strategy, featuring token-passing and embedded read-back mechanisms.

Contribution

It introduces a token-passing interaction net approach with a non-deterministic extension, enabling normal form achievement and integrated read-back without leaving the formalism.

Findings

Guarantees reaching normal form regardless of reduction strategy

Integrates read-back mechanism within interaction nets

Demonstrates effectiveness of token-passing approach

Abstract

We introduce a new interaction net implementation of optimal reduction for the pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of the interaction net reduction strategy using the approach of so-called token-passing nets and a non-deterministic extension for interaction nets. Another new feature is the read-back mechanism implemented without leaving the formalism of interaction nets.