article

Revisiting an automatic program inverter for Lisp

Authors:

Masahiko KawabeAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 5

Pages 8 - 17

https://doi.org/10.1145/1071221.1071222

Published: 01 May 2005 Publication History

Abstract

We reformulate the Korf-Eppstein method for automatic inversion of first-order functional programs using a structural operational semantics and compare it with the program inversion method described by Gries. We analyze the method and suggest possible extensions. The method is noteworthy in that it was used to construct the first automatic program inverter described in the literature. The key features of the Korf-Eppstein method are the simultaneous inversion of an injective system of functions, an equation-oriented transformation, and the use of postcondition inference heuristics.

References

[1]

S. M. Abramov, R. Glück. Principles of inverse computation and the universal resolving algorithm. In T. Æ. Mogensen, D. Schmidt, I. H. Sudborough (eds.), The Essence of Computation: Complexity, Analysis, Transformation, LNCS 2566, 269--295. Springer-Verlag, 2002.]]

Digital Library

[2]

C. H. Bennet. Logical reversibility of computation. IBM Journal of Research and Development, 17(6):525--532, 1973.]]

Digital Library

[3]

B. Biswas, R. Mall. Reverse execution of programs. SIGPLAN Notices, 34(4):61--69, 1999.]]

Digital Library

[4]

J. S. Briggs. Generating reversible programs. Software Practice and Experience, 17:439--453, 1987.]]

Digital Library

[5]

H. Buhrman, J. Tromp, P. Vitányi. Time and space bounds for reversible simulation. In F. Orejas, P. G. Spirakis, J. van Leeuwen (eds.), Automata, Languages and Programming. Proceedings, LNCS 2076, 1017--1027. Springer-Verlag, 2001.]]

Digital Library

[6]

W. Chen, J. T. Udding. Program inversion: More than fun! Science of Computer Programming, 15:1--13, 1990.]]

Digital Library

[7]

J. Darlington. An experimental program transformation and synthesis system. Artificial Intelligence, 16(1):1--46, 1981.]]

Digital Library

[8]

E. W. Dijkstra. Program inversion. In F. L. Bauer, M. Broy (eds.), Program Construction: International Summer School, LNCS 69, 54--57. Springer-Verlag, 1978.]]

Digital Library

[9]

D. Eppstein. A heuristic approach to program inversion. In International Joint Conference on Artificial Intelligence (IJCAI-85), 219--221. Morgan Kaufmann. Inc., 1985.]]

[10]

R. P. Feynman. Feynman Lectures on Computation. Addison-Wesley, 1996. Edited by A. J. G. Hey and R. W. Allen.]]

Digital Library

[11]

R. W. Floyd. Nondeterministic algorithms. Journal of the ACM, 14(4):636--644, 1967.]]

Digital Library

[12]

R. Glück, M. Kawabe. A program inverter for a functional language with equality and constructors. In A. Ohori (ed.), Programming Languages and Systems. Proceedings, LNCS 2895, 246--264. Springer-Verlag, 2003.]]

[13]

R. Glück, M. Kawabe. Derivation of deterministic inverse programs based on LR parsing. In Y. Kameyama, P. J. Stuckey (eds.), Functional and Logic Programming. Proceedings, LNCS 2998, 291--306. Springer-Verlag, 2004.]]

[14]

R. Glück, Y. Kawada, T. Hashimoto. Transforming interpreters into inverse interpreters by partial evaluation. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, 10--19. ACM Press, 2003.]]

Digital Library

[15]

D. Gries. The Science of Programming, chapter 21 Inverting Programs, 265--274. Texts and Monographs in Computer Science. Springer-Verlag, 1981.]]

[16]

Z. Hu, S.-C. Mu, M. Takeichi. A programmable editor for developing structured documents based on bidirectional transformations. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 178--189. ACM Press, 2004.]]

Digital Library

[17]

R. E. Korf. Inversion of applicative programs. In International Joint Conference on Artificial Intelligence (IJCAI-81), 1007--1009. William Kaufmann, Inc., 1981.]]

[18]

S.-C. Mu, R. Bird. Inverting functions as folds. In E. A. Boiten, B. Möller (eds.), Mathematics of Program Construction. Proceedings, LNCS 2386, 209--232. Springer-Verlag, 2002.]]

Digital Library

[19]

S.-C. Mu, Z. Hu, M. Takeichi. An injective language for reversible computation. In D. Kozen (ed.), Mathematics of Program Construction. Proceedings, LNCS 3125, 289--313. Springer-Verlag, 2004.]]

[20]

M. D. Peters, C. D. Carothers. An algorithm for fully reversible optimistic parallel simulation. In S. Chick, et al. (eds.), Proceedings of the 2003 Winter Simulation Conference, 864--871, 2003.]]

