ON TRANSLATION OF TYPED FUNCTIONAL PROGRAMS INTO UNTYPED FUNCTIONAL PROGRAMS
DOI:
https://doi.org/10.46991/PYSU:A/2017.51.2.177Keywords:
typed functional program, untyped functional program, basic semantics, translation, l-definabilityAbstract
In this paper typed and untyped functional programs are considered. Typed functional programs use variables of any order and constants of order $\le$1, where constants of order 1 are strong computable, $\lambda$-definable functions with indeterminate values of arguments. The basic semantics of a typed functional program is a function with indeterminate values of arguments, which is the main component of its least solution. The basic semantics of an untyped functional program is an untyped $\lambda$-term, which is defined by means of a fixed point combinator. An algorithm that translates typed functional program $P$ into untyped functional program $P'$ is suggested. It is proved that the basic semantics of the program $P'$ $\lambda$-defines the basic semantics of the program $P$.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2017 Proceedings of the YSU
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.