Abstract

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′.

‹ 1 / ? › − 100% + Open in new tab Download Cite

Loading the full text…