Sub-λ-calculi, Classified

AbstractWhen sharing is studied in the λ-calculus, some sub-calculi often pop up, for instance λI or the linear λ-calculus. In this paper, we generalise these to a large class of sub-calculi, parametrised by an arbitrary predicate on the number of occurrences of bound variables. Such a definition only makes sense when the sub-calculi are stable by β-reduction. Surprisingly, we are able to give a complete description and classification of such stable sub-calculi, in a rather algebraic way; and surprisingly again, we discover some unexpected such subcalculi. This could lead to a better understanding of the structure of the λ-calculus