Digital Library

[21]

T. Toffoli. Reversible computing. In J. W. de Bakker, J. van Leeuwen (eds.), Automata, Languages and Programming. Proceedings, LNCS 85, 632--644. Springer-Verlag, 1980.]]

Digital Library

[22]

J. L. A. van de Snepscheut. Inversion of a recursive tree traversal. Information Processing Letters, 39(5):265--267, 1991.]]

Digital Library

Cited By

Glück RNormann L(2024)Inversion by Partial Evaluation: A Reversible Interpreter ExperimentElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.413.1413(1-14)Online publication date: 30-Nov-2024
https://doi.org/10.4204/EPTCS.413.1
Glück RYokoyama T(2023)Reversible computing from a programming language perspectiveTheoretical Computer Science10.1016/j.tcs.2022.06.010953:COnline publication date: 10-Apr-2023
https://dl.acm.org/doi/10.1016/j.tcs.2022.06.010
Glück RKaarsgaard RYokoyama T(2022)From reversible programming languages to reversible metalanguagesTheoretical Computer Science10.1016/j.tcs.2022.02.024920:C(46-63)Online publication date: 12-Jun-2022
https://dl.acm.org/doi/10.1016/j.tcs.2022.02.024
Show More Cited By

Index Terms

Revisiting an automatic program inverter for Lisp
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Completing Herbelin's programme
TLCA'07: Proceedings of the 8th international conference on Typed lambda calculi and applications

In 1994 Herbelin started and partially achieved the programme of showing that, for intuitionistic implicational logic, there is a Curry-Howard interpretation of sequent calculus into a variant of the λ-calculus, specifically a variant which manipulates ...
Revisiting the Correspondence between Cut Elimination and Normalisation
ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming

Cut-free proofs in Herbelin's sequent calculus are in 1-1 correspondence with normal natural deduction proofs. For this reason Herbelin's sequent calculus has been considered a privileged middle-point between L-systems and natural deduction. However, ...
Revisiting quantification in autoepistemic logic

In this article, we introduce first-order autoepistemic logic. Our definition is semantical and is based on the intuition similar to that lying behind the definition of first-order default logic. Thus, our definition of first-order autoepistemic logic ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 5

May 2005

47 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1071221

Issue’s Table of Contents

Copyright © 2005 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2005

Published in SIGPLAN Volume 40, Issue 5

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
216
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Glück RNormann L(2024)Inversion by Partial Evaluation: A Reversible Interpreter ExperimentElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.413.1413(1-14)Online publication date: 30-Nov-2024
https://doi.org/10.4204/EPTCS.413.1
Glück RYokoyama T(2023)Reversible computing from a programming language perspectiveTheoretical Computer Science10.1016/j.tcs.2022.06.010953:COnline publication date: 10-Apr-2023
https://dl.acm.org/doi/10.1016/j.tcs.2022.06.010
Glück RKaarsgaard RYokoyama T(2022)From reversible programming languages to reversible metalanguagesTheoretical Computer Science10.1016/j.tcs.2022.02.024920:C(46-63)Online publication date: 12-Jun-2022
https://dl.acm.org/doi/10.1016/j.tcs.2022.02.024
Yamaguchi MMatsuda KDavid CWang M(2022)Synbit: synthesizing bidirectional programs using unidirectional sketchesFormal Methods in System Design10.1007/s10703-023-00436-961:2-3(198-247)Online publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1007/s10703-023-00436-9
Mikkelsen MGlück RKirkeby M(2021)An Inversion Tool for Conditional Term Rewriting Systems - A Case Study of Ackermann InversionElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.341.3341(33-41)Online publication date: 6-Sep-2021
https://doi.org/10.4204/EPTCS.341.3
Yamaguchi MMatsuda KDavid CWang M(2021)Synbit: synthesizing bidirectional programs using unidirectional sketchesProceedings of the ACM on Programming Languages10.1145/34854825:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485482
Nishida NNiwa M(2021)Determinization of inverted grammar programs via context-free expressionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2021.100688122(100688)Online publication date: Aug-2021
https://doi.org/10.1016/j.jlamp.2021.100688
Kirkeby MGlück RGabbrielli MAbel ACheney J(2020)Inversion Framework: Reasoning about Inversion by Conditional Term Rewriting SystemsProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414089(1-14)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414089
Glück RKaarsgaard RYokoyama T(2019)Reversible Programs Have Reversible SemanticsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54997-8_26(413-427)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-54997-8_26
Kirkeby MGlück R(2019)Semi-inversion of Conditional Constructor Term Rewriting SystemsLogic-Based Program Synthesis and Transformation10.1007/978-3-030-45260-5_15(243-259)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-45260-5_15
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents