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

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, Susana Isabel, Sabia, Juan Vicente Rafael
Publicado: 1998
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00224049_v129_n2_p173_Puddu
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 paper:paper_00224049_v129_n2_p173_Puddu
record_format dspace
spelling paper:paper_00224049_v129_n2_p173_Puddu2023-06-08T14:50:33Z An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs Puddu, Susana Isabel Sabia, Juan Vicente Rafael 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 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00224049_v129_n2_p173_Puddu 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.
author Puddu, Susana Isabel
Sabia, Juan Vicente Rafael
spellingShingle Puddu, Susana Isabel
Sabia, Juan Vicente Rafael
An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
author_facet Puddu, Susana Isabel
Sabia, Juan Vicente Rafael
author_sort Puddu, Susana Isabel
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 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00224049_v129_n2_p173_Puddu
http://hdl.handle.net/20.500.12110/paper_00224049_v129_n2_p173_Puddu
work_keys_str_mv AT puddususanaisabel aneffectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
AT sabiajuanvicenterafael aneffectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
AT puddususanaisabel effectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
AT sabiajuanvicenterafael effectivealgorithmforquantifiereliminationoveralgebraicallyclosedfieldsusingstraightlineprograms
_version_ 1768546102426992640

Ejemplares similares