Conversion Typed Functions into Relational Form
https://doi.org/10.15514/ISPRAS-2018-30(2)-3
Abstract
Relational programming is an approach that allows you to execute programs in different "directions" to get different behaviors from one relational specification. The direct development of relational programs is a complex task, requiring the developer to have certain skills. However, in many cases, the required relational program can be obtained from a certain functional program automatically. In this paper, the problem of automatic conversion of functional programs into relational ones is considered. The main contribution of the paper is the method of converting typed functions into a relational form, as well as proving its static and dynamic correctness. This method can be applied to typed programs of a general kind. To describe these programs, a compact ML-like language (a subset of OCaml) is used, equipped with a Hindley-Milner type system with let-polymorphism Also, the paper discusses the limitations of the proposed method, presents an implementation for a subset of the OCaml language, and evaluates the method on a number of realistic examples.
About the Authors
P. . Lozov
St. Petersburg State University
Russian Federation
Russian Federation
D. . Boulytchev
St. Petersburg State University
Russian Federation
Russian Federation
References
1. Friedman D. P., E.Byrd W., Kiselyov O. The Reasoned Schemer. MIT Press, 2005.
2. Mercury Language. URL: https://mercurylang.org (accessed 09.04.2018).
3. Curry Language. URL: http://www-ps.informatik.uni-kiel.de/currywiki (дата обращения 09.04.2018).
4. miniKanren Language. URL: http://minikanren.org (accessed 09.04.2018).
5. Hemann J., Friedman D. P. µKanren: A Minimal Core for Relational Programming. Workshop on Scheme and Functional Programming, 2013.
6. Byrd W. E. Relational Programming in miniKanren: Techniques, Applications, and Implementations. Ph.D. thesis, Indiana University, Bloomington, 2009.
7. Pierce B. Types and Programming Languages. MIT Press, 2002.
8. Koznov D. V. Methodology and tools for object-oriented modeling. PhD Thesis, SPBU, 2016 (in Russian).
9. Ol'khovich L., Koznov D.V. Ocl-based Automated Validation Method For Uml Specifications. Programming and Computer Software, 2003, vol. 29, № 6, pp. 323–327. DOI: 10.1023/B:PACS.0000004132.42846.11.
10. Terekhov A. N., Romanovskii K. Yu., Koznov D. V., Dolgov P. S., Ivanov A. N. RTST++: Methodology and a CASE Tool for the Development of Information Systems and Software For Real-Time Systems. Programming and Computer Software, 1999, vol. 25, № 5, pp. 276–281.
11. Codognet P., Diaz D. WAMCC: Compiling Prolog to C. The MIT Press, 1995, pp. 317–331.
12. Henderson F., Somogyi Z. Compiling mercury to high-level C code. In Computational Complexity, 2002, pp. 197–212.
13. Banbara M., Tamura N., Inoue K. Prolog Cafe: A prolog to Java translator system. Lecture Notes in Computer Science, vol. 4369, 2006, pp. 1–11.
14. G´omez-Zamalloa M., Albert E., Puebla G. Decompilation of Java bytecode to Prolog by partial evaluation. Information and Software Technology, 2009, vol. 51, № 10, pp. 1409–1427.
15. Calejo M. InterProlog: Towards a Declarative Embedding of Logic Programming in Java. JELIA 2004: Logics in Artificial Intelligence, pp. 714-717.
16. J. Cook J. P#: A concurrent Prolog for the .NET framework. Software Practice and Experience, vol. 34. № 9, 2004, pp. 815-845.
17. Byrd W. E., Holk E., Friedman D. P. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl), Workshop on Scheme and Functional Programming, 2012.
18. Kosarev D., Boulytchev D. Typed Embedding of a Relational Language in OCaml. ACM SIGPLAN Workshop on ML, 2016.
19. Язык OCanren. URL: http://github.com/dboulytchev/ocanren (accessed 09.04.2018).
20. Alvis C. E., Willcock J. J., Byrd W. E. cKanren: miniKanren with Constraints, Workshop on Scheme and Functional Programming, 2011.
21. Byrd W. E., Ballantyne M., Rosenblatt G., Might M. A Unified Approach to Solving Seven Programming Problems (Functional Pearl). Proc. ACM Program. Lang, 2017, vol. 1, ICFP, pp. 8:1–8:26.
22. Barendregt H. Lambda Calculi with Types. Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993.
Review
For citations:
Lozov P., Boulytchev D. Conversion Typed Functions into Relational Form. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(2):45-64. (In Russ.) https://doi.org/10.15514/ISPRAS-2018-30(2)-3
Email this article 