BRICS RS-02-2 L. R. Nielsen: A Simple Correctness Proof of the Direct-Style Transformation BRICS

Basic Research in Computer Science

A Simple Correctness Proof of the Direct-Style Transformation

Lasse R. Nielsen BRICS Report Series RS-02-2 ISSN 0909-0878 January 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Lasse R. Nielsen.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/2/

A simple proof of the direct-style transformation

Lasse R. Nielsen BRICS ^{∗} Department of Computer Science, University of Aarhus ^{†}

January 2002

Abstract

We build on Danvy and Nielsen’s first-order program transformation into continuation-passing style (CPS) to present a new correctness proof of the converse transformation, i.e., a one-pass transformation from CPS back to direct style. Previously published proofs were based on CPS transformations that were either higher-order, noncompositional, or operating in two passes, and were correspondingly complicated to reason about. In contrast, this work is based on a CPS transformation that is first-order, compositional, and that operates in one pass. Therefore the proof simply proceeds by structural induction on syntax.

Keywords: compositionality, CPS-transformation, direct-style transformation, correctness proof.

∗ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

† Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: lrn@brics.dk

Contents

1 Introduction 3 1.1 The continuation-passing-style transformation . . . . . . . . . 3 1.2 The direct-style transformation . . . . . . . . . . . . . . . . . 3 1.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Definitions 4

3 Correctness 6

4 Conclusion 10

List of Figures

1 Syntax of the λ-calculus in direct style . . . . . . . . . . . . . 4 2 Syntax of the λ-calculus in continuation-passing style . . . . . 4 3 Call-by-value CPS transformation . . . . . . . . . . . . . . . . 5 4 The direct-style transformation . . . . . . . . . . . . . . . . . 5

1 Introduction

1.1 The continuation-passing-style transformation

The CPS transformation on the λ-calculus maps direct-style expressions into semantically equivalent CPS expressions. Reynolds used it to map a functional program into an evaluation-order-independent form [9], and Plotkin later formalized it and proven it to be semantics preserving [8].

The CPS programs generated by Plotkin’s CPS transformation contains so-called administrative redexes. Steele added a second pass to the transformation to reduce these redexes, generating equivalent but more compact CPS expressions [11]. This two-pass CPS transformation inspired several researchers to write one-pass CPS transformations that directly generate administratively reduced CPS expressions, making CPS transformation more practically useful. Appel, Danvy and Filinski, and Wand independently discovered a higher-order one-pass CPS transformation [1, 4, 12] while Sabry and Felleisen constructed a non-compositional one-pass CPS transformation based on syntactic theory [10]. Recently, however, Danvy and Nielsen presented a one-pass CPS transformation that is both first-order and compositional [6].

1.2 The direct-style transformation

The direct-style transformation is the inverse of the CPS transformation, and it maps CPS expressions back into direct-style expressions.

Danvy introduced the direct style transformation [2], and it was proven to preserve semantics by Lawall [7] and by Danvy, Dzafic, and Pfenning [3]. These proofs are based on the higher-order CPS transformation, and as such they require reasoning about higher-order functions, e.g., using logical relations.

This paper gives a simpler proof using only structural induction.

1.3 Overview

The rest of this paper is structured as follows: Section 2 presents the notation and definitions, Section 3 proves that the direct-style transformation preserves meaning by showing that it is a left inverse to the CPS transformation, and Section 4 concludes.

2 Definitions

A syntax for the λ-calculus is shown in Figure 1.

p ::= e  p ∈ DProg
e ::= t | s  e ∈ DExpr
t ::= x | λx.e t ∈ DTriv, trivial terms, i.e., values
s ::= e e  s ∈ DComp, serious terms, i.e., computations

x ∈ Ide, a set of identifiers

Figure 1: Syntax of the λ-calculus in direct style

A grammar of λ-expressions in continuation-passing style is shown in Figure 2.

p ::= λk.e  p ∈ CProg
e ::= r c | c t  e ∈ CExpr
t ::= v | x | λx.r t ∈ CTriv
r ::= λk.e | t t r ∈ Croot
c ::= k | λv.e  c ∈ CCont

