On randomised strategies in the lambda-calculus

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 classical sub-lambda-calculi, namely those where duplication and erasure are syntactically forbidden.

In questo lavoro studiamo le strategie di riduzione randomizzate, una nozione già introdotta nel contesto nei sistemi astratti di riduzione. Sviluppiamo un semplice modello che permette di dimostrare che una strategia randomizzata è quasi certamente normalizzante positiva. Proponiamo in seguito un semplice esempio di strategia randomizzata per il lambda-calcolo che gode di questa proprietà e mostriamo perché è non banale rispetto alle classiche strategie deterministiche come leftmost-outermost o rightmost-innermost. Studiamo inoltre questa strategia per due sotto-lambda-calcoli, in particolare quelli in cui copia e cancellazioni sono impediti per via sintattica.