Proofs, lambda terms and control operators (Q4357067)

The so-called continuation-passing-style translation (cps-translation) has been introduced by \textit{M. Fischer} [``Lambda calculus schemata'', Sigplan Notices 7, 104-109 (1972)] for the \(\lambda\)-calculus and extended to the \(\lambda\)-calculus with control operators \({\mathcal C}\) and \({\mathcal A}\) by \textit{M. Felleisen}, \textit{D. P. Friedman}, \textit{E. Kohlbecker} and \textit{B. Duba} [Theor. Comput. Sci. 52, 205-237 (1987; Zbl 0643.03011)]. By giving a typing, a connection with implicational propositional logic has been established by \textit{A. R. Meyer} and \textit{M. Wand} [Lect. Notes Comput. Sci. 193, 219-224 (1985; Zbl 0565.68028)] for the \(\lambda\)-calculus and extended to the \(\lambda\)-calculus with control operators \({\mathcal C}\) and \({\mathcal A}\) by \textit{T. G. Griffin} [``A formulae-as-types notion of control'', Conf. Rec. 17th Ann. ACM Symp. Principles Program. Lang., 47-58 (1990)]. Griffin has shown that all evaluations with respect to call-by-value \(\beta\)-conversion and the standard conversion rules for \({\mathcal C}\) and \({\mathcal A}\) terminate. More precisely Griffin extends the Meyer/Wand typing of Fischer's cps-translation \(\overline M\) of a term \(M\) to the language involving the control operators \({\mathcal C}\) and \({\mathcal A}\). It still holds that if \(M\) has type \(A\), then \(\overline M\) has type \(\neg \neg A^0\), where \(A^0\) is defined as \(P^0:=P\) and \((A\to B)^0: =A^0\to \neg B^0 \to \text{F}\) (which is equivalent to \(\neg B^0 \to \neg A^0)\). Griffin's proof of termination of evaluation is based on \textit{G. D. Plotkin}'s [Theor. Comput. Sci. 1, 125-159 (1975; Zbl 0325.68006)] technique of the so-called colon-translation (denoted \(M:V\) and typed by \(M^A: V^{\neg A^0})\) and context unwrapping (denoted by \(V^E\) and typed by requiring \(V\) to be of type \(\neg B^0\), and the evaluation context \(E\square\) to be of type \(B\) with the `hole' of type \(A)\). Here we essentially give an exposition of Griffin's result, with some simplifications and extensions based on work of \textit{A. Sabry} and \textit{M. Felleisen} [``Reasoning about programs in continuation-passing style'', Lisp Symb. Comput. 6, 289-360 (1993)]. In particular we stress its connection with questions of termination of different normalization strategies for minimal, intuitionistic and classical logic, or more precisely their fragments in implicational propositional logic. We also give some examples (due to Hirokawa) of derivations in minimal and classical logic which reproduce themselves under certain reasonable conversion rules. For the entire collection see [Zbl 0869.00051].