실존론

수학적 논리학, 계산적 복잡성 이론, 컴퓨터 과학에서 실존적 이론은 형식의 모든 참된 문장의 집합이다.

${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),\,}$

여기서 $F{\displaystyle (}$ ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$,${\displaystyle }$… ${\displaystyle X_{}}$ n${\displaystyle {}_{}}$) ${\displaystyle F(X_{1},\dots X_{n}})$는 실제 다항식의 동일성과 불평등을 포함하는 계량자 없는 공식이다.^[1]

실존적 이론의 결정 문제는 그러한 공식 각각에 대해 그것이 참인지 거짓인지를 결정하는 알고리즘을 찾는 문제다.마찬가지로, 주어진 반제곱 집합이 비어 있지 않은지 여부를 검정하는 것이 문제다.^[1]이 결정 문제는 NP-hard이며 PSpace에 있다.^[2]따라서 실존적 정량자에 대한 제약 없이 실존적 정량자의 1차 이론에서 진술을 결정하는 알프레드 타르스키의 정량화 제거 절차보다 복잡성이 현저히 낮다.^[1]그러나 실제로 1차 이론에 대한 일반적인 방법은 이러한 문제들을 해결하기 위한 선호되는 선택으로 남아 있다.^[3]

기하학적 그래프 이론의 많은 자연적인 문제들, 특히 기하학적 교차 그래프를 인식하고 교차하는 것으로 그래프 도면의 가장자리를 일직선으로 하는 문제들은 실존적 이론의 사례로 번역함으로써 해결될 수 있으며, 이 이론에 대해서는 완전하다.NP와 PSPACE 사이에 있는 복잡도 등급 $\exists {\displaystyle \mathrm{}}$ ${\displaystyle R\mathbb{}}$ ${\$ $\}$은(는) 이 등급의 문제를 설명하기 위해 정의되었다.^[4]

배경

수학 논리학에서 이론은 고정된 기호 집합을 사용하여 쓴 문장 집합으로 구성된 형식 언어다.실제 폐쇄장의 1차 이론에는 다음과 같은 기호가 있다.^[5]

• 0과 1의 상수
• ${\displaystyle {변수}_{}}$ X i ${\$
• 추가, 빼기, 곱하기, 그리고 (계속) 분할 작업,
• 기호 <, ≤, =, ≥, > 및 ≠은 실제 값 비교를 위한 것이다.
• 논리 결합체 ∧, ∨, ¬, ⇔, ⇔,
• 괄호, 그리고
• 만능정량기 ∀과 실존정량기 ∃

이들 기호의 순서는 문법적으로 잘 형성되어 있고, 그 모든 변수가 적절히 정량화 되어 있으며, (실수에 대한 수학적 진술로 해석될 때) 실수의 제1차 이론에 속하는 문장을 형성한다.타르스키가 보여주었듯이, 이 이론은 공리 스키마와 완전하고 효과적인 결정 절차에 의해 설명될 수 있다: 모든 완전 정량화된 문장과 문법적인 문장에 대해 문장이나 그 부정(두 가지 모두 그렇지는 않지만)은 공리로부터 파생될 수 있다.같은 이론은 실제 숫자뿐만 아니라 모든 실제 폐쇄된 분야를 설명한다.^[6]그러나 이러한 공리에 의해 정확하게 기술되지 않는 다른 수 체계도 있다.특히 마티야세비치의 정리에 의한 실존적 문장(다이오판타인 방정식)에도 불구하고 실수 대신 정수에 대해 같은 방법으로 정의한 이론은 불가해하다.^[5][7]

실존 이론은 모든 정량자가 실존하며 다른 어떤 기호보다 먼저 나타나는 문장으로 구성된 1차 이론의 부분집합이다.즉, 양식의 모든 참된 문장의 집합이다.

${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),\,}$

여기서 $F{\displaystyle (}$ ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$,${\displaystyle }$… ${\displaystyle X_{}}$ n${\displaystyle {}_{}}$) ${\displaystyle F(X_{1},\dots X_{n}})$는 실제 다항식의 동일성과 불평등을 포함하는 계량자 없는 공식이다.실존이론의 결정문제는 주어진 문장이 이 이론에 속하는지 여부를 시험하는 알고리즘적인 문제로서, 동등하게, 기본적인 구문적 검사를 통과한 문자열(정확한 구문을 가진 올바른 기호를 사용하고, 정량화되지 않은 변수를 가지고 있지 않음)에 대해서는 송신된 것이 시험의 문제다.실제 숫자에 대한 진실된 진술이다.The set of n-tuples of real numbers ${\displaystyle (X_{1},\dots X_{n})}$ for which ${\displaystyle F(X_{1},\dots X_{n})}$ is true is called a semialgebraic set, so the decision problem for the existential theory of the reals can equivalently be rephrased as testing whether a given semi대수 집합은 비어 있지 않다.^[1]

