Skip to main content
SpringerLink
Log in
Book cover

The Essence of Computation pp 269–295Cite as

Principles of Inverse Computation and the Universal Resolving Algorithm

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2566))

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.

On leave from DIKU, Department of Computer Science, University of Copenhagen.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. M. Abramov. RuMetavychislenija i logicheskoe programmirovanie (Metacomputation and logic programming). Programmirovanie, 3:31–44, 1991. (In Russian).

    Google Scholar 

  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.

    Google Scholar 

  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.

    Chapter  Google Scholar 

  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.

    Article  Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  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.

    Chapter  Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

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

    Google Scholar 

  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.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  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.

    Chapter  Google Scholar 

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

    Google Scholar 

  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.

    Google Scholar 

  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).

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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.

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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.

    Google Scholar 

  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.

    Chapter  Google Scholar 

  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.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  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.

    Google Scholar 

  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.

    Chapter  Google Scholar 

  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.

    Google Scholar 

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

    Google Scholar 

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

    Article  MATH  Google Scholar 

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

    Google Scholar 

  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).

    Google Scholar 

  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.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  52. P. Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73:231–248, 1990.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Program Systems Institute, Russian Academy of Sciences, RU-152140, Pereslavl-Zalessky, Russia

    Sergei Abramov

  2. PRESTO, JST & Institute for Software Production Technology, Waseda University, School of Science and Engineering, Tokyo, 169-8555, Japan

    Robert Glück

Authors
  1. Sergei Abramov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert Glück
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DIKU, University of Copenhagen, Universitetsparken 1, 2100, Copenhagen, Denmark

    Torben Æ. Mogensen

  2. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, 66506, Manhattan, KS, USA

    David A. Schmidt

  3. Department of Computer Science, University of Texas at Dallas, P.O. Box 830688, 75083, Richardson, TX, USA

    I. Hal Sudborough

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Abramov, S., Glück, R. (2002). Principles of Inverse Computation and the Universal Resolving Algorithm. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds) The Essence of Computation. Lecture Notes in Computer Science, vol 2566. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36377-7_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-36377-7_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00326-7

  • Online ISBN: 978-3-540-36377-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation