On typed and untyped lambda-terms (Տիպիզացված և ոչ տիպիզացված լամբդա-թերմերի մասին)

Համառոտագիր

Typed λ-terms that use variables of any order and don’t use constants of order > 1 are studied in the paper. Used constants of order 1 are strong computable functions and each of them has an untyped λ-term, which λ-defines it. Besides, for the set of built-in functions there exists such a notion of δreduction, that every typed term has a single normal form. An algorithm of translation of typed λ-terms to untyped λ-terms is presented. According to that algorithm, each typed term t is mapped to an untyped term t 0 . We study in which case typed termst1, t2 such that t1 →→βδ t2 correspond to untyped terms t1 0 ,t2 0 such that t1 0 →→β t2 0 .