A deconstruction of non-deterministic classical cut elimination. (English) Zbl 0981.03057
Abramsky, Samson (ed.), Typed lambda calculi and applications. 5th international conference, TLCA 2001, Kraków, Poland, May 2-5, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2044, 268-282 (2001).
Summary: This paper shows how a symmetric and non-deterministic cut elimination procedure for a classical sequent calculus can be faithfully simulated using a non-deterministic choice operator to combine different ‘double-negation’ translations of each cut. The resulting interpretation of classical proofs in a \(\lambda\)-calculus with non-deterministic choice leads to a simple proof of termination for cut elimination.
For the entire collection see [Zbl 0961.00016].
For the entire collection see [Zbl 0961.00016].
