ON MAIN CANONICAL NOTION OF δ-REDUCTION

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.

Submitted: 2025-01-30; Published: 2025-01-30

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

Abstract

In this paper the main canonical notion of δ-reduction is considered. Typed λ-terms use variables of any order and constants of order ≤1, where constantsof order 1 are strongly computable, monotonic functions with indeterminatevalues of arguments. The canonical notion of δ-reduction is the notion of δ-reduction that is used in the implementation of functional programminglanguages. For main canonical notion of δ-reduction the uniqueness of β δ-normal form of typed λ-terms is shown.