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′.
No institution available
Mathematics
, 2025, Issue 1, pp. 1–10
ISSN Online: 0000-0000
DOI:
10.xxxx/example-doi