A token-passing net implementation of optimal reduction with embedded read-back

TL;DR

This paper presents a novel token-passing net implementation of optimal reduction for untyped lambda calculus, enabling strategy-independent normalization and integrated read-back within interaction nets.

Contribution

It introduces a token-passing net approach for optimal reduction with embedded read-back, enhancing flexibility and formalism integration.

Findings

Achieves normal form regardless of reduction strategy

Integrates read-back mechanism within interaction nets

Demonstrates effectiveness for pure untyped lambda calculus

Abstract

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