An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs

Mostrar todas las versiones(3)

In this paper we obtain an effective algorithm for quantifier elimination over algebraically closed fields: For every effective infinite integral domain k, closed under the extraction of pth roots when the characteristic p of k is positive, and every prenex formula φ with r blocks of quantifiers inv...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Puddu, S., Sabia, J.
Formato: Artículo publishedVersion
Lenguaje:Inglés
Publicado: 1998
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_00224049_v129_n2_p173_Puddu
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paperaa:paper_00224049_v129_n2_p173_Puddu
record_format dspace
spelling paperaa:paper_00224049_v129_n2_p173_Puddu2023-06-12T16:44:47Z An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs J. Pure Appl. Algebra 1998;129(2):173-200 Puddu, S. Sabia, J. In this paper we obtain an effective algorithm for quantifier elimination over algebraically closed fields: For every effective infinite integral domain k, closed under the extraction of pth roots when the characteristic p of k is positive, and every prenex formula φ with r blocks of quantifiers involving s polynomials F1,...,Fs∈k[X1,...,Xn] encoded in dense form, there exists a well-parallelizable algorithm without divisions whose output is a quantifier-free formula equivalent to φ. The sequential complexity of this algorithm is bounded by O(|φ|) - D(O(n))r, where |φ| is the length of φ and D ≥ n is an upper bound for 1 + ∑si-1 deg Fi, and the polynomials in the output are encoded by means of a straight line program. The complexity bound obtained is better than the bounds of the known elimination algorithms, which are of the type |φ|.Dncr, where c ≥ 2 is a constant. This becomes notorious when r = 1 (i.e., when there is only one block of quantifiers): the complexity bounds known up to now are not less than Dn2, while our bound is DO(n). Moreover, in the particular case that there is only one block of existential quantifiers and the input polynomials are given by a straight line program, we construct an elimination algorithm with even better bounds which depend on the length of this straight line program: Given a formula of the type ∃xn-m + 1, . . . , ∃xn: F1(x1, . . . ,Xn) = 0 ∧ ⋯ ∧ Fs(x1, . . . ,Xn) = 0 ∧ G1(x1, . . . , Xn) ≠ 0 ∧ ⋯ ∧ Gs′ (x1, . . . ,xn) ≠ 0, where F1, . . . ,Fs ∈ k[X1, . . . ,Xn] are polynomials whose degrees in the m variables Xn-m+1,. . . ,Xn are bounded by an integer d ≥ m and G1, . . . ,Gs′ ∈ k[X1, . . . ,Xn] are polynomials whose degrees in the same variables are bounded by an integer δ, this algorithm eliminates quantifiers in time L2.(s.s′.δ)O(1).dO(m), where L is the length of the straight line program that encodes F1, . . . ,Fs, G1, . . . ,Gs′. Finally, we construct a fast algorithm to compute the Chow Form of an irreducible projective variety. The construction of all the algorithms mentioned above relies on a preprocessing whose cost exceedes the complexity classes considered (they are based on the construction of correct test sequences). In this sense, our algorithms are non-uniform but may be considered uniform as randomized algorithms (choosing the correct test sequences randomly). © 1998 Elsevier Science B.V. All rights reserved. Fil:Puddu, S. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Sabia, J. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 1998 info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion application/pdf eng info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00224049_v129_n2_p173_Puddu
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Inglés
orig_language_str_mv eng
description In this paper we obtain an effective algorithm for quantifier elimination over algebraically closed fields: For every effective infinite integral domain k, closed under the extraction of pth roots when the characteristic p of k is positive, and every prenex formula φ with r blocks of quantifiers involving s polynomials F1,...,Fs∈k[X1,...,Xn] encoded in dense form, there exists a well-parallelizable algorithm without divisions whose output is a quantifier-free formula equivalent to φ. The sequential complexity of this algorithm is bounded by O(|φ|) - D(O(n))r, where |φ| is the length of φ and D ≥ n is an upper bound for 1 + ∑si-1 deg Fi, and the polynomials in the output are encoded by means of a straight line program. The complexity bound obtained is better than the bounds of the known elimination algorithms, which are of the type |φ|.Dncr, where c ≥ 2 is a constant. This becomes notorious when r = 1 (i.e., when there is only one block of quantifiers): the complexity bounds known up to now are not less than Dn2, while our bound is DO(n). Moreover, in the particular case that there is only one block of existential quantifiers and the input polynomials are given by a straight line program, we construct an elimination algorithm with even better bounds which depend on the length of this straight line program: Given a formula of the type ∃xn-m + 1, . . . , ∃xn: F1(x1, . . . ,Xn) = 0 ∧ ⋯ ∧ Fs(x1, . . . ,Xn) = 0 ∧ G1(x1, . . . , Xn) ≠ 0 ∧ ⋯ ∧ Gs′ (x1, . . . ,xn) ≠ 0, where F1, . . . ,Fs ∈ k[X1, . . . ,Xn] are polynomials whose degrees in the m variables Xn-m+1,. . . ,Xn are bounded by an integer d ≥ m and G1, . . . ,Gs′ ∈ k[X1, . . . ,Xn] are polynomials whose degrees in the same variables are bounded by an integer δ, this algorithm eliminates quantifiers in time L2.(s.s′.δ)O(1).dO(m), where L is the length of the straight line program that encodes F1, . . . ,Fs, G1, . . . ,Gs′. Finally, we construct a fast algorithm to compute the Chow Form of an irreducible projective variety. The construction of all the algorithms mentioned above relies on a preprocessing whose cost exceedes the complexity classes considered (they are based on the construction of correct test sequences). In this sense, our algorithms are non-uniform but may be considered uniform as randomized algorithms (choosing the correct test sequences randomly). © 1998 Elsevier Science B.V. All rights reserved.
format Artículo
Artículo
publishedVersion
author Puddu, S.
Sabia, J.
spellingShingle Puddu, S.
Sabia, J.
An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
author_facet Puddu, S.
Sabia, J.
author_sort Puddu, S.
title An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
title_short An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
title_full An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
title_fullStr An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
title_full_unstemmed An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
title_sort effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
publishDate 1998
url http://hdl.handle.net/20.500.12110/paper_00224049_v129_n2_p173_Puddu
work_keys_str_mv AT puddus aneffectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
AT sabiaj aneffectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
AT puddus effectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
AT sabiaj effectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
_version_ 1769810020271128576

Ejemplares similares