Affiliations: Department of Mathematics, Stockholm University, Stockholm, Sweden. [email protected]
Correspondence:
[*]
Address for correspondence: Department of Mathematics, Stockholm University, SE–106 91 Stockholm, Sweden.
Note: [†] Also affiliated at: Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria.
Abstract: In this article, we introduce Moschovakis higher-order type theory of acyclic recursion Larλ. We present the potentials of Larλ for incorporating different reduction systems in Larλ, with corresponding reduction calculi. At first, we introduce the original reduction calculus of Larλ, which reduces Larλ-terms to their canonical forms. This reduction calculus determines the relation of referential, i.e., algorithmic, synonymy between Larλ-terms with respect to a chosen semantic structure. Our contribution is the definition of a (γ) rule and extending the reduction calculus of Larλ and its referential synonymy to γ-reduction and γ-synonymy, respectively. The γ-reduction is very useful for simplification of terms in canonical forms, by reducing subterms having superfluous λ-abstraction and corresponding functional applications. Typically, such extra λ abstractions can be introduced by the λ-rule of the reduction calculus of Larλ.
Keywords: algorithms, type theory recursion, acyclic recursion, reduction calculi, gamma-reduction, canonical form
