Redexes are stable in the λ-calculus

摘要

In the theory of sequential programming languages, Berry’s stability property is anrnimportant step claiming that values have unique origins in their calculations. It has beenrnshown that Bohm trees are stable in the λ-calculus, meaning that there is a unique minimumrnprefix of any lambda term which computes its Bohm tree. Moreover this property is alsorntrue for finite prefixes of Bohm trees. The proof relies on Curry’s standardization theorem asrninitially pointed out by Plotkin in his famous article LCF considered as a programmingrnlanguage. In this paper we will show that the stability property also holds for redexes.rnNamely for any redex family, there is a unique minimum calculation and a unique redexrnwhich computes this family. This property was already known in the study of optimalrnreductions, but we stress here on stability and want to show that stability is inside the basicrnobjects of calculations. The proof will be based on nice commutations between residuals andrncreations of new redexes. Our tool for proving this property will be the labelled lambdarncalculus used in the study of optimal reductions.