ON TYPED AND UNTYPED LAMBDA-TERMS

Tigran Khondkaryan

This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

This work is licensed under Creative Commons Attribution–NonCommercial International License (CC BY-NC 4.0).

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

Author(s)

Table of Contents

ON TYPED AND UNTYPED LAMBDA-TERMS

Abstract

Author(s)

Table of Contents

Related Articles

ON UNIQUENESS OF HOLOMORPHIC AND BOUNDED OUTSIDE THE CLOSED LOGARITHMIC SECTOR FUNCTIONS REPRESENTABLE BY LACUNARY POWER SERIES

COMPUTER DETECTING AND PROCESSING OF THE SIGNALS OF A FLAT-COIL ABSOLUTE-POSITION SENSOR BASED SEISMIC DETECTOR

ON TYPED AND UNTYPED LAMBDA-TERMS

Abstract

Subscribe to TheGufo Newsletter​

Subscribe to TheGufo Newsletter