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.

---

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).