Fundamenta Informaticae - Volume 170, issue 4

Authors: Darkey-Mensah, Mawunyo Kofi | Koprowski, Przemysław

Article Type: Research Article

Abstract: We present a generalization of a polynomial factorization algorithm that works with ideals in maximal orders of global function fields. The method presented in this paper is intrinsic in the sense that it does not depend on the embedding of the ring of polynomials into the Dedekind domain in question.

Keywords: Dedekind domain, ideal factorization, polynomial factorization, algorithm, square-free decomposition

DOI: 10.3233/FI-2019-1865

Citation: Fundamenta Informaticae, vol. 170, no. 4, pp. 325-338, 2019

Authors: Ketema, Jeroen | Simonsen, Jakob Grue

Article Type: Research Article

Abstract: We define computable infinitary rewriting by introducing computability to the study of strongly convergent infinite reductions over infinite first-order terms. Given computable infinitary reductions, we show that descendants and origins—essential to proving fundamental properties such as compression and confluence—are computable across such reductions.

Keywords: Infinitary term rewriting, computability, descendants, origins, needed reductions

DOI: 10.3233/FI-2019-1866

Citation: Fundamenta Informaticae, vol. 170, no. 4, pp. 339-365, 2019

Authors: Loukanova, Roussanka

Article Type: Research Article

Abstract: 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 λ . Show more

Keywords: algorithms, type theory recursion, acyclic recursion, reduction calculi, gamma-reduction, canonical form

DOI: 10.3233/FI-2019-1867

Citation: Fundamenta Informaticae, vol. 170, no. 4, pp. 367-411, 2019