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 sub-lambda-calculi, namely those where duplication and erasure are syntactically forbidden, showing some non-trivial properties. (C) 2019 Elsevier B.V. All rights reserved.