where x ∈ Ide, k ∈ CIde, and v ∈ VIde, disjoint sets of identifiers.

Figure 2: Syntax of the λ-calculus in continuation-passing style

The call-by-value (CBV) CPS transformation is shown in Figure 3. Being “fresh wrt. e” and “fresh wrt. c” means that we pick, determinis-

tically, an element of CIde, or two different elements of VIde, that do not occur freely in e, respectively in c.

A typing argument shows that the CPS transformation actually generates only programs in continuation-passing style.

The direct-style transformation corresponding to the CPS transformation uses a stack of expressions to keep track of the intermediate results. This stack, represented by σ, is either the empty stack (•) or a stack with something on top (x:: σ′), and the set of stacks of direct-style expressions is represented by [DExpr].

The definition of the Direct-Style transformation is shown in Figure 4. The direct-style transformation is not total on the set of CPS programs. In

C : DProg → CProg
C[[e]] = λk. C^{DExpr}[[e]] k
C^{DExpr} : DExpr × CIde → CExpr
C^{DExpr}[[t]] k = k C^{DTriv}[[t]]
C^{DExpr}[[s]] k = C^{DComp}[[s]] k
C^{DTriv} : DTriv → CTriv
C^{DTriv}[[x]] = x
C^{DTriv}[[λx.e]] = λx.λk. C^{DExpr}[[e]] k where k fresh wrt. e
C^{DComp} : DComp × CCont → CExpr
C^{DComp}[[t_{1} t_{2}]] c = C^{DTriv}[[t_{1}]] C^{DTriv}[[t_{2}]] c
C^{DComp}[[s_{1} t_{2}]] c = C^{DComp}[[s_{1}]] (λv_{1}.v_{1} C^{DTriv}[[t_{2}]] c)
C^{DComp}[[t_{1} s_{2}]] c = C^{DComp}[[s_{2}]] (λv_{2}.C^{DTriv}[[t_{1}]] v_{2} c)
C^{DComp}[[s_{1} s_{2}]] c = C^{DComp}[[s_{1}]] (λv_{1}.C^{DComp}[[s_{2}]] (λv_{2}.v_{1} v_{2} c))
where v_{1} and v_{2} are distinct and fresh wrt. c

Figure 3: Call-by-value CPS transformation

D : CProg → DProg
D[[λk.e]] = D^{CExpr}[[e]] •
D^{CExpr} : CExpr × [DExpr] → DExpr
D^{CExpr}[[r c]] σ = D^{CCont}[[c]] (D^{Croot}[[r]] σ)
D^{CExpr}[[c t]] σ = D^{CCont}[[c]] (D^{CTriv}[[t]] σ)
D^{CTriv} : CTriv × [DExpr] → DExpr × [DExpr]
D^{CTriv}[[v]] (e :: σ) = (e, σ)
D^{CTriv}[[x]] σ = (x, σ)
D^{CTriv}[[λx.r]] σ = (λx.e, σ) where (e, •) = D^{Croot}[[r]] •
D^{Croot} : Croot × [DExpr] → DExpr × [DExpr]
D^{Croot}[[λk.e]] σ = (D^{CExpr}[[e]] •, σ)
D^{Croot}[[t_{1} t_{2}]] σ = (e_{1} e_{2}, σ′′) where (e_{2},σ’) = D^{CTriv}[[t_{2}]] σ (e_{1},σ”) = D^{CCont}[[t_{1}]] σ′
D^{CCont} : CCont × (DExpr × [DExpr]) → DExpr
D^{CCont}[[k]] (e, σ) = e
D^{CCont}[[λv.e]] (e′, σ) = D^{CExpr}[[e]] (e′:: σ)

Figure 4: The direct-style transformation the next section we show that it is total on the image of the CPS transformation, and we only consider the transformation on this set.

3 Correctness

We prove that the direct-style transformation is correct and non-trivial. By correct we mean that it preserves meaning. By non-trivial we mean that the direct-style expressions generated by the transformation are not only a limited subset of λ-expressions. Since CPS expressions are a subset of direct-style expressions, the identity function could be considered a trivial direct-style transformation.

The proof shows that the direct-style transformation is a left-inverse to the CPS transformation. Since the CPS transformation preserves meaning and is defined on all terms, the direct-style transformation must also preserve meaning and be non-trivial. The CPS transformation is injective but not surjective, so when restricted to its image, it is a bijection, and the left inverse also becomes a right inverse.

Lemma 1 (Left Inverse) The D function is a left inverse to the C function.

∀p ∈ DProg.D[[C[[p]]]] = p

Proof:

The proof is by structural induction on the program. We show the following three properties by mutual structural induction.

1. If e : DExpr is an expression and k : CIde a continuation identifier

then for any σ

D^{CExpr}[[C^{DExpr}[[e]] k]] σ = e

2. If t : DTriv is a value then for any σ

D^{CTriv}[[C^{DTriv}[[t]]]] σ = (t, σ)

3. If s : DComp is a computation and c : CCont a continuation then

for any σ

D^{CExpr}[[C^{DComp}[[s]] c]] σ = D^{CCont}[[c]] (s, σ)

Property 1: There are two cases, one for each production in the grammar.

Case e = t:

D^{CExpr}[[C^{DExpr}[[t]] k]] σ

= D^{CExpr}[[k C^{DTriv}[[t]]]] σ
= D^{CCont}[[k]] (D^{CTriv}[[C^{DTriv}[[t]]]] σ)
= D^{CCont}[[k]] (t, σ)  (by I.H.)
= t

Case e = s:

D^{CExpr}[[C^{DExpr}[[s]] k]] σ = D^{CExpr}[[C^{DComp}[[s]] k]] σ
= D^{CCont}[[k]] (s, σ)
= s

Property 2: There are two cases, one for each production in the grammar.

Case t = x:

D^{CTriv}[[C^{DTriv}[[x]]]] σ = D^{CTriv}[[x]] σ = (x, σ)

Case t = λx.e:

D^{CTriv}[[C^{DTriv}[[λx.e]]]] σ

= D^{CTriv}[[λx.λk. C^{DExpr}[[e]] k]] σ
= (λx.e′, σ′)
where (e′, σ′) = D^{Croot}[[λk. C^{DExpr}[[e]] k]] σ
= (λx.e′, σ′)
where (e′, σ′) = (D^{CExpr}[[C^{DExpr}[[e]] k]] • ,σ)
= (λx.e′, σ′)
where (e′, σ′) = (e, σ)  (by I.H.)
= (λx.e, σ)

Property 3: There are four cases, one for each case of the C^{DComp} function.

Case s = t_{1} t_{2}:

D^{CExpr}[[C^{DComp}[[t_{1} t_{2}]] c]] σ
= D^{CExpr}[[C^{DTriv}[[t_{1}]] C^{DTriv}[[t_{2}]] c]] σ
= D^{CCont}[[c]] (D^{Croot}[[C^{DTriv}[[t_{1}]] C^{DTriv}[[t_{2}]]]] σ)
= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = D^{CTriv}[[C^{DTriv}[[t_{2}]]]] σ

(e_{1}, σ′′) = D^{CTriv}[[C^{DTriv}[[t_{1}]]]] σ

= D^{CCont}[[c]] (t_{1} t_{2}, σ)

Case s = s_{1} t_{2}:

D^{CExpr}[[C^{DComp}[[s_{1} t_{2}]] c]] σ

= D^{CExpr}[[C^{DComp}[[s_{1}]] (λv_{1}.v_{1} C^{DTriv}[[t_{2}]] c)]] σ
= D^{CCont}[[λv_{1}.v_{1} C^{DTriv}[[t_{2}]] c]] (s_{1}, σ)  (by I.H.)
= D^{CExpr}[[v_{1} C^{DTriv}[[t_{2}]] c]] s_{1} :: σ
= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = D^{CTriv}[[C^{DTriv}[[t_{2}]]]] s_{1} :: σ
(e_{1}, σ′′) = D^{CTriv}[[v_{1}]] σ′
= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = (t_{2}, s_{1} :: σ)
(e_{1}, σ′′) = D^{CTriv}[[v_{1}]] σ′
= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = (t_{2}, s_{1} :: σ)
(e_{1}, σ′′) = (s_{1}, σ)
= D^{CCont}[[c]] (s_{1} t_{2}, σ)

