ON TYPED AND UNTYPED LAMBDA-TERMS Tigran Khondkaryan
Typedλ-terms that use variables of any order and don’t use constants oforder>1 are studied in the paper. An algorithm of translation of typedλ-terms to untypedλ-terms is presented. According to that algorithm, eachtyped termtis mapped to an untyped termt′. We study in which case typedtermst1,t2such thatt1→→β δt2correspond to untyped termst1′,t2′such thatt1′→→βt2′.
DOI: 10.46991/PYSUA.2015.49.2.045 Physical and Mathematical Sciences, 49(2 (237) 45-52
