Abstract
We present a method for synthesising recursive inverses for first-order functions. Since inverse functions are not, in general, single-valued, we introduce a powerdomain to define their semantics, in terms of which we express their transformation into recursive form. First, inverses that require unification at run-time are synthesised and these are then optimised by term-rewriting based on a set of axioms that facilitates a form of compile-time unification. The optimisations reduce the dependency on run-time unification, in many instances removing it entirely to give a recursive inverse. The efficiency of the use of relations in two modes is thereby improved, so enhencing extended functional languages endowed with logical variables and narrowing semantics. Our function-level, axiomatised system is more generally applicable than previous approaches to this type of optimis tion, and in general induces more mechanisable transformation systems.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
[Backus78] Backus, J.W.; Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. CACM 21 (8), 613–641 (1978)
[Bird87] Bird, R.S.; A calculus of functions for program synthesis. Research Report, PRG. Oxford: Oxford University 1987
[Darlington82] Darlington, J.: Program transformation. In: Darlington, J., Henderson, P., Turner, D.A. (eds) Functional programming and its applications. Cambridge: Cambridge University Press 1982
[Darlington86] Darlington, J., Field, A.J., Pull, H.: The unification of functional and logic languages. In: Degroot, D., Lindstrom, G. (eds.) Logic languages, pp. 37–70. Englewood Cliffs: Prentice-Hall 1986
[Darlington89] Darlington, J. et al.: A functional programming environment supporting execution, partial execution and transformation. in proc. PARLE, France, 1989
[Dybjer88] Dybjer, P.; Inverse image analysis generalises strictness analysis. Research Report, Chalmers University of Technology and University of Goteborg, Sweden, 1988
[Harrison91] Harrison, P.G., Khoshnevisan, H.: The mechanical transformation of data types. Comput. J. To appear 1992
[Harrison92] Harrison, P.G., Khoshnevisan, H.: ‘A new approach to recursion removal’, Theoret. Comput. Sci. To appear 1992
[Khoshnevisan89] Khoshnevisan, H., Sephton, K.M.: ‘An automatic function inverter’. 3rd International Conference on Rewriting Techniques and Applications (Lect. Notes Comput. Sci. Vol. 355) Berlin, Heidelberg New York: Springer 1989
[Kieburtz81] Kieburtz, R.B., Shultis, J.: ‘Transformations of FP program schemes’. ACM Conference on Functional Languages and Computer Architecture. Portsmouth, New Hampshire 1981
[Lillie91] Lillie, D.J., Harrison, P.G.: ‘A projection model of types’. International Conference on Functional Programming Languages and Computer Architecture, Cambridge, MA USA 1991
[Milner78] Milner, R.: ‘A theory of type polymorphism in programming’. J. Comput. System Sci. 17, 348–375 (1978)
[Robinson65] Robinson, J.A.: ‘A machine-oriented logic based on the resolution principle’. JACM 12 (1), 23–41 (1965)
[Romanenko88] Romanenko, A.Y.: ‘The generation of inverse functions in REFAL’. In: Bjorner, D., Ershov, A.P., Jones, N.D. (eds) Partial evaluation and mixed computation; pp. 427–444. Amsterdam: North-Holland 1988
[Plotkin76] Plotkin, G.D.: ‘A powerdomain construction’. SIAM J. Comput. 5, 452–487 (1976)
[Plotkin81] Plotkin, G.D.: ‘Lecture notes on domain theory’. (unpublished) University of Edinburgh 1981
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Harrison, P.G., Khoshnevisan, H. On the synthesis of function inverses. Acta Informatica 29, 211–239 (1992). https://doi.org/10.1007/BF01185679
Received:
Issue date:
DOI: https://doi.org/10.1007/BF01185679