Case s = t_{1} s_{2}:

D^{CExpr}[[C^{DComp}[[t_{1} s_{2}]] c]] σ

= D^{CExpr}[[C^{DComp}[[s_{2}]] (λv_{2}.C^{DTriv}[[t_{1}]] v_{2} c)]] σ
= D^{CCont}[[λv_{2}.C^{DTriv}[[t_{1}]] v_{2} c]] (s_{2}, σ)  (by I.H.)
= D^{CExpr}[[C^{DTriv}[[t_{1}]] v_{2} c]] (s_{2} :: σ)
= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = D^{CTriv}[[v_{2}]] (s_{2} :: σ)

(e_{1}, σ′′) = D^{CTriv}[[C^{DTriv}[[t_{1}]]]] σ′

= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = (s_{2}, σ)

(e_{1}, σ′′) = (t_{1}, σ′)

= D^{CCont}[[c]] (t_{1} s_{2}, σ)

Case s = s_{1} s_{2}:

D^{CExpr}[[C^{DComp}[[s_{1} s_{2}]] c]] σ

= D^{CExpr}[[C^{DComp}[[s_{1}]] (λv_{1}.C^{DComp}[[s_{2}]] (λv_{2}.v_{1} v_{2} c))]] σ
= D^{CCont}[[λv_{1}.C^{DComp}[[s_{2}]] (λv_{2}.v_{1} v_{2} c)]] (s_{1}, σ)  (by I.H.)
= D^{CExpr}[[C^{DComp}[[s_{2}]] (λv_{2}.v_{1} v_{2} c)]] (s_{1} :: σ)
= D^{CCont}[[λv_{2}.v_{1} v_{2} c]] (s_{2}, s_{1} :: σ)  (by I.H.)
= D^{CExpr}[[v_{1} v_{2} c]] (s_{2} :: s_{1} :: σ)
= D^{CCont}[[c]] D^{Croot}[[v_{1} v_{2}]] (s_{2} :: s_{1} :: σ)
= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = D^{CTriv}[[v_{2}]] (s_{2} :: s_{1} :: σ)
(e_{1}, σ′′) = D^{CTriv}[[v_{1}]] σ′
= D^{CCont}[[c]] (e_{1} e_{2}, σ′′)
where (e_{2}, σ′) = (s_{2}, s_{1} :: σ)
(e_{1}, σ′′) = (s_{1}, σ)
= D^{CCont}[[c]] (s_{1} s_{2}, σ)

These cases shows that the properties hold for all direct-style expressions, so in particular if e : DProg

D[[C[[e]]]] = D[[λk. C^{DExpr}[[e]] k]] = D^{CExpr}[[C^{DExpr}[[e]] k]] • = e

qed

When restricting the CPS transformation to its image, i.e., forcing it to be surjective, a left inverse is also a right inverse.

Lemma 2 (Right Inverse) The function D is the right inverse of C on C[[DProg]], the image of DProg under C.

∀p ∈ C[[DProg]].C[[D[[p]]]] = p

Proof: Let p ∈ C[[DProg]], i.e., there exists a p′ ∈ DProg such that p = C[[p′]]. Then (C∘D)(p) = (C∘D)(C[[p′]]) = C[[(D∘ C)(p′)]]. From Theorem 1 we know that D∘ C is the identity on DProg, so C[[(D∘ C)(p′)]] = C[[p′]] = p.

qed

With these lemmas showing the following connection

\xymatrix{DProg \ar[r]^{C} & C[[DProg]] \ar[l]^{D}}

we can directly show correctness and non-triviality Theorem 1 The direct-style transformation is correct and non-trivial.

Proof: Follows from the correctness of the CPS transformation and the previous lemmas. qed

4 Conclusion

