Roussanka Loukanova: Gamma-Reduction in Type Theory of Acyclic Recursion

Abstract:
I will introduce Moschovakis Type Theory of Acyclic Recursion (TTAR) by extending its reduction system. The extended TTAR has potentials for more efficient computational semantics of formal and natural languages.

At first, I will present the original reduction calculus of TTAR, which reduces TTAR-terms to their canonical forms. The canonical forms of the terms determine the algorithms that compute their semantic denotations, and, in addition, the relation of algorithmically referential synonymy between TTAR-terms. The lambda-rule, which is the most important rule of the reduction calculus of TTAR, strictly preserves the algorithmic structure of the reduced terms. However, in its original, general formulation, the lambda-rule may result in superfluous lambda abstractions in some parts of the terms.

In the second part of the talk, I introduce the gamma-rule, which extends the reduction calculus of TTAR and its referential synonymy to gamma-reduction calculus and gamma-synonymy, respectively. The gamma-rule is useful for simplifying terms. It reduces superfluous lambda-abstraction and corresponding functional applications in the terms, while retaining the major algorithmic structure of the terms.