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 $\leq 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, $\beta$-reduction and canonical $\delta$-reduction. The basic semantics of the untyped functional program is the untyped $\lambda$-term, which is defined by means of the fixed point combinator. The interpretation algorithms of untyped functional programs are based on substitutions and $\beta$-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.
Fulltext:
PDF file (202 kB)