ON TRANSLATION OF TYPED FUNCTIONAL PROGRAMS INTO UNTYPED FUNCTIONAL PROGRAMS

This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Submitted: 2025-02-06; Published: 2025-02-06

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.