More Web Proxy on the site http://driver.im/

chapter

Principles of inverse computation and the Universal resolving algorithm

Authors:

Sergei Abramov,

Robert GlückAuthors Info & Claims

The essence of computation: complexity, analysis, transformation

January 2002

Pages 269 - 295

Published: 01 January 2002 Publication History

Abstract

We survey fundamental concepts in inverse programming and present the Universal Resolving Algorithm (URA), an algorithm for inverse computation in a first-order, functional programming language. We discuss the principles behind the algorithm, including a three-step approach based on the notion of a perfect process tree, and demonstrate our implementation with several examples. We explain the idea of a semantics modifier for inverse computation which allows us to perform inverse computation in other programming languages via interpreters.

References

[1]

{1} S. M. Abramov. Metavychislenija i logicheskoe programmirovanie (Metacomputation and logic programming). Programmirovanie, 3:31-44, 1991. (In Russian).]]

[2]

{2} S. M. Abramov, R. Glück. Combining semantics with non-standard interpreter hierarchies. In S. Kapoor, S. Prasad (eds.), Foundations of Software Technology and Theoretical Computer Science. Proceedings, LNCS 1974, 201-213. Springer-Verlag, 2000.]]

Digital Library

[3]

{3} S.M. Abramov, R. Glück. The universal resolving algorithm: inverse computation in a functional language. In R. Backhouse, J. N. Oliveira (eds.), Mathematics of Program Construction. Proceedings, LNCS 1837, 187-212. Springer-Verlag, 2000.]]

Digital Library

[4]

{4} S.M. Abramov, R. Glück. From standard to non-standard semantics by semantics modifiers. International Journal of Foundations of Computer Science. 12(2):171 211, 2001.]]

[5]

{5} S. M. Abramov, R. Glück. The universal resolving algorithm and its correctness: inverse computation in a functional language. Science of Computer Programming, 43(2-3):193-229, 2002.]]

[6]

{6} E. Albert, G. Vidal. The narrowing-driven approach to functional logic program specialization. New Generation Computing, 20(1):3-26, 2002.]]

Digital Library

[7]

{7} R. Bird, O. de Moor. Algebra of Programming. Prentice Hall International Series in Computer Science. Prentice Hall, 1997.]]

Digital Library

[8]

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

Digital Library

[9]

{9} M. Davis, H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960.]]

Digital Library

[10]

{10} E.W. Dijkstra. EWD671: Program inversion. In Selected Writings on Computing: A Personal Perspective, 351-354. Springer-Verlag, 1982.]]

[11]

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

Digital Library

[12]

{12} Y. Futamura. Partial evaluation of computing process - an approach to a compiler-compiler. Systems, Computers, Controls, 2(5):45-50, 1971.]]

[13]

{13} Y. Futamura, K. Nogi. Generalized partial computation. In D. Bjørner, A. P. Ershov, N. D. Jones (eds.), Partial Evaluation and Mixed Computation, 133-151. North-Holland, 1988.]]

[14]

{14} P. C. Gilmore. A proof method for quantification theory: its justification and realization. IBM Journal of Research and Development, 4:28-35, 1960.]]

Digital Library

[15]

{15} R. Glück, A. V. Klimov. Occam's razor in metacomputation: the notion of a perfect process tree. In P. Cousot, M. Falaschi, G. Filé, A. Rauzy (eds.), Static Analysis. Proceedings, LNCS 724, 112-123. Springer-Verlag, 1993.]]

Digital Library

[16]

{16} R. Glück, A. V. Klimov. Metacomputation as a tool for formal linguistic modeling. In R. Trappl (ed.), Cybernetics and Systems '94, Vol. 2, 1563-1570. World Scientific, 1994.]]

[17]

{17} R. Glück, A. V. Klimov. A regeneration scheme for generating extensions. Information Processing Letters, 62(3):127-134, 1997.]]

Digital Library

[18]

