On randomised strategies in the $\lambda$-calculus (long version)

TL;DR

This paper explores randomised reduction strategies in the lambda-calculus, providing a framework to prove their almost-sure normalisation and analyzing their properties compared to classical strategies.

Contribution

It introduces a framework for analyzing randomised strategies in lambda-calculus and demonstrates a non-trivial example with almost-sure normalisation.

Findings

A simple randomised strategy is almost-surely normalising.

The strategy differs from classical deterministic strategies.

Properties are studied in sub-calculi with restricted operations.

Abstract

In this work we study randomised reduction strategies,a notion already known in the context of abstract reduction systems, for the $\lambda$-calculus. We develop a simple framework that allows us to prove a randomised strategy to be positive almost-surely normalising. Then we propose a simple example of randomised strategy for the $\lambda$-calculus that has such a property and we show why it is non-trivial with respect to classical deterministic strategies such as leftmost-outermost or rightmost-innermost. We conclude studying this strategy for two sub-$\lambda$-calculi, namely those where duplication and erasure are syntactically forbidden, showing some non-trivial properties.