半代数集 投影 量词消去

hbghlyj

Tarski-Seidenberg 定理: 由多项式方程和不等式的布尔组合定义的 $n+1$ 维空间中的集合投影到 $n$ 维空间得到的集合仍然可以由多项式方程和不等式的布尔组合定义。 这意味着在 $\mathbf R$ 上量词消去的可行性，也就是说，每个由多项式方程和不等式由逻辑连接词 ∨、∧、¬ 和量词 ∀、∃ 构成的公式可以等于一个不含量词的类似公式。一个重要的结果是实闭域理论的可判定性。尽管定理的原始证明是构造性的，但由此产生的算法的计算复杂度太高了。 George E. Collins 引入了柱形代数分解算法(CAD, cylindrical algebraic decomposition, paper)，该算法允许在双指数时间内对实数进行量词消去。这个复杂性是最佳的，因为有一些例子显示输出具有双指数数量的胞腔¹。因此，该算法是计算代数几何的基本算法。

---

量词消去是指从 Tarski 公式中消除量词，Tarski 公式是多项式方程和不等式的布尔组合。变量 $x_1,..., x_k$ 的Tarski 公式的原子公式的形式为 $f(x_1, ..., x_k)\ \text{s}\ g(x_1, ..., x_k)$，其中 $f$ 和 $g$ 是整系数多项式，$\text{s}$ 是关系运算符 >,<,=,≠,≥,≤ 之一。$\mathbf R^n$中的一个半代数集是由 Tarski 公式定义的集合。投影是指一个映射$π:\mathbf R^{n+1}\to\mathbf R^n$，$(x_1, ...,x_n,x_{n+1})\mapsto(x_1, ...,x_n)$. Tarski-Seidenberg 定理是说: 集合 $X$ 是$\mathbf R^{n+1}$中的一个半代数集 ($n≥1$)，则 $π(X)$ 是$\mathbf R^{n}$中的一个半代数集。

---

代数集是由多项式方程的布尔组合定义的集合。如果将定理中的半代数集替换为代数集则不成立，例如 $\mathbf R^2$ 中的一个代数集 $\{(x,y)|xy=1\}$ 投影到 $\mathbf R$ 上变成了 $\{x|x≠0\}$，它是一个半代数集而不是代数集。

---

我们可以利用软件 tarski 计算 Tarski 公式和半代数集，用 QEPCAD 计算量词消去。 扩展 Tarski 公式(ETF, Extended Tarski Formula)的范围大于简单的 Tarski 公式，它仍然准确地定义了半代数集，但它描述某些集比简单的 Tarski 公式更容易，使 QEPCAD 更有效地计算。 QEPCAD 中输入和输出公式的语言是受限 ETF 语言(Restricted ETF)，它是 ETF 的一个子集，但它仍然是 Tarski 公式语言的超集。这里我们只给出一个非正式的定义。 受限 ETF 语言与 Tarski 公式相比，多了对于称为根索引表达式(indexed root expression)的原子公式的支持。根索引表达式形如$x_k \text{ s root}_jf(x_1, ..., x_k)$，其中 $f$ 是整系数多项式，$j$ 是非零整数，$\rm s$ 是关系运算符 >,<,=,≠,≥,≤ 之一，其真值定义为: 若 $n\lt k$，则该原子公式的真值由 $a_k\text{ s }b$ 给出，其中 $b$ 是 $f(x_1,...,x_{k-1},x_k)$ 的第 $|j|$ 个根，如果 $j\gt0$，则从最小到最大排序，否则从最大到最小排序; 若 $n≥k$，该原子公式在点 $(a_1,...,a_n)$ 处为假，如果多项式 $f(a_1,...,a_{k-1},x_k)$ 的不同实数根少于 $k$ 个。请记住，在 CAD 构造问题中，$x_a < x_2 < ... < x_k$ 的变量有一个假定的顺序。该顺序是此定义的一部分！

---

索引根表达式及其定义的集合的一些示例