{18} R. Glück, A. V. Klimov. On the degeneration of program generators by program composition. New Generation Computing, 16(1):75-95, 1998.]]

Digital Library

[19]

{19} R. Glück, M. Leuschel. Abstraction-based partial deduction for solving inverse problems - a transformational approach to software verification (extended abstract). In D. Bjørner, M. Broy, A. V. Zamulin (eds.), Perspectives of System Informatics. Proceedings, LNCS 1755, 93-100. Springer-Verlag, 2000.]]

Digital Library

[20]

{20} R. Glück, M. H. Sørensen. Partial deduction and driving are equivalent. In M. Hermenegildo, J. Penjam (eds.), Programming Language Implementation and Logic Programming. Proceedings, LNCS 844, 165-181. Springer-Verlag, 1994.]]

Digital Library

[21]

{21} R. Glück, M. H. Sørensen. A roadmap to metacomputation by supercompilation. In O. Danvy, R. Glück, P. Thiemann (eds.), Partial Evaluation. Proceedings, LNCS 1110, 137-160. Springer-Verlag, 1996.]]

Digital Library

[22]

{22} R. Glück, V. F. Turchin. Application of metasystem transition to function inversion and transformation. In Int. Symposium on Symbolic and Algebraic Computation (ISSAC'90), 286-287. ACM Press, 1990.]]

Digital Library

[23]

{23} C. Green. Application of theorem proving to problem solving. In D. E. Walker, L. M. Norton (eds.), Int. Joint Conference on Artificial Intelligence (IJCAI-69), 219-239. William Kaufmann, Inc., 1969.]]

[24]

{24} D. Gries. The Science of Programming. Texts and Monographs in Computer Science. Springer-Verlag, 1981.]]

Digital Library

[25]

{25} D. Gries, J. L. A. van de Snepscheut. Inorder traversal of a binary tree and its inversion. In E. W. Dijkstra (ed.), Formal Development of Programs and Proofs, 37-42. Addison Wesley, 1990.]]

Digital Library

[26]

{26} M. Hanus. The integration of functions into logic programming: from theory to practice. Journal of Logic Programming, 19&20:583-628, 1994.]]

[27]

{27} P. G. Harrison, H. Khoshnevisan. On the synthesis of function inverses. Acta Informatica, 29:211-239, 1992.]]

Digital Library

[28]

{28} J. Hatcliff. An introduction to online and offline partial evaluation using a simple flowchart language. In J. Hatcliff, T. Mogensen, P. Thiemann (eds.), Partial Evaluation. Practice and Theory, LNCS 1706, 20-82. Springer-Verlag, 1999.]]

Digital Library

[29]

{29} N. D. Jones. The essence of program transformation by partial evaluation and driving. In N. D. Jones, M. Hagiya, M. Sato (eds.), Logic, Language and Computation, LNCS 792, 206-224. Springer-Verlag, 1994.]]

[30]

{30} N.D. Jones, C. K. Gomard, P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.]]

Digital Library

[31]

{31} H. Khoshnevisan, K. M. Sephton. InvX: An automatic function inverter. In N. Dershowitz (ed.), Rewriting Techniques and Applications (RTA '89), LNCS 355, 564-568. Springer-Verlag, 1989.]]

Digital Library

[32]

{32} A. V. Klimov, S. A. Romanenko. Metavychislitel' dlja jazyka Refal. Osnovnye ponjatija i primery. (A metaevaluator for the language Refal. Basic concepts and examples). Preprint 71, Keldysh Institute of Applied Mathematics, Academy of Sciences of the USSR, Moscow, 1987. (in Russian).]]

[33]

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

[34]

{34} R. Kowalski. Predicate logic as programming language. In J. L. Rosenfeld (ed.), Information Processing 74, 569-574. North-Holland, 1974.]]

[35]

{35} M. Leuschel, T. Massart. Infinite state model checking by abstract interpretation and program specialisation. In A. Bossi (ed.), Logic-Based Program Synthesis and Transformation. Proceedings, LNCS 1817, 62-81. Springer-Verlag, 2000.]]

