On canonical notion of δ-reduction and on translation of typed λ-terms into untyped λ-terms (δ-Ռեդուկցիայի կանոնական գաղափարը և տիպիզացված λ-թերմերի թարգմանությունն առանց տիպերի λ-թերմերի)

Համառոտագիր

In the paper typed and untyped λ-terms are considered. Typed λ-terms use variables of any order and constants of order ≤ 1. Constants of order 1 are strong computable functions 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 functional programming languages. For the canonical notion of δ-reduction the translation of typed λ-terms into untyped λ-terms is studied.