ON CANONICAL NOTION OF $\delta$-REDUCTION AND ON TRANSLATION OF TYPED $\lambda$-TERMS INTO UNTYPED $\lambda$-TERMS
DOI:
https://doi.org/10.46991/PYSU:A/2017.51.1.046Keywords:
typed $\lambda$--term, untyped $\lambda$-term, translation, notion of $\delta$-reduction, $\lambda$-definabilityAbstract
In the paper typed and untyped $\lambda$-terms are considered. Typed $\lambda$-terms use variables of any order and constants of order $\leq$1. Constants of order 1 are strong computable functions with indeterminate values of arguments and every function has an untyped $\lambda$-term that $\lambda$-defines it. The so-called canonical notion of $\delta$-reduction is introduced. This is the notion of $\delta$-reduction that is used in the implementation of functional programming languages. For the canonical notion of $\delta$-reduction the translation of typed $\lambda$-terms into untyped $\lambda$-terms is studied.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2017 Proceedings of the YSU
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.