In the paper typed and untyped λ-terms are considered. Typed λ-terms use variablesof any order and constants of order ≤1. Constants of order 1 are strong computablefunctions with indeterminate values of arguments and every function has an untyped λ-term that λ-defines it. The so-called canonical notion of δ-reduction is introduced.This is the notion of δ-reduction that is used in the implementation of functionalprogramming languages. For the canonical notion of δ-reduction the translation of typed λ-terms into untyped λ-terms is studied.
No institution available
Mathematics
, 2025, Issue 1, pp. 1–10
ISSN Online: 0000-0000
DOI:
10.xxxx/example-doi