Strong normalization in a non-deterministic typed lambda-calculus

Abstract

In a previous paper [4], we introduced a non-deterministic λ-calculus (λ-LK) whose type system corresponds exactly to Gentzen’s cut-free LK [9]. This calculus, however, cannot be provided with a computational interpretation. Some of the constructs act as oracles and, for this reason, it is not possible to define an effective notion of reduction. In the present paper, we address this problem. We consider a weak version of the implicative fragment of λ-LK, and we define for it a relation of reduction that models, at the level of the terms, the appropriate proof-theoretic notion of proof reduction. This reduction relation satisfies several properties of interest, among others, the property of strong normalization. We prove this last result by using a reducibility argument à la Tait.