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.
No institution available
Mathematics
, 2025, Issue 1, pp. 1–10
ISSN Online: 0000-0000
DOI:
10.xxxx/example-doi