Strong Normalization in a Non-Deterministic Typed Lambda-Calculus

10 years 3 days ago
Strong Normalization in a Non-Deterministic Typed Lambda-Calculus
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 `a la Tait.
Philippe de Groote
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1994
Where LFCS
Authors Philippe de Groote
Comments (0)