Digital Library

[36]

{36} J. W. Lloyd. Foundations of Logic Programming. Second, extended edition. Springer-Verlag, 1987.]]

Digital Library

[37]

{37} K. Marriott, P. J. Stuckey. Programming with Constraints. MIT Press, 1998.]]

[38]

{38} J. McCarthy. The inversion of functions defined by Turing machines. In C. E. Shannon, J. McCarthy (eds.), Automata Studies, 177-181. Princeton University Press, 1956.]]

[39]

{39} 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

[40]

{40} A. P. Nemytykh, V. A. Pinchuk. Program transformation with metasystem transitions: experiments with a supercompiler. In D. Bjørner, M. Broy, I. V. Pottosin (eds.), Perspectives of System Informatics. Proceedings, LNCS 1181, 249-260. Springer-Verlag, 1996.]]

Digital Library

[41]

{41} J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, 1965.]]

Digital Library

[42]

{42} A. Y. Romanenko. The generation of inverse functions in Refal. In D. Bjørner, A. P. Ershov, N. D. Jones (eds.), Partial Evaluation and Mixed Computation, 427-444. North-Holland, 1988.]]

[43]

{43} J. P. Secher, M. H. Sørensen. On perfect supercompilation. In D. Bjørner, M. Broy, A. Zamulin (eds.), Perspectives of System Informatics. Proceedings, LNCS 1755, 113-127. Springer-Verlag, 2000.]]

Digital Library

[44]

{44} J. P. Secher, M. H. Sørensen. From checking to inference via driving and DAG grammars. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, 41-51. ACM Press, 2002.]]

Digital Library

[45]

{45} P. Sestoft. The structure of a self-applicable partial evaluator. Technical Report 85/11, DIKU, University of Copenhagen, Denmark, Nov. 1985.]]

Digital Library

[46]

{46} M. H. Sørensen, R: Glück, N. D. Jones. A positive supercompiler. Journal of Functional Programming, 6(6):811-838, 1996.]]

[47]

{47} L. Sterling, E, Shapiro. The Art of Prolog. Second Edition. MIT Press, 1994.]]

[48]

{48} V. F. Turchin. Ehkvivalentnye preobrazovanija rekursivnykh funkcij na Refale (Equivalent transformations of recursive functions defined in Refal). In Teorija Jazykov i Metody Programmirovanija (Proceedings of the Symposium on the Theory of Languages and Programming Methods), 31-42, 1972, (In Russian).]]

[49]

{49} V. F. Turchin. The use of metasystem transition in theorem proving and program optimization. In J. W. de Bakker, J. van Leeuwen (eds.), Automata, Languages and Programming, LNCS 85, 645-657. Springer-Verlag, 1980.]]

Digital Library

[50]

{50} V. F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8(3):292-325, 1986.]]

Digital Library

[51]

{51} J.L.A. van de Snepscheut. What Computing is All About. Texts and Monographs in Computer Science. Springer-Verlag, 1993.]]

Digital Library

[52]

{52} P. Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73:231-248, 1990.]]

Digital Library

Cited By

Hoey JLanese INishida NUlidowski IVidal G(2020)A Case Study for Reversible Computing: Reversible Debugging of Concurrent ProgramsReversible Computation: Extending Horizons of Computing10.1007/978-3-030-47361-7_5(108-127)Online publication date: 9-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-47361-7_5
Axelsen HGlück R(2016)On reversible Turing machines and their function universalityActa Informatica10.1007/s00236-015-0253-y53:5(509-543)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s00236-015-0253-y
Kuraj IKuncak VJackson D(2015)Programming with enumerable sets of structuresACM SIGPLAN Notices10.1145/2858965.281432350:10(37-56)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2858965.2814323
Show More Cited By

Index Terms

Principles of inverse computation and the Universal resolving algorithm

Recommendations

