ON INTERPRETATION OF TYPED AND UNTYPED FUNCTIONAL PROGRAMS
This work is licensed under Creative Commons Attribution–NonCommercial International License
(CC BY-NC 4.0).
Abstract
In this paper the interpretation algorithms for 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 strongly computable, monotonic functions with indeterminate values of arguments. The basic semantics of the typed functional program is a function with indeterminate values of arguments, which is the main component of its least solution. The interpretation algorithms of typed functional programs are based on substitutions, β-reduction and canonical δ-reduction. The basic semantics of the untyped functional program is the untyped λ-term, which is defined by means of the fixed point combinator. The interpretation algorithms of untyped functional programs are based on substitutions and β-reduction. Interpretation algorithms are examined for completeness and comparability. It is investigated how the “behavior” of the interpretation algorithm changes after translation of typed functional program into untyped functional program.