We have presented a simpler proof of the correctness of the direct-style transformation than what has previously been published. The proof, like the previous ones, is based on a CPS transformation, since the choice of CPS transformation dictates the type of proof. Earlier proofs of the higher-order CPS transformation used logical relations [5], proofs of the non-compositional CPS-transformation used well-founded induction [10], and proofs of twopass CPS transformations need to address both passes [10]. In contrast, a first-order, compositional, and one-pass CPS transformation allows a proof using only a single structural induction [6].

One can also show correctness of the direct-style transformation on larger sets than just the image of the CPS transformation. Proofs of such properties can also be derived from correctness of a CPS transformation, and using the first-order compositional CPS transformation also gives proofs using only structural induction.

References

[1] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, 1992.

[2] Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183–195, 1994.

[3] Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. In Third International Workshop on Higher-Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science, pages 19–31, Paris, France, September 1999. Also available as the technical report BRICS RS-99-23.

[4] Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.

[5] Olivier Danvy and Lasse R. Nielsen. A higher-order colon translation. In Herbert Kuchen and Kazunori Ueda, editors, Fifth International Symposium on Functional and Logic Programming, number 2024 in Lecture Notes in Computer Science, pages 78–91, Tokyo, Japan, March 2001. Springer-Verlag. Extended version available as the technical report BRICS RS-00-33.

[6] Olivier Danvy and Lasse R. Nielsen. A first-order one-pass CPS transformation. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002, number 2303 in Lecture Notes in Computer Science, pages 98–113, Grenoble, France, April 2002. Springer-Verlag. Extended version available as the technical report BRICS RS-01-49.

[7] Julia L. Lawall. Continuation Introduction and Elimination in Higher-Order Programming Languages. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana, July 1994.

[8] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[9] John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363– 397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972).

[10] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3/4):289–360, 1993.

[11] Guy L. Steele Jr. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978.

[12] Mitchell Wand. Correctness of procedure representations in higherorder assembly language. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics, number 598 in Lecture Notes in Computer Science, pages 294–311, Pittsburgh, Pennsylvania, March 1991. Springer-Verlag. 7th International Conference.

Recent BRICS Report Series Publications

RS-02-2 Lasse R. Nielsen. A Simple Correctness Proof of the Direct-Style Transformation. January 2002. 11 pp.

RS-02-1 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. The <bigwig> Project. January 2002. 36 pp. This revised report supersedes the earlier BRICS report RS-00-42.

RS-01-55 Daniel Damian and Olivier Danvy. A Simple CPS Transformation of Control-Flow Information. December 2001. 18 pp.

RS-01-54 Daniel Damian and Olivier Danvy. Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation. December 2001. 41 pp. To appear in the Journal of Functional Programming. This report supersedes the earlier BRICS report RS-00-15.

RS-01-53 Zoltán Ésik and Masami Ito. Temporal Logic with Cyclic Counting and the Degree of Aperiodicity of Finite Automata. December 2001. 31 pp.

RS-01-52 Jens Groth. Extracting Witnesses from Proofs of Knowledge in the Random Oracle Model. December 2001. 23 pp.

RS-01-51 Ulrich Kohlenbach. On Weak Markov’s Principle. December 2001. 10 pp. Appears in Math. Logic Quaterly.

RS-01-50 Jiří Srba. Note on the Tableau Technique for Commutative Transition Systems. December 2001. 19 pp. Appears in Nielsen and Engberg, editors, Foundations of Software Science and Computation Structures, FoSSaCS ’02 Proceedings, LNCS 2303, 2002, pages 387–401.

RS-01-49 Olivier Danvy and Lasse R. Nielsen. A First-Order One-Pass CPS Transformation. December 2001. 21 pp. Extended version of a paper appearing in Nielsen and Engberg, editors, Foundations of Software Science and Computation Structures, FoS-SaCS ’02 Proceedings, LNCS 2303, 2002, pages 98–113.

RS-01-48 Mogens Nielsen and Frank D. Valencia. Temporal Concurrent Constraint Programming: Applications and Behavior. December 2001. 36 pp. Appears in Brauer, Ehrig, Karhumäki and Salomaa, editors, Formal and Natural Computing, LNCS 2300, 2001, pages 298–321.