In this work we study randomised reduction strategies—a notion already known in the context of abstract reduction systems—for the λ-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 λ-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-λ-calculi, namely those where duplication and erasure are syntactically forbidden, showing some non-trivial properties.
Dal Lago U., Vanoni G. (2020). On randomised strategies in the λ-calculus. THEORETICAL COMPUTER SCIENCE, 813, 100-116 [10.1016/j.tcs.2019.09.033].
On randomised strategies in the λ-calculus
Dal Lago U.
;Vanoni G.
2020
Abstract
In this work we study randomised reduction strategies—a notion already known in the context of abstract reduction systems—for the λ-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 λ-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-λ-calculi, namely those where duplication and erasure are syntactically forbidden, showing some non-trivial properties.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
