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: JOUR
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 todo:paper_00224049_v129_n2_p173_Puddu
record_format dspace
spelling todo:paper_00224049_v129_n2_p173_Puddu2023-10-03T14:32:36Z An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs 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. JOUR 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)
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 JOUR
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
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_ 1807318455573020672

Ejemplares similares