ON TRANSLATION OF TYPED FUNCTIONAL PROGRAMS INTO UNTYPED FUNCTIONAL PROGRAMS - Nigiyan, S.A.; Khondkaryan, T.V. (Proceedings of the YSU A: Physical and Mathematical Sciences, 2017)
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, $λ$-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 $λ$-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'$ $λ$-defines the basic semantics of the program $P$.
Keywords: typed functional program, untyped functional program, basic semantics, translation, l-definability