An universal resolving algorithm for inverse computation of lazy languages
PSI'06: Proceedings of the 6th international Andrei Ershov memorial conference on Perspectives of systems informatics

The Universal Resolving Algorithm was originally formulated for inverse computation of tail-recursive programs. We present an extension to general recursion that improves the efficiency and termination of inverse computation because partially produced ...
The Principles of the Flix Programming Language
Onward! 2022: Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software

We present the design values and design principles of the Flix programming language, a functional-first, imperative, and logic programming language. We explain how these values and principles came into being and how they have influenced the design of ...
Design principles for internal domain-specific languages: a pattern catalog illustrated by Ruby
PLOP '10: Proceedings of the 17th Conference on Pattern Languages of Programs

Some programming languages, especially dynamic programming languages, offer suitable mechanisms for the construction of internal domain-specific languages (DSL). Internal DSLs inherit the facilities of their host language such as the availability of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide books

The essence of computation: complexity, analysis, transformation

January 2002

500 pages

ISBN:3540003266

Editors:
Torben Æ Mogensen
University of Copenhagen, DIKU, Universitetsparken 1, 2100 Copenhagen, Denmark
,
David A. Schmidt
Kansas State University, Department of Computing and Information Sciences, 234 Nichols Hall, Manhattan, KS
,
I. Hal Sudborough
University of Texas at Dallas, Department of Computer Science, P.O. Box 830688, Richardson, TX

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 2002

Qualifiers

Chapter

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hoey JLanese INishida NUlidowski IVidal G(2020)A Case Study for Reversible Computing: Reversible Debugging of Concurrent ProgramsReversible Computation: Extending Horizons of Computing10.1007/978-3-030-47361-7_5(108-127)Online publication date: 9-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-47361-7_5
Axelsen HGlück R(2016)On reversible Turing machines and their function universalityActa Informatica10.1007/s00236-015-0253-y53:5(509-543)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s00236-015-0253-y
Kuraj IKuncak VJackson D(2015)Programming with enumerable sets of structuresACM SIGPLAN Notices10.1145/2858965.281432350:10(37-56)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2858965.2814323
Foster JGreenwald MMoore JPierce BSchmitt A(2015)POPL 2005ACM SIGPLAN Notices10.1145/2854695.285470050:8S(49-62)Online publication date: 4-Dec-2015
https://dl.acm.org/doi/10.1145/2854695.2854700
Kuraj IKuncak VJackson DAldrich JEugster P(2015)Programming with enumerable sets of structuresProceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2814270.2814323(37-56)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2814270.2814323
Matsuda KInaba KNakano KKiselyov OThompson S(2012)Polynomial-time inverse computation for accumulative functions with multiple data traversalsProceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation10.1145/2103746.2103752(5-14)Online publication date: 23-Jan-2012
https://dl.acm.org/doi/10.1145/2103746.2103752
Matsuda KInaba KNakano K(2012)Polynomial-time inverse computation for accumulative functions with multiple data traversalsHigher-Order and Symbolic Computation10.1007/s10990-013-9097-825:1(3-38)Online publication date: 1-Mar-2012
https://dl.acm.org/doi/10.1007/s10990-013-9097-8
Axelsen HGlück R(2011)What do reversible programs compute?Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of software10.5555/1987171.1987176(42-56)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987171.1987176
Glück R(2011)Bootstrapping compiler generators from partial evaluatorsProceedings of the 8th international conference on Perspectives of System Informatics10.1007/978-3-642-29709-0_13(125-141)Online publication date: 27-Jun-2011
https://dl.acm.org/doi/10.1007/978-3-642-29709-0_13
Yokoyama TAxelsen HGlück R(2011)Towards a reversible functional languageProceedings of the Third international conference on Reversible Computation10.1007/978-3-642-29517-1_2(14-29)Online publication date: 4-Jul-2011
https://dl.acm.org/doi/10.1007/978-3-642-29517-1_2
Show More Cited By

View Options

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 Chapter

Media

Figures

Other

Tables

View Table of Contents