[ x2 > _root_1 x1^2 + x2^2 - 1 ]		A simple example in the extended language - the cells colored blue are in the set defined by the formula
[ x2 > _root_-2 (x1^2 + x2^2)^4 - 7 x1^6 x2 + 35 x1^4 x2^3 - 21 x1^2 x2^5 + x2^7 ]		Sometimes the sets defined by indexed root expressions are a bit odd!

---

¹ CAD是将 $\mathbf R^n$ 分成若干连通的半代数集,称为胞腔,使得每个多项式在单个胞腔内的符号恒定,并且满足,对于 $1≤k\lt n$, $π$ 是从 $\mathbf R^n$ 到 $\mathbf R^{n−k}$ 的投影(即删除末尾的 $k$ 个坐标)，那么对于每对单元格 $c$ 和 $d$，要么 $π(c) = π(d)$ 要么 $π( c) ∩ π(d) = ∅$(这意味着胞腔的投影是 $\mathbf R^{n-k}$ 的一个柱形分解)

hbghlyj

Using QEPCAP

prompt% qepcad
=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 0.1, 30 Jul 2002
                                                       
                          by                           
                       Hoon Hong                       
                  (hhong@math.ncsu.edu)                
                                                       
With contributions by: Christopher W. Brown, George E. 
Collins, Mark J. Encarnacion, Jeremy R. Johnson        
Werner Krandick, Richard Liska, Scott McCallum,        
Nicolas Robiduex, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ This is the ever-popular "X Axis Ellipse" problem ]
Enter a variable list:
(a,b,c,x,y)
Enter the number of free variables:
3
Enter a prenex formula:
(A x)(A y)[ a > 0 /\ b > 0 /\ [
  [ b^2 (x - c)^2 + a^2 y^2 - a^2 b^2 = 0] ==>
  x^2 + y^2 - 1 <= 0
] ].

=======================================================

Before Normalization >
finish
An equivalent quantifier-free formula:

a > 0 /\ b > 0 /\ c - a + 1 >= 0 /\ c + a - 1 <= 0 /\ [ 
b^2 - a <= 0 \/ b^2 c^2 + b^4 - a^2 b^2 - b^2 + a^2 <= 0 ]

=======================================================
prompt%
      

