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.

‹ 1 / ? › − 100% + Open in new tab Download Cite

Loading the full text…