실존적 이론에 대한 의사결정 문제에 대한 알고리즘의 시간 복잡성을 결정하는데 있어서, 입력의 크기에 대한 측도를 갖는 것이 중요하다.이러한 유형의 가장 간단한 척도는 문장의 길이, 즉 문장에 포함된 기호의 수입니다.^[5]그러나 이 문제에 대한 알고리즘의 동작에 대한 보다 정밀한 분석을 달성하기 위해서는 입력 크기를 정량화할 변수의 수, 문장 내의 다항식의 수, 이러한 다항식의 정도를 구분하여 여러 변수로 분해하는 것이 편리하다.^[8]

예

황금 비율 $\phi {\displaystyle }$ ${\displaystyle \varphi }$은(는) 다항식 x ${\displaystyle {2\mathrm{}}^{}}$- ${\displaystyle \mathrm{x}}$ -${\displaystyle }$1 ${\displaystyle x^{2}-x-1}$의 루트로 정의할 수 있다$$$.$이 다항식은 두 개의 뿌리를 가지고 있는데, 그 중 한 가지(황금비)만이 한 가지보다 크다.따라서 황금비율의 존재는 문장으로 표현될 수 있다.

${\displaystyle \exists X_{1}(X_{1})1\wedge X_{1}\time X_{1}-X_{1}-1=0).}$

황금비율이 존재하기 때문에 이것은 참된 문장이며 실존자의 실존 이론에 속한다.실존적 이론의 결정 문제에 대한 답은 이 문장을 입력으로 보아 부울 값 참이다.

산술과 기하학의 불평등은 두 개의 비음수 $x{\displaystyle }$ ${\displaystyle$ x$}$과 $y{\displaystyle }$ ${\displaystyle$ y$}$에$$대해 다음과 같은 불평등이 유지된다는 것을 의미한다.

${\displaystyle {\frac {x+y}{2}}}}\geq {\sqrt {xy}.}$

위에서 말한 바와 같이 실수에 관한 1차적 문장이지만 실존적 정량자가 아닌 보편적 정량자가 있는 문장이며, 실존자의 1차적 이론에서는 허용되지 않는 분단, 제곱근, 숫자 2에 대해 여분의 기호를 사용하는 문장이다.그러나 양쪽을 모두 제곱함으로써 불평등이 백배수를 가지고 있는지를 묻는 것으로 해석할 수 있는 다음과 같은 실존적 진술로 변형될 수 있다.

${\displaystyle \exists X_{1}\exists X_{2}{\bigl (}X_{1}\geq 0\wedge X_{2}\geq 0\wedge (X_{1}+X_{2})\times (X_{1}+X_{2})<(X_{1}+X_{1})\times (X_{2}+X_{2}){\bigr )}.}$

실존적 이론의 결정 문제에 대한 답은, 이 문장을 입력으로 간주하면, 부울 값 거짓이다: 백작샘플은 없다.그러므로 이 문장은 올바른 문법적 형식을 갖추고 있음에도 불구하고 실존적 실존적 이론에 속하지 않는다.

알고리즘

알프레드 타르스키의 정량화 제거 방법(1948)은 실존적 이론(그리고 보다 일반적으로 실존적 이론)이 알고리즘적으로 해결 가능하지만, 그 복잡성에 대한 기본적인 구속이 없는 것을 보여주었다.^[9][6]원통형 대수분해법은 조지 E. 콜린스(1975)에 의해 시간 의존도가 두 배로 기하급수적으로 향상되었다.^[9][10]

${\displaystyle L^{3}(md)^{2^{O(n)}}}$

여기서 $L{\displaystyle }$ ${\displaystyle L}$은(는) 문장의 계수를 나타내는 데 필요한 비트 수, m ${\displaystyle m}$은 문장의 다항식 수, $d{\displaystyle }$ ${\displaystyle d}$은 전체 도, n ${\displaystyle n}$은 변수의 수입니다.^[8]1988년까지, Dima Grioriev와 Nicolai Vorobjov는 복잡성이 $n{\displaystyle }$ ${\displaystyle n}$의 다항식에서 기하급수적으로 나타나는 것을 보여주었다$.$^[8][11][12]

