Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: reduction calculi

Sortuj według:

Ogranicz wyniki do:

Gamma-Reduction in Type Theory of Acyclic Recursion

Loukanova Roussanka

Fundamenta Informaticae

2019

Vol. 170, nr 4

367--411

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.