ON TRANSLATION OF TYPED FUNCTIONAL PROGRAMS INTO UNTYPED FUNCTIONAL PROGRAMS
This work is licensed under Creative Commons Attribution–NonCommercial International License
(CC BY-NC 4.0).
Abstract
In this paper typed and untyped functional programs are considered. Typed functional programs use variables of any order and constants of order ≤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.