The logical essence of compiling with continuations

The Logical Essence of Compiling With Continuations José Espírito Santo # Centre of Mathematics, University of Minho, Portugal Filipa Mendes # Centre of Mathematics, University of Minho, Portugal Abstract The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi’s computational lambda-calculus ( λ C), we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation reconstructs the original CPS-translation. Going back to direct style, the “essence” of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another one, the continuation-enclosing style (CES): such an alternative is due to a dilemma in the syntax of λ C, concerning how to expand the application constructor. In the typed scenario, VES and CES correspond to an alternative between two proof systems for call-by-value, LJQ and natural deduction with generalized applications, confirming proof theory as a foundation for intermediate representations. 2012 ACM Subject Classification Theory of computation → Proof theory; Theory of computation →Operational semantics; Theory of computation →Type structures Keywords and phrases Continuation-passing style, Sequent calculus, Generalized applications, Administrative normal form Digital Object Identifier 10.4230/LIPIcs.FSCD.2023.15 Related Version Full Version:https://arxiv.org/abs/2304.14752 Funding The first author was partially financed by Portuguese Funds through FCT (Fundação para a Ciência e a Tecnologia) within the Projects UIDB/00013/2020 and UIDP/00013/2020 1 Introduction The conversion of a program in a source call-by-value language to continuation-passing style (CPS) by an optimizing translation that reduces on the fly the so-called administrative redexes produces programs which can be translated back to direct style, so that the final result, obtained by composing the two stages of translation, is a new program in the source language which can be obtained from the original one by reduction to administrative normal form (ANF) – a program transformation in the source language [ 10 , 24 ]. This fact has been dubbed the “essence” of compiling with continuations and has had a big impact and generated an on-going debate in the theory and practice of compiler design [11, 16, 18]. Our starting point is the refinement of that “essence”, obtained in [ 25 ], in the form of a reflection of the CPS target in the computational λ -calculus [ 20 ], the latter playing the role of source language and here denoted λ C– see Fig. 1. Then we ask: What is the proof-theoretical meaning of this reflection? What is the logical reading of this reflection in the typed setting? Of course, the CPS-translation has a well-known logical reading as a ©José Espírito Santo and Filipa Mendes; licensed under Creative Commons License CC-BY 4.0 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 15:2 The Logical Essence of Compiling With Continuations λC admin  CPS-translation $$ ANF kernel of CPS-translation//CPS inverse CPS-translation oo Direct Style Continuation-Passing Style Figure 1 The essence of compiling with continuations negative translation, based on the introduction of double negations, capable of translating a classical source calculus with control operators [ 19 , 12 , 26 ]. But it is not clear how this reading is articulated with the reflection in Fig.1, which provides a decomposition of the CPS-translation as the reduction to ANF followed by a “kernel” translation that relates the “kernel” ANF with CPS. It is also well-known that the CPS-translation can be decomposed in several ways: indeed in the reference [ 25 ] alone we may find two of them, one through the monadic meta-language [ 21 ], the other through the linear λ -calculus [ 17 ]. Here we will propose another intermediate language, the sequent calculus LJQ [ 3 , 4 ]. The calculus LJQ has a long history and several applications in proof theory [ 3 ] and can be turned into a typed call-by-value λ -calculus in equational correspondence with λ C[ 4 ]. Here we want to show it has a privileged role as a tool to analyze the CPS-translation. Languages of proof terms for the sequent calculus handle contexts (i.e. λ -terms with a hole) formally [ 13 , 1 , 8 , 5 ]. This seems most convenient, since a continuation may be seen as a certain kind of context, and suggests that we can write an alternative translation into the sequent calculus, as if we were CPS-translating, but without the need to pass around a reification of the current continuation as a λ -abstraction, nor the concomitant need to translate types by the insertion of double negations, to make room for a type A∼ of values, a type ¬A∼of continuations and a type ¬¬A∼of programs, out of a source type A. We develop this in detail, which requires: to rework entirely the term calculus for LJQ and obtain a system, named λQ , more manageable for our purposes; and to identify the kernel and the sub-kernel of λQ , the latter being the target system, named V FS after value-filling style, of the new translation. In the end, we are rewarded with an isomorphism between V FS and the target of the CPS-translation, which, when composed with the alternative translation, reconstructs the CPS-translation. The isomorphism is a negative translation, reduced to the role of optional and late stage of translation. Going back to direct style, the “essence” of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another sublanguage of ANF, the continuation-enclosing style (CES): such alternative between VES and CES is due to a dilemma in the syntax of λ C, concerning how to expand the application constructor. Hence, José Espírito Santo and Filipa Mendes 15:3 λC admin  CPS-translation  VFS-translation (((( LJQ admin  ANF LNF CPS V ES  V ES ∼ =//V FSnegative translation ∼ =////CP S  CES ∼ =//CNF ∼ =//CP S Direct Style Generalized Applications Sequent Calculus Continuation-Passing Style Figure 2 The logical essence of compiling with continuations these two sub-kernels of λ Care under a layer of expansion – and the same was already true for the passage from the kernel to the sub-kernel of λQ. While VES corresponds to the sub-kernel VFS of λQ , CES corresponds to a fragment of λ J v [ 6 ], a call-by-value λ -calculus with generalized applications; the fragment is that of commutative normal forms (CNF), that is, normal forms w. r. t. the commutative conversions, naturally arising when application is generalized, which reduce both the head term and the argument in an application to the form of values. So the alternative between VES and CES is also a reflection, in the source language, of the alternative between two proof systems for call-by-value: the sequent calculus LJQ and the natural deduction system behind λJv. A summary is contained in Fig. 2: it shows a proof-theoretical background hidden in Fig. 1, which this paper wants to reveal. In the process, we want to confirm proof theory as a foundation for intermediate representations useful in the compilation of functional languages. Plan of the paper. Section 2 recalls λ Cand the CPS-translation. Section 3 contains our reworking of LJQ . Section 4 introduces the alternative translation into LJQ and the decomposition of the CPS-translation. Section 5 goes back to direct style and studies the sub-kernels of λ C. Section 6 summarizes our contribution and discusses related and future work. All proofs can be found in the long version of this paper [7]. 2 Background Preliminaries. Simple types (=formulas) are given by A, B, C ::= a|A⊃B . In typing systems, a context Γwill always be a consistent set of declarations x : A ; consistency here means that no variable can be declared with two different types in Γ. We recall the concepts of equational correspondence, pre-Galois connection and reflection [4, 24, 25] characterizing different forms of relationship between two calculi. ▶ Definition 1. Let (Λ 1,→1 )and (Λ 2,→2 )be two calculi and, for each i = 1 , 2, let ↠i FSCD 2023 15:4 The Logical Essence of Compiling With Continuations (resp. ↔i ) be the reflexive-transitive (resp. reflexive-transitive-symmetric) closure of →i . Consider the mappings f: Λ1→Λ2and g: Λ2→Λ1. f and g form an equational correspondence between Λ 1 and Λ 2 if the following conditions hold: (1) If M→1N then f ( M ) ↔2f ( N ); (2) If M→2N then g ( M ) ↔1 g(N); (3) M↔1g(f(M)); (4) f(g(M)) ↔2M. f and g form a pre-Galois connection from Λ 1 to Λ 2 if the following conditions hold: (1) If M→1N then f ( M ) ↠2f ( N ); (2) If M→2N then g ( M ) ↠1g ( N ); (3) M↠1g(f(M)). f and g form a reflection in Λ 1 of Λ 2 if the following conditions hold: (1) If M→1N then f ( M ) ↠2f ( N ); (2) If M→2N then g ( M ) ↠1g ( N ); (3) M↠1g ( f ( M )); (4) f(g(M)) = M. Note that if f and g form a pre-Galois connection from Λ 1 to Λ 2 and →2 is confluent, then →1 is also confluent. Besides, it is also important to observe that if f and g form a reflection from Λ1to Λ2, then gand fform a pre-Galois connection from Λ2to Λ1. Computational lambda-calculus. The computational λ -calculus [ 20 ] is defined in Table 1. In addition to ordinary λ -terms, one also has let-expressions let x := Min N : these are explicit substitutions which trigger only after the actual parameter M is reduced to a value (that is, a variable or λ -abstraction). So, in addition to the rule letv that triggers substitution, there are reduction rules – let1 , let2 and assoc – dedicated to that preliminary reduction of actual parameters in let-expressions. For the reduction of β -redexes, we adopt the rule B from [ 4 ], which triggers even if the argument N is not a value, and just generates a let-expression. Most presentations of λ C [ 20 , 25 ] have rule βv instead, which reads ( λx.M ) V→ [ V/x ] M . The two versions of the system are equivalent. In our presentation, the effect of βv is achieved with B followed by letv. Conversely, when Nis not a value, we can perform the reduction (λx.M)N→let y:= Nin (λx.M)y→let y:= Nin [y/x]M=αlet x:= Nin M . The first step is by let2, the second by βv. The last term is the contractum of B. In this paper, we leave the η -rule for λ -abstraction out of the definition of λ C, and similarly for other systems – since it plays no rule in what we want to say. But we include the η-rule for let-expressions, and other incarnations of it in other systems. In [ 4 , 25 ] the λ C-calculus is studied in its untyped version. Here we will also consider its simply-typed version, which handles sequents Γ ⊢CM : A , where Γis a set of declarations x : A . The typing rules are obvious, Table 1 only contains the rule for typing let-expressions. The kernel of the computational λ -calculus [ 25 ] is defined in Table 2. It is named here ANF , after “administrative normal form”, because its terms are the normal forms w. r. t. the administrative rules of λC:let1,let2and assoc [25]. In the kernel, only a specific form of applications and two forms of let-expressions are primitive. The general form of a let-expression, written LET y := Min P , is a derived form defined by recursion on Mas follows: LET y:= Vin P=let y:= Vin P LET y:= V W in P=let y:= V W in P LET y:= (let x:= Vin M)in P=let x:= Vin LET y:= Min P LET y:= (let x:= V W in M)in P=let x:= V W in LET y:= Min P Obviously, given M and P in the kernel, let y := Min P↠assoc LET y := Min P in λ C. Hence, a Bv -step in the kernel can be simulated in λ Cas a B -step followed by a series of José Espírito Santo and Filipa Mendes 15:5 (terms) M, N, P, Q ::= V|MN |let x:= Min N (values) V, W ::= x|λx.M (B) (λx.M)N→let x:= Nin M (letv)let x:= Vin M→[V/x]M (ηlet)let x:= Min x→M (assoc)let y:= (let x:= Min N)in P→let x:= Min let y:= Nin P (let1)MN →let x:= Min xN (a) (let2)V N →let x:= Nin V x (b) Γ⊢CM:AΓ, x :A⊢CN:B Γ⊢Clet x:= Min N:B Table 1 The computational λ -calculus, here also named λ C-calculus. Provisos: ( a ) M is not a value. (b)Nis not a value. Typing rules for x,λx.M and MN as usual. (terms) M, N, P, Q ::= V|V W |let x:= Vin M|let x:= V W in M (values) V, W ::= x|λx.M (Bv)let y:= (λx.M)Vin P→let x:= Vin LET y:= Min P (B′ v) (λx.M)V→let x:= Vin M (letv)let x:= Vin M→[V/x]M (ηlet)let x:= V W in x→V W Table 2 The kernel of the computational λ-calculus, here named ANF. FSCD 2023 15:6 The Logical Essence of Compiling With Continuations assoc -steps. On the other hand B′ v is a restriction of rule B to the sub-syntax, and the same is true of the remaining rules of the kernel. Notice that in the form let x := V W in M the immediate sub-expressions are V , W and M – but not V W . For this reason, there is no overlap between the redexes of rules Bv and B′ v, nor between the redexes of rules B′ vand ηlet. Our presentation of the kernel is very close to the original one in [ 25 ], as detailed in Appendix B. CPS-translation. We present in this subsection the call-by-value CPS-translation of λ C. It is a “refined ” translation [ 4 ], in the sense that it reduces “administrative redexes” at translation time, as already done in [23]. The target of the translation is the system CP S , presented in Table 3. This target is a subsystem of the λ -calculus (or of Plotkin’s call-by-value λv -calculus – the “indifference property” [ 23 ]), whose expressions are the union of four different classes of λ -terms (commands, continuations, values and terms), and whose reduction rules are either particular cases of rules β and η (the cases of σv or ηk , respectively), or are derivable as two β -steps (the case of βv ). Each command or continuation has a unique free occurrence of k , which is a fixed (in the calculus) continuation variable. A term is obtained by abstracting this variable over a command. A command is always composed of a continuation K , to which a value may be passed (the form KV ), or which is going to instantiate k in the command resulting from an application V W (the form V WK). There is a simply-typed version of this target, not found in [ 23 , 4 , 25 ], defined as follows. Simple types are augmented with a new type ⊥ , and we adopt the usual abbreviation ¬A := A⊃⊥ . Then, as defined in Table 3, one has: two subclasses of such types, one ranged by A , A′ and the other ranged over by B , B′ ; four kinds of sequents, one per each syntactic class; and one typing rule for each syntactic constructor. The CPS-translation is defined in Table 4. It comprises: For each V∈λ C, a value V† ; for each term M∈λ Cand continuation K∈CP S , a command ( M : K ); for each term M∈λC, a command M⋆and a term M. In the typed setting, each simple type A of λ Cdetermines an A -type A† and a B -type A , as in Table 4. The translation preserves typing, according to the admissible typing rules displayed in the last row of the same table. 3 Sequent calculus LJQ and its simplification λQ In this section we start by recapitulating the term calculus for LJQ designed by DyckhoffLengrand [ 4 ]. Next we do some preliminary work, by proposing a simplified variant, named λQ , more appropriate for our purposes in this paper. Finally, we also single out the kernel of λQ , which is the sub-calculus of “administrative” normal forms. This further simplification will be necessary for the later analysis of CPS. The original term calculus. An abridged presentation of the original term calculus for LJQ by Dyckhoff-Lengrand is found in Table 5 1 . The separation between terms and values corresponds to the separation between the two kinds of sequents handled by LJQ : the ordinary sequents Γ ⇒M : A and the focused sequents Γ →V : A . There are three forms of cut and the reduction rules correspond to cut-elimination rules. We may think of the forms C 1 ( V, x.W )and C 2 ( V, x.N )as explicit substitutions: in this abridged presentation we omitted the rules for their stepwise execution. 1See Appendix A for the full system. José Espírito Santo and Filipa Mendes 15:7 (Commands) M, N ::= KV |V WK (Continuations) K::= λx.M |k (Values) V, W ::= λx.P |x (Terms) P::= λk.M (σv) (λx.M)V→[V/x]M (βv) (λxk.M)W K →[K/k][W/x]M (ηk)λx.Kx →Kif x /∈FV (K) Types: A::= a|A⊃B B ::= ¬¬A Contexts Γ: sets of declarations (x:A) Sequents: k:¬A,Γ⊢CPS M:⊥k:¬A,Γ⊢CPS K:¬A′Γ⊢CPS V:AΓ⊢CPS P:B k:¬A,Γ⊢CPS K:¬A′Γ⊢CPS V:A′ k:¬A,Γ⊢CPS KV :⊥ Γ⊢CPS V:A⊃ ¬¬A′Γ⊢CPS W:Ak:¬A′′,Γ⊢CPS K:¬A′ k:¬A′′,Γ⊢CPS V W K :⊥ k:¬A,Γ, x :A′⊢CPS M:⊥ k:¬A,Γ⊢CPS λx.M :¬A′k:¬A,Γ⊢CPS k:¬A Γ, x :A⊢CPS P:B Γ⊢CPS λx.P :A⊃BΓ, x :A⊢CPS x:A k:¬A,Γ⊢CPS M:⊥ Γ⊢CPS λk.M :¬¬A Table 3 The system CPS x†=x(V:K) = KV † (λx.M)†=λx.M (PQ :K)=(P:λm.(mQ :K)) (a) M=λk.M⋆(V Q :K)=(Q:λn.(V n :K)) (b) M⋆= (M:k) (V W :K) = V†W†K (let y:= Min P:K)=(M:λy.(P:K)) A=¬¬A†a†=a(A⊃B)†=A†⊃B Γ⊢CV:A Γ†⊢CPS V†:A Γ⊢CM:A k :¬B†,Γ⊢CPS K:¬A† k:¬B†,Γ†⊢CPS (M:K) :⊥ Γ⊢CM:A k:¬A†,Γ†⊢CPS M⋆:⊥ Γ⊢CM:A Γ†⊢CPS M:A Table 4 The CPS-translation, from λ Cto CPS , with admissible typing rules. Provisos: ( a ) P is not a value. (b)Qis not a value. FSCD 2023 15:8 The Logical Essence of Compiling With Continuations (terms) M, N ::= ↑V|x(V, y.N)|C2(V, x.N)|C3(M, x.N) (values) V, W ::= x|λx.M |C1(V, x.W) (1) C3(↑(λx.M), y.y(V, z.N)) →C3(C3(↑V, x.M), z.N) (a) (2) C3(↑x, y.N)→[x/y]N (3) C3(M, x. ↑x)→M (4) C3(z(V, y.P), x.N)→z(V, y.C3(P, x.N)) (5) C3(C3(↑W, y.y(V, z.P)), x.N)→C3(↑W, y.y(V, z.C3(P, x.N))) (b) (6) C3(C3(M, y.P ), x.N)→C3(M, y.C3(P, x.N)) (c) (7) C3(↑(λx.M), y.N)→C2(λx.M, y.N) (d) Γ, x :A→x:AAx Γ→V:A Γ⇒↑V:ADer Γ, x :A⇒M:B Γ→λx.M :A⊃BR⊃Γ⇒M:AΓ, x :A⇒N:B Γ⇒C3(M, x.N) : BCut3 Γ, x :A⊃B→V:AΓ, x :A⊃B, y :B⇒N:C Γ, x :A⊃B⇒x(V, y.N) : CL⊃ Table 5 The original calculus by Dyckhoff-Lengrand, here named λLJQ -calculus (abridged). Provisos: ( a ) y /∈FV ( V ) ∪FV ( N ).( b ) y /∈FV ( V ) ∪FV ( P )).( c )If rule (5) does not apply. ( d )If rule (1) does not apply. We now introduce a slight modification of λLJQ , named λLjQ , determined by two changes in the reduction rules: in rule (6) we omit the proviso; and rule (5) is dropped. A former redex of (5) is reduced by (6) – now possible because there is no proviso – followed by (4), achieving the same effect as previous rule (5). In fact, very soon we will define a big modification and simplification of the original λLJQ , which is more appropriate to our goals here. But we need to justify that big modification, by a comparison with the original system. For the purpose of this comparison, we will use, not λLJQ , but λLjQ instead. So, the first thing we do is to check that λLjQ has the same properties as the original. The maps between λ Cand λLJQ defined by Dyckhoff-Lengrand can be seen as maps to and from λLjQ instead. Next, it is easy to see that such maps still establish an equational correspondence, now between λ Cand λLjQ . It turns out that the correspondence is also a pre-Galois connection from λLjQ to λ C. Because of this, λLjQ inherits confluence of λ C, as λLJQ did. A simplified calculus. We now define the announced simplified calculus, named λQ . It is presented in Table 6. The idea is to drop the cut forms C 1 ( V, x.W )and C 2 ( V, x.N ), which correspond to explicit substitutions. Since only one form of cut remain, C 3 ( M, x.N ), we write it as C( M, x.N ). The typing rules of the surviving constructors remain the same. The omitted reduction rules for the stepwise execution of substitution are now dropped, since they concerned the omitted forms of cut. Rules (1) and (3) are renamed as Bv and ηcut , respectively. Rules (4) and (6) are renamed π1 and π2 , respectively, and we let π := π1∪π2 . Rules (2) and (7) are combined into a single rule named σv. The design of rule σv is interesting. Rule (2) fired a variable substitution operation [ x/y ] − , already present in the original calculus. The contractum of rule (7), being an explicit substitution, has to be replaced by the call to an appropriate, implicit, substitution operator José Espírito Santo and Filipa Mendes 15:9 (terms) M, N ::= ↑V|x(V, y.N)|C(M, x.N) (values) V, W ::= x|λx.M (Bv)C(↑(λx.M), y.y(V, z.N)) →C(C(↑V, x.M), z.N)if y /∈FV (V)∪FV (N) (σv)C(↑V, y.N)→[V/y]Nif Bvdoes not apply (ηcut)C(M, x. ↑x)→M (π1)C(z(V, y.P), x.N)→z(V, y.C(P, x.N)) (π2)C(C(M, y.P ), x.N)→C(M, y.C(P, x.N)) Table 6 The simpified λLJQ-calculus, named λQ-calculus [ λx.M/y ] − , whose stepwise execution should be coherent with the omitted reduction rules for C 1 ( V, x.W )and C 2 ( V, x.N ). Hopefully, the sought operation and the already present variable substitution operation are subsumed by a value substitution operation [V/y]−. The critical clause is the definition of [ V/y ]( y ( W, z.P )). We adopt [ V/y ]( y ( W, z.P )) = C( ↑V, y.y ([ V/y ] W, z. [ V/y ] P )) in the case V = λx.M , but not in the case of V = x , because σv would immediately generate a cycle in the case y /∈FV ( V ) ∪FV ( N ). We adopt instead [ x/y ]( y ( W, z.P )) = x ([ x/y ] W, z. [ x/y ] P )which moreover is what the original calculus dictates. Notice that another cycle would arise, if a Bv -redex was contracted by σv . But this is blocked by the proviso of the latter rule. There is a map ( _ ) √ : λLjQ →λQ , based on the idea of translating the omitted cuts by calls to substitution: C 1 ( V, x.W )is mapped to [ V/x ] W and C 2 ( V, y.N )is mapped to [ V/x ] N . This map, together with the inclusion λQ ⊂λLjQ (seeing C( M, x.N )as C 3 ( M, x.N )) gives a reflection of λQ in λLjQ . This reflection allows to conclude easily that reduction in λLjQ is conservative over reduction in λQ . Moreover, this reflection can be composed with the equational correspondence between λ Cand λLjQ to produce an equational correspondence between λ Cand λQ . Finally, this reflection is also a pre-Galois connection from λQ to λLjQ . Thus, confluence of λQ can be pulled back from the confluence of λLjQ. To sum up, we obtained a more manageable calculus, conservatively extended by the original one, which, as the latter, is confluent and is in equational correspondence with λC. The kernel of the simplified calculus. For a moment, we do an analogy between λ Cand λQ . As was recalled in Section 2, the former system admits a kernel, a subsystem of “administrative” normal forms, which are the normal forms with respect to a subset of the set of reduction rules [ 25 ]. For λQ , the “administrative” normal forms are very easy to characterize: in a cut C( M, x.N ), M has to be of the form ↑V . Logically, this means that the left premiss of the cut comes from a sequent Γ →V : A ; given that such sequents are obtained either with Ax or R⊃ , the cut formula A in that premiss is not a passive formula of the previous inference; hence the cut is fully permuted to the left – so we call such forms left normal forms. The reduction rules of λQ which perform left permutation are rules π1 and π2 (even though textually the outer cut in the redex of those rules seems to move to the right after the reduction), so these rules are declared “administrative”. The kernel of λQ is named LNF . The specific form of cut allowed, namely C( ↑V, x.N ), is written C v ( V, x.N ). No other change is made to the grammar of terms. Given M, N ∈LNF , the general form of cut becomes in LNF a derived constructor written C v ( M : z.N )and FSCD 2023 15:16 The Logical Essence of Compiling With Continuations Ψ(V) = ↑Ψv(V) Ψ(let x:= Vin cx) = Cv(ΨvV, Ψx(cx)) Ψv(x) = x Ψv(λx.M) = λx.ΨM Ψx(M) = x.ΨM Ψx(let y:= xW in N) = (ΨW, y.ΨN) Θ(↑V)=Θv(V) Θ(Cv(V, c)) = let x:= ΘvVin Θx(c) Θv(x) = x Θv(λx.M) = λx.ΘM Θx(y.M)=[x/y](ΘM) Θx(W, y.N) = let y:= x(ΘvW)in ΘN Table 10 Translation from V ES to V F S and vice-versa. Therefore the alternative between the two sub-kernels corresponds to the alternative between two proof-systems for call-by-value, the sequent calculus LJQ and the natural deduction system with general elimination rules behind λJv. AλJv-term is either a value or a generalized applications M(N, x.P), with typing rule Γ⊢JM:A⊃BΓ⊢JN:AΓ, x :B⊢JP:C Γ⊢JM(N, x.P ) : C If the head term M is itself an application M1 ( M2, y.M3 ), then M3 has type A⊃B and the term can be rearranged as M1 ( M2, y.M3 ( N, x.P )), to bring M3 and N together. This is a known commutative conversion [ 15 ], here named π1 , which aims to convert the head term M to a value V . On the other hand, if the argument N is itself an application N1 ( N2, y.N3 ), then N3 has type A and the term can be rearranged as N1 ( N2, y.M ( N3, x.P )), to bring M and N3 together. This is a conversion π2 which has not been studied, and which aims to convert the argument Nto a value W. The combined effect of π := π1∪π2 is to reduce generalized applications to the form V(W, x.P), called commutative normal form. On these forms, the βv-rule of λJvreads (βv) (λy.M)(W, x.P)→[[W/y]M\x]P The left substitution operation [N\x]Pis defined by [V\x]P= [V/x]P[V(W, y.N3)\x]P=V(W, y.[N3\x]P) The commutative normal forms, equipped with βv, constitute the system CNF . The announced isomorphisms are given in Tables 10 and 11. The map Ψ : V ES →V FS requires the key auxiliary map Ψ x , whose design is guided by types: if Γ , x : A⊢Ccx : B then Γ |A⇒ Ψ x ( cx ) : B . The isomorphism Υ : CES →CNF should be obvious. It can be proved that the operation LET y := Min P in CES is translated as left substitution: Υ(LET y:= Min P) = [ΥM\y]ΥP. A final point. The sub-kernel V ES is isomorphic to the CPS-target, after composition with the negative translation: V ES ∼ =V FS ∼ =CP S . A variant of the negative translation delivers: ▶Theorem 5. CNF ∼ =CP S. José Espírito Santo and Filipa Mendes 15:17 Υ(x) = x Υ(λx.M) = λx.ΥM Υ(let x:= V W in M)=ΥV(ΥW, x.ΥM) Φ(x) = x Φ(λx.M) = λx.ΦM Φ(V(W, x.M)) = let x:= ΦVΦWin ΦM Table 11 Translation from CES to CN F and vice-versa. So we also have CES ∼ =CNF ∼ =CP S . Here CP S is the sub-calculus of CP S where commands KV are omitted and σv normalization is enforced. Its unique reduction rule, named βv, becomes (βv) (λy.λk.M)W(λx.N)→[λx.N/k][W/y]M The definition of substitution [λx.N/k]Mhas the following critical clause: [λx.N/k](kV )=[V/x]N This clause does the reduction of the σv -redex ( λx.N ) V on the fly; and it echoes the critical clause of a structural substitution. Moreover, CP S is the target of a version of the CPS-translation, obtained by changing just one clause: (V:λx.M)=[V†/x]M. The variant of the negative translation yielding CNF ∼ =CP S is defined by (V(W, x.M))≀=V∼W∼(λx.M≀) All the other needed clauses as before. For the isomorphism, we have to prove: ([N\x]M)≀= [λx.M≀/k]N≀ This is a last minute bonus: a CP S explanation of left substitution. 6 Conclusions Contributions. We list our main contribution: the VFS-translation; the negative translation as an isomorphism between the VFS and CPS targets; the decomposition of the CPStranslation in terms of the VFS-translation and the negative translation; the two sub-kernels of λ Cand their perfect relationship with appropriate fragments of the sequent calculus LJQ and natural deduction with general eliminations; the reworking of the term calculus for LJQ . In all, we took the polished account of the essence of CPS, obtained in [ 25 ] and illustrated in Fig. 1, and revealed a rich proof-theoretical background, as in Fig. 2, with a double layer of sub-kernels, under a layer of expansions (see the dotted lines in Fig. 2 and recall (1), (2), and (3)), intersecting an intermediate zone, between the source language and the CPS targets, of calculi corresponding to proof systems. Related work. In [ 4 ], LJQ is studied as a source language, while the CPS translation of LJQ is a tool to establish indirectly a connection with λ C, through their respective kernels, in order to confirm that cut-elimination in LJQ is connected with call-by-value computation. There is nothing wrong with using the sequent calculus as source language and translating it with CPS: this has been done abundantly, even by the first author [ 1 , 27 , 4 , 9 ]. But the FSCD 2023 15:18 The Logical Essence of Compiling With Continuations point made here is that the sequent calculus should also be used as a tool to analyze the CPS-translation, and is able to play a special role as an intermediate language. The sequent calculus was put forward as an intermediate representation for compilation of functional programs in [ 2 ]. This study addresses compilation of programs for a real-world language; designs an intermediate language Sequent Core (SC) inspired in the sequent calculus for such source language; and compares SC with CPS heuristically w. r. t. several desirable properties in the context of optimized compilation. In the present paper, we address the foundations of compilation, employing theoretical languages; pick the sequent calculus LJQ , which is a standard systems with decades of history in proof-theory [ 3 ]; and compare LJQ and CPS, not through a benchmarking of competing languages, but through mathematical results showing their intimate connection. Future work. We know an appropriate CPS target will be capable of interpreting a classical extension of our chosen source language. The problem in moving in this direction is that there is no standard extension of λ Cwith control operators readily available. Source languages with let-expressions and control operators can be found in [ 14 , 5 ], but adopting them means to redo all that we have done here – that is another project. On the other hand, maybe a system with generalized applications will make a good source language. The system λ J v performed well in this paper, since its sub-kernel of administrative normal forms ( CNF ) is reachable without consideration of expansions – a sign of a well calibrated syntax. References 1 Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, SIGPLAN Notices 35(9), pages 233–243. ACM, 2000. doi:http://doi.acm.org/10.1145/351240.351262. 2 Paul Downen, Luke Maurer, Zena M. Ariola, and Simon Peyton Jones. Sequent calculus as a compiler intermediate language. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 74–88. ACM, 2016. 3 Roy Dyckhoff and Stéphane Lengrand. LJQ, a strongly focused calculus for intuitionistic logic. In A. Beckmann, U. Berger, B. Löwe, and J. V Tucker, editors, Proc. of the 2nd Conference on Computability in Europe (CiE’06), volume 3988 of Lecture Notes in Computer Science. Springer-Verlag, 2006. 4 Roy Dyckhoff and Stéphane Lengrand. Call-by-value lambda calculus and LJQ. Journal of Logic and Computation, 17:1109–1134, 2007. 5 José Espírito Santo. Towards a canonical classical natural deduction system. Annals of Pure and Applied Logic, 164(6):618–650, 2013. 6 José Espírito Santo. The call-by-value lambda-calculus with generalized applications. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 35:1–35:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. 7 José Espírito Santo and Filipa Mendes. The logical essence of compiling with continuations. CoRR, 2023. URL: https://arxiv.org/2304.14752. 8 José Espírito Santo. The λ -calculus and the unity of structural proof theory. Theory of Computing Systems, 45:963–994, 2009. 9 José Espírito Santo, Ralph Matthes, and Luís Pinto. Continuation-passing-style and strong normalization for intuitionistic sequent calculi. Logical Methods in Computer Science, 5(2:11), 2009. 10 Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Robert Cartwright, editor, Proceedings of the ACM SIGPLAN’93 José Espírito Santo and Filipa Mendes 15:19 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, pages 237–247. ACM, 1993. 11 Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations (with retrospective). In Kathryn S. McKinley, editor, 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection, pages 502–514. ACM, 2003. 12 Timothy G. Griffin. A formulae-as-types notion of control. In ACM Conf. Principles of Programming Languages. ACM Press, 1990. 13 Hugo Herbelin. A λ -calculus structure isomorphic to a Gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn, editors, Proceedings of CSL’94, volume 933 of Lecture Notes in Computer Science, pages 61–75. Springer-Verlag, 1995. 14 Hugo Herbelin and Stéphane Zimmermann. An operational account of call-by-value minimal and classical lambda-calculus in “natural deduction” form. In Proceedings of Typed Lambda Calculi and Applications’09, volume 5608 of LNCS, pages 142–156. Springer-Verlag, 2009. 15 Felix Joachimski and Ralph Matthes. Standardization and confluence for a lambda calculus with generalized applications. In Proceedings of RTA 2000, volume 1833 of LNCS, pages 141–155. Springer, 2000. 16 Andrew Kennedy. Compiling with continuations, continued. In Ralf Hinze and Norman Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 177–190. ACM, 2007. 17 John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-byvalue, call-by-need and the linear lambda calculus. Theoretical Computer Science, 228(1-2):175– 210, 1999. 18 Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. Compiling without continuations. In Albert Cohen and Martin T. Vechev, editors, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pages 482–494. ACM, 2017. 19 Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs, Conference, Brooklyn College, New York, NY, USA, June 17-19, 1985, Proceedings, volume 193 of Lecture Notes in Computer Science, pages 219–224. Springer, 1985. 20 Eugenio Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS88-86, University of Edinburgh, 1988. 21 Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55–92, 1991. 22 M. Parigot. λµ -calculus: an algorithmic interpretation of classic natural deduction. In Int. Conf. Logic Prog. Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 190–201. Springer Verlag, 1992. 23 Gordon Plotkin. Call-by-name, call-by-value and the λ -calculus. Theoretical Computer Science, 1:125–159, 1975. 24 Amr Sabry and Matthias Felleisen. Reasoning about programms in continuation-passing-style. LISP and Symbolic Computation, 6(3/4):289–360, 1993. 25 Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Trans. on Programming Languages and Systems, 19(6):916–941, 1997. 26 Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry/Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. 27 Philip Wadler. Call-by-value is dual to call-by-name. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, pages 189–201. ACM, 2003. A The original LJQ system The original calculus by Dyckhoff-Lengrand is recalled in Table 12. FSCD 2023 15:20 The Logical Essence of Compiling With Continuations (terms) M, N ::= ↑V|x(V, y.N)|C2(V, x.N)|C3(M, x.N) (values) V, W ::= x|λx.M |C1(V, x.W) (1) C3(↑(λx.M), y.y(V, z.N)) →C3(C3(↑V, x.M), z.N) (a) (2) C3(↑x, y.N)→[x/y]N (3) C3(M, x. ↑x)→M (4) C3(z(V, y.P), x.N)→z(V, y.C3(P, x.N)) (5) C3(C3(↑W, y.y(V, z.P)), x.N)→C3(↑W, y.y(V, z.C3(P, x.N))) (b) (6) C3(C3(M, y.P ), x.N)→C3(M, y.C3(P, x.N)) (c) (7) C3(↑(λx.M), y.N)→C2(λx.M, y.N) (d) (8) C1(V, x.x)→V (9) C1(V, x.y)→y(e) (10) C1(V, x.(λy.M)) →λy.C2(V, x.M) (11) C2(V, x. ↑W)→ ↑(C1(V, x.W)) (12) C2(V, x.x(W, z.N)) →C2(↑V, x.x(C1(V, x.W), z.C2(V, x.N))) (13) C2(V, x.y(W, z.N)) →y(C1(V, x.W), z.C2(V, x.N)) (e) (14) C2(V, x.C3(M, y.N)) →C3(C2(V, x.M), y.C2(V, x.N)) Provisos: ( a ) y /∈FV ( V ) ∪FV ( N ).( b ) y /∈FV ( V ) ∪FV ( P )).( c )If rule (5) does not apply. (d)If rule (1) does not apply. (e)x=y. Γ, x :A→x:AAx Γ→V:A Γ⇒↑V:ADer Γ, x :A⇒M:B Γ→λx.M :A⊃BR⊃Γ⇒M:AΓ, x :A⇒N:B Γ⇒C3(M, x.N) : BCut3 Γ→V:AΓ, x :A→W:B Γ→C1(V, x.W) : BCut1 Γ→V:AΓ, x :A⇒N:B Γ⇒C2(V, x.N) : BCut2 Γ, x :A⊃B→V:AΓ, x :A⊃B, y :B⇒N:C Γ, x :A⊃B⇒x(V, y.N) : CL⊃ Table 12 The original calculus by Dyckhoff-Lengrand B Kernel of λC Our presentation of the kernel of λ Cgiven in Table 2 is very close to the original one in [ 25 ], as we now see. In [25], the terms Mof the kernel are generated by the grammar: M, N, P ::= K [V]| K [V W] V, W ::= x|λx.M K ::= [_]|let x:= [_]in P We take for granted the sets of terms and values of λ C, together with the set of contexts of λ C, which are λ C-terms with a single hole, and the concept of hole filling in such contexts. This grammar defines simultaneously a subset of the terms of λ C, a subset of the values of λC, and a subset of the contexts of λC. The second production in the grammar of terms, K [ V W ], should be understood thus: given in the kernel values V , W and a context K , the λ C-term K [ V W ], obtained by filling the José Espírito Santo and Filipa Mendes 15:21 hole of K with the λ C-term V W , is in the kernel. In λ C, V W is a subterm of K [ V W ]; but, as we observed in Section 2, in the kernel, the term V W is not an immediate subterm of K [ V W ]– the immediate subexpressions are just V , W , and K . Notice the λ C-term M = V W is a term in the kernel, generated by the second production of the grammar with K = [ _ ]. But that second production should not be interpreted as K [M]with M=V W. There is no primitive K [ M ]in the kernel. Instead, there is the operation ( M : K ), defined by recursion on Mas follows: (V: K ) = K [V] (V W : K ) = K [V W] (let x:= Vin M: K ) = let x:= Vin (M: K ) (let x:= V W in M: K ) = let x:= V W in (M: K ) It is easy to see that (M:let x:= [_]in P) = LET x:= Min Pand that (M: [_]) = M. In [25], the kernel has the following reduction rule (β.v) K [(λx.M)V]→([V/x]M: K ). There is no need for the requirement of maximal K in this rule, as done in [ 25 ], once the above clarification about K [ V W ]is obtained. We now see the relationship between β.v and our Bvand B′ v. Let K =let y:= [_]in P. Then rule Bvcan re written as K [(λx.M)V]→let x:= Vin (M: K ). The contractum is a letv -redex, which could be immediately reduced, to achieve the effect of β.v . Here we prefer to delay this letv -step, and the same applies to our rule B′ v , which corresponds to the case K = [_]. This issue of delaying letvis also seen in Section 5. Finally, rule ηlet in [ 25 ] reads let x := [ _ ] in K [ x ] → K . We argue that in our presentation we can derive (M:let x:= [_]in K [x]) →(M: K ). If K = [ _ ], then we have to prove LET x := Min x→M . This is proved by an easy induction on M : the case M = V (resp. M = V W ) gives rise to a σv -step (resp. ηlet -step); the remaining two cases follow by induction hypothesis. If K = let y := [ _ ] in P , then we have to prove LET x := Min let y := xin P→LET y := Min P . Now let y := xin P→letv [ y/x ] P . Since Q→Q′ implies LET x := Min Q→ LET x := Min Q′ , we obtain LET x := Min let y := xin P→LET x := Min [ y/x ] P = α LET y:= Min P. FSCD 2023