${\displaystyle L(md)^{n^{2}}$

1992년에 발표된 일련의 논문에서 제임스 르네거는 $이것$을 n ${\displaystyle n}$에 대한 단일 지수 의존으로 개선했다$.$^{[8][13][14][15]}

${\displaystyle L\log L\log \log L(md)^{O(n)}}$

한편 1988년 존 캐니는 시간 의존도가 기하급수적인 또 다른 알고리즘을 설명했지만 다항식 공간 복잡성만 가지고 있다. 즉, 그는 이 문제가 PSpace에서 해결될 수 있다는 것을 보여주었다.^[2][9]

실제로 매우 작은 크기의 입력에서만 실행할 수 있기 때문에 이러한 알고리즘의 점증적 계산 복잡성은 오해의 소지가 있다.1991년 비교에서 훈 홍은 콜린스의 이중 지수적 절차가 위의 모든 파라미터를 1초도 안 되는 2로 설정함으로써 그 크기를 설명하는 문제를 해결할 수 있을 것이라고 추정했지만, 그 대신 그리고리예프, 보르브조프, 르네가르의 알고리즘은 100만년 이상이 걸릴 것이다.^[8]1993년 주스, 로이, 솔레노 등은 이론상으로는 물론 원통형 대수적 결정보다 실제적으로 더 빠르게 하기 위해 지수적 시간 절차에 대한 작은 수정이 가능해야 한다고 제안했다.^[16]그러나 2009년을 기점으로 실재자의 실존 이론에 특화된 단일 지수 알고리즘에 비해 실재자의 1차 이론에 대한 일반적인 방법들이 실제적으로 우위에 있는 것은 여전히 사례였다.^[3]

완전한 문제

계산 복잡성과 기하학적 그래프 이론의 몇 가지 문제들은 실존적 이론에 대해 완전한 것으로 분류될 수 있다.즉 실존론상의 모든 문제는 다항 시간 다수를 이 문제들 중 하나의 예로 축소하고, 나아가 실존론까지 환원할 수 있는 것이다.^[4][17]

이러한 유형의 여러 문제점은 특정 유형의 교차로 그래프를 인식하는 것과 관련이 있다.이러한 문제에서 입력은 방향성이 없는 그래프입니다. 목표는 특정 등급의 도형의 기하학적 모양이 그래프에서 두 꼭지점이 인접한 방식으로 그래프의 정점과 연관될 수 있는지 여부를 결정하는 것이다.실재의 실존이론에 대해 완성되는 이 유형의 문제에는 평면 내 선 세그먼트의 교차 그래프 인식,^[4][18][5] 단위 디스크 그래프의 인식,^[19] 평면 내 볼록 집합의 교차 그래프 인식 등이 있다.^[4]

교차 없이 평면에 그려진 그래프의 경우, 파리의 정리는 그래프의 가장자리가 직선 세그먼트로 그려지는지 임의 곡선으로 그려지는지에 관계없이 동일한 등급의 평면 그래프를 얻는다고 명시한다.그러나 이 등가성은 다른 유형의 도면에는 해당되지 않는다.예를 들어, 그래프의 교차 수(임의적으로 곡선이 있는 도면의 교차 최소 수)는 NP로 결정할 수 있지만, 실체들의 실존 이론은 직선 교차 수(edg의 최소 쌍 수)에 대해 주어진 경계를 달성하는 도면이 존재하는지 여부를 판단하는 것이 완성된다.es 평면에서 직선 세그먼트로 그려진 가장자리가 있는 모든 도면에서 교차하는 것).^[4][20]또한 실재자의 실존적 이론은 주어진 그래프를 직선 가장자리와 주어진 에지 쌍을 교차로서 평면에 그릴 수 있는지, 또는 동등하게 교차점이 있는 곡선 도면을 그 교차점을 보존하는 방식으로 바로 잡을 수 있는지를 시험하는 것이 완성된다.^[21]

실존적 이론의 다른 완전한 문제들은 다음과 같다.

• 주어진 다각형의 모든 점이 보이는 가장 적은 수의 점을 찾는 미술관 ^[22]문제
• 주어진 다각형 세트가 주어진 사각형 용기에 들어갈 수 있는지 여부를 결정하는 ^[23]포장 문제
• 단위 거리 그래프의 인식 및 그래프의 치수 또는 유클리드 치수가 최대 주어진 값인지 시험한다.^[9]
• 가성체의 신축성(즉, 평면의 곡선 계열을 주어진 후 선 배열에 대해 동형인지 여부를 결정하는 것)^[4][24][25]
• 고정 치수 >2에서 기하학적 양자 논리의 약한 만족도 및 강한 만족도 모두.^[26]
• 모호하지 않은 오토마타에 대한 모델 확인 간격 Markov 체인.^[27]
• 4차원 폴리토페로 제한된 경우에도 알고리즘 스타이니츠 문제(격자를 주어 볼록 폴리토페의 얼굴 격자인지 여부를 판단한다).^[28][29]
• 특정 볼록한 신체의^[30] 배치 공간 실현
• 멀티플레이어 게임의^[31][32][33] 나시 평형성의 다양한 특성
• 주어진 추상적인 삼각망과 사변측정감시 복합체를 3차원 유클리드 공간에 내장.^[17]
• 모든 그래프를 교차 없이 그릴 수 있도록 평면에 설정된 공유 정점에 여러 개의 그래프를 포함.^[17]
• 평면 점 집합의 가시성 그래프 ^[17]인식
• (^[34]프로젝트적 또는 비프로젝트적 조건) 교차 제품에 대한 두 용어 사이의 방정식의 만족도
• 평면 그래프의 비경사 도면의 최소 기울기 번호 ^[35]결정
• 모든 교차점을 직각으로 그릴 수 있는 그래프 ^[36]인식
• MATLANG+ 고유 행렬 쿼리 언어의 부분 평가 문제.^[37]
• 하위 행렬 완료 ^[38]문제

이를 바탕으로 복잡도 등급 $\exists {\displaystyle \mathrm{}}$ ${\displaystyle R\mathbb{}}$ ${\$은(는) 다항식 시간 다수를 실제의 실존 이론으로 축소하는 문제의 집합으로 정의되었다$$.^[4]

참고 항목

• 힐버트의 열 번째 문제, 정수들의 (결정할 수 없는) 실존 이론에 관한 것이다.

참조