Gamma-Reduction in Type Theory of Acyclic Recursion

In this article, we introduce Moschovakis higher-order type theory of acyclic recursion L ar λ . We present the potentials of L ar λ for incorporating different reduction systems in L ar λ , with corresponding reduction calculi. At first, we introduce the original reduction calculus of L ar λ , which reduces L ar λ -terms to their canonical forms. This reduction calculus determines the relation of referential, i.e., algorithmic, synonymy between L ar λ -terms with respect to a chosen semantic structure. Our contribution is the definition of a (γ) rule and extending the reduction calculus of L ar λ 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 L ar λ .