Publication | Closed Access
Representing Control: a Study of the CPS Transformation
351
Citations
18
References
1992
Year
EngineeringSoftware EngineeringControl ManagementSoftware AnalysisCps TransformSystems EngineeringProgram TransformationProgram DerivationProgramming LanguagesDesignComputer ScienceAutomated ReasoningProgram AnalysisCommand And ControlAutomationIntermediate RepresentationsProcess ControlMathematical FoundationsFormal MethodsContinuation-passing StyleLambda CalculusCps TransformationControl Structureλ ν
The paper investigates transforming λν‑terms into continuation‑passing style and demonstrates how CPS‑based control operators can be naturally incorporated into this transformation. By η‑expanding Fisher and Plotkin’s two‑pass specification, the authors derive a static, context‑free one‑pass CPS algorithm that separates essential syntax‑building constructs from executable administrative code and extends it to accommodate control operators such as Scheme’s call/cc, yielding a concise formulation of the transformation. The resulting algorithm provides a simple, efficient one‑pass CPS transformation, simplifies proofs of Plotkin’s simulation and indifference results, and enables a one‑pass CPS for λn‑terms, suggesting further research directions.
This paper investigates the transformation of λ ν -terms into continuation-passing style (CPS). We show that by appropriate η-expansion of Fisher and Plotkin's two-pass equational specification of the CPS transform, we can obtain a static and context-free separation of the result terms into “essential” and “administrative” constructs. Interpreting the former as syntax builders and the latter as directly executable code, We obtain a simple and efficient one-pass transformation algorithm, easily extended to conditional expressions, recursive definitions, and similar constructs. This new transformation algorithm leads to a simpler proof of Plotkin's simulation and indifference results. We go on to show how CPS-based control operators similar to, more general then, Scheme's call/cc can be naturally accommodated by the new transformation algorithm. To demonstrate the expressive power of these operators, we use them to present an equivalent but even more concise formulation of the efficient CPS transformation algorithm. Finally, we relate the fundamental ideas underlying this derivation to similar concepts from other work on program manipulation; we derive a one-pass CPS transformation of λ n -terms; and we outline some promising areas for future research.
| Year | Citations | |
|---|---|---|
Page 1
Page 1