Enter an informal description  between '[' and ']':
[Produces a CAD that's not projection definable ]
Enter a variable list:
(x,y)
Enter the number of free variables:
1
Enter a prenex formula:
(Ey)[ x^2 + y^2 - 3 = 0 /\ x + y > 0 ].
=======================================================

Before Normalization >
go

Before Projection (y) >
go

Before Choice >
go

Before Solution >
pdq
CAD is not projection definable.

Before Solution >
solution-extension T
An equivalent quantifier-free formula:

x^2 - 3 <= 0 /\ [ x >= 0 \/ 2 x^2 - 3 < 0 ]

Before Solution >
solution-extension E
An equivalent quantifier-free formula:

x^2 - 3 <= 0 /\ x > _root_1 2 x^2 - 3

      

hbghlyj

A Generic Projection Operator for Partial Cylindrical Algebraic Decomposition

Figure. 2.

X-AXIS Ellipse Problem

Write down conditions such that the ellipse $\frac{(x-c)^{2}}{a^{2}}+\frac{(y-d)^{2}}{b^{2}}-1=0$ is inside the circle $x^{2}+y^{2}-1=0$. We treat the special case $d=0$; compare Figure 2. Our input formula reads as follows:$$\forall x \forall y\left(b^{2}(x-c)^{2}+a^{2} y^{2}-a^{2} b^{2}=0 \longrightarrow x^{2}+y^{2}-1 \leq 0\right)$$ Due to clearing denominators, this description includes de-generate cases of exactly the sort observed by Chou[4] to be inevitable in general The projection order is $\stackrel{y}{\longrightarrow} \stackrel{x}{\longrightarrow} \mid \stackrel{c}{\longrightarrow} \stackrel{b}{\longrightarrow} \stackrel{a}{\longrightarrow}$. With the regular projection operator PROJH, we successively obtain intermediate projection sets of the following sizes$$2→918→28→32\tag{20ms}$$ On the basis of this projection set, regular PCAD succeeds after 1 min with a quantifier-free equivalent containing 4234 atomic formulas. With our generic projection operator GPROJ, we obtain in contrast, the following intermediate projection set sizes:$$9→116→24→24 \tag{10ms}$$In addition, we obtain the following theory$$\{a+b \neq 0, a-b \neq 0, a \neq 0, b \neq 0\}$$On this basis, generic PCAD returns after 7s a quantifier-free formula containing 448 atomic formulas. We next analyze the situation when using GPROJ but admitting only monomial assumptions. Here we obtain the projection set sizes $$2→9→117→25→25\tag{10ms}$$together with the theory$$\Theta=\{a \neq 0, b \neq 0, c \neq 0\}$$On this basis, generic PCAD yields after 8s a quantifier-free formula y with 578 atomic formulas. Note that $a≠0$ and $b≠0$ are obviously non-degeneracy conditions. We finally use $\Theta$ and $\varphi'$ obtained by this last generic PCAD and complete it to a quantifier-free equivalent of the input formula. For this we additionally treat the three cases excluded by $\Theta$. Applying regular PCAD to the original problem with 0 substituted for $a$. we obtain "false" in less than 10 ms The same holds for the case $b=0$. For the case $c=0$ we obtain in 240 ms a quantifier-free equivalent $\varphi_{c}^{\prime}$ with 76 atomic formulas. Combining these results, we have$$\mathbb{R} \models\left(\left(\bigwedge \Theta \wedge \varphi^{\prime}\right) \vee\left(c=0 \wedge \varphi_{c}^{\prime}\right)\right) \longleftrightarrow \varphi$$Our quantifier-free formula obtained by one generic PCAD plus three regular PCAD's on special cases contains 3+578+1+76=658 atomic formulas. It requires an overall com-putation time of less than 9 s. This is a considerable improvement compared to the straightforward PCAD with 4234 atomic formulas in 1 min.

hbghlyj

paper

Figure 9. Collision Problem

In this section we illustrate our algorithm by a simple collision problem from robot motion planning.
Consider two semi-algebraic objects: a circle and a square (See Fig 9). The circle has diameter 2 and is initially centered at $(0,0)$ and is moving with the velocity $v_x=1$ and $v_y=0$. The square has side-length 2 and is initially centered at $(0,-8)$ and is moving with the velocity $v_x=17/16$ and $v_y=17/16$. Now we want to decide if these two objects would collide.
The moving circle can be described algebraically as:$$(x-t)^{2}+y^{2} \leq 1$$The moving square can be described algebraically as:$$-1 \leq x-\frac{17}{16} t \leq 1 \quad \wedge \quad-9 \leq y-\frac{17}{16} t \leq-7$$From these we can express the collision problem as a decision problem of a sentence in elementary algebra and geometry:\begin{align*}(\exists t)(\exists x)(\exists y)(\qquad &t>0 \\ \wedge\quad &x-\frac{17}{16} t \geq-1 \\  \wedge \quad &x-\frac{17}{16} t \leq 1 \\  \wedge \quad &y-\frac{17}{16} t \geq-9 \\\wedge \quad &y-\frac{17}{16} t \leq-7 \\ \wedge \quad&(x-t)^{2}+y^{2} \leq 1)\end{align*}We can refine this sentence by observing that collision can occur only when the topside of the square is above or on the line $y=-1$ and the bottom side of the square is below or on the line $y=1$. Translating this observation into a restriction on the range of $t$, we get the following sentence:\begin{align*}(\exists t)(\exists x)(\exists y)(\quad& \frac{17}{16} t \geq 6 \\ \wedge& \frac{17}{16} t \leq 10 \\ \wedge &x-\frac{17}{16} t \geq-1 \\ \wedge &x-\frac{17}{16} t \leq 1 \\ \wedge& y-\frac{17}{16} t \geq-9 \\ \wedge &y-\frac{17}{16} t \leq-7 \\ \wedge&(x-t)^{2}+y^{2} \leq 1) \end{align*}We entered this sentence into an implementation(Arnon 1981)of the original CAD algorithm, and it reported collision, after constructing 25 cells in 1-space, 263 cells in2-space, and 1795 cells in 3-space, taking 1 hour and 44 minutes on a Sun3/50 runningUnix.
We tried our partial CAD algorithm on the same sentence using the cell choice strategy HL-LI. It reported collision, after constructing 25 cells in 1-space, 11 cells in 2-space, and 25 cells in 3-space, taking 20.5 seconds (7.8 seconds for projection, 12.7 seconds for stackconstruction.
Below we present the trace of the actual computation carried out by the partial CADsystem. In order to save space the trace output has been compressed. In this trace, apartial CAD is represented as a tree of cells, where each cell is represented by its cell-index along with one character indicating its truth value(T, F, respectively for true,false, undetermined The text in italics consists of comments inserted afterwards
Enter a prenex formula:
(Et)(Ex)(Ey)(17/16t>=6
&17/16t<=10
&x-17/16t>=-1
&x-17/16t<=1
&y-17/16t>=-9
&y-17/16t<=-7
&y^2+x^2-2tx+t^2<=1)

hbghlyj

tarski

Example

~/$ tarski
> (def F1 [ y > -x (x - 1) /\ (x - 1/3)^2 + y^2 < (1/2)^2 ])   ; define F1 as a formula
:void
> (def R1 (SAT-NuCADConjunction F1))                           ; determine (open) satisfiability of F1
:void
> (head R1)
( ( x:sym y:sym ) ( 0:num 1/8:num ) )
> (def F2 [ y > -x (x - 1) /\ (x - 1/3)^2 + y^2 < (1/8)^2 ])   ; define F2 as a formula
:void
> (def R2 (SAT-NuCADConjunction F2))                           ; determine (open) satisfiability of F2
:void
> (head R2)
false:boo
> (def F [ y > -x (x - 1) /\ (x - c)^2 + y^2 < r^2 /\ r > 0 ]) ; F generalizes with parameters
:void
> (def D (make-NuCADConjunction '(c r x y) '(0 0 0 0) F))      ; construct an open NuCAD for F
:void
> (msg D 'project 2)                                           ; project onto (c,r)-space
:void
> (msg D 'plot-leaves "-1 1 -1 1 500 500" "C" "/tmp/foo.svg")  ; produce a plot
:void
> (msg D 'negate)                                              ; swap true/false labels on the cells of D
:void
> (msg D 'def-form)                                            ; get a defining formula for D
"[ [ r < _root_1 r ] \/ [ r > _root_1 r /\ r < _root_2 16 r^6 - 48 c^2 r^4 + 48 c r^4 - 13 r^4 
+ 48 c^4 r^2 - 96 c^3 r^2 + 92 c^2 r^2 - 44 c r^2 + 8 r^2 - 16 c^6 + 48 c^5 - 52 c^4 + 24 c^3 - 4 c^2  
/\ c > _root_1 c /\ c < _root_1 2 c - 1 ] \/ [ r > _root_1 r /\ r < _root_2 16 r^6 
- 48 c^2 r^4 + 48 c r^4 - 13 r^4 + 48 c^4 r^2 - 96 c^3 r^2 + 92 c^2 r^2 - 44 c r^2 + 8 r^2 - 16 c^6 
+ 48 c^5 - 52 c^4 + 24 c^3 - 4 c^2  /\ c > _root_1 2 c - 1 /\ c < _root_1 c - 1 ] ]":str
> (quit)
~/$	
      

hbghlyj

1 October 2021- Web version of Tarski
这个页面上的框就是Tarski的Web版本.无需安装任何软件,在浏览器中即可使用Tarski.