고정점 논리

수리 논리학에서 **고정점 논리**()는 재귀를 표현하기 위해 도입된 고전 술어 논리의 확장이다. 고정점 논리의 발전은 기술 복잡도 이론과 데이터베이스 질의어, 특히 Datalog와의 관계에 의해 촉진되었다.

최소 고정점 논리는 1974년 이안니스 N. 모스호바키스에 의해 처음으로 체계적으로 연구되었고, 앨프리드 에이호와 제프리 울먼이 고정점 논리를 표현적인 데이터베이스 질의어로 제안한 1979년에 컴퓨터 과학자들에게 소개되었다.

## 부분 고정점 논리
관계적 기호 X에 대해, FO[PFP](X)는 1차 연결사 및 술어, 2차 변수 그리고 [\operatorname{PFP}_{\vec{x},P} \varphi]\vec{t} 형식의 공식을 형성하는 데 사용되는 부분 고정점 연산자 \operatorname{PFP}를 사용하여 X로부터 형성된 공식들의 집합이다. 여기서 P는 2차 변수이고, \vec{x}는 1차 변수들의 튜플이며, \vec{t}는 항들의 튜플이고, \vec{x}와 \vec{t}의 길이는 P의 항수와 일치한다.

를 정수라 하고, x, y를  변수들의 벡터라 하고, 를 항수 의 2차 변수라 하고, 를 와 를 변수로 사용하는 FO(PFP,X) 함수라고 하자. 우리는 (P_i)_{i\in N}를 P_0(x)=false 및 P_i(x)=\varphi(P_{i-1},x) (즉, 2차 변수  대신 P_{i-1}을 대입한 )가 되도록 반복적으로 정의할 수 있다. 그러면 고정점이 있거나, (P_i)들의 목록이 순환적이다.

[\operatorname{PFP}_{P,x} \varphi (y)]는 고정점이 있다면 에 대한 (P_i)의 고정점 값으로 정의되고, 그렇지 않다면 거짓으로 정의된다. 는 항수 의 속성이므로, P_i에 대한 값은 최대 2^{n^k}개가 존재하므로, 다항 공간 카운터를 사용하면 루프가 있는지 없는지 확인할 수 있다.

정렬된 유한 구조에서, FO(PFP,X)로 표현할 수 있는 속성은 PSPACE에 속하는 속성이라는 것이 증명되었다.

## 최소 고정점 논리
부분 고정점 계산에 포함된 반복 술어는 일반적으로 단조적이지 않으므로, 고정점이 항상 존재하지 않을 수도 있다.
최소 고정점 논리 FO(LFP,X)는 부분 고정점이 의 양의 발생 (즉, 짝수 개의 부정에 선행된 발생)만 포함하는 공식 에 대해서만 취해지는 FO(PFP,X)의 공식 집합이다. 이는 고정점 구성의 단조성을 보장한다 (즉, 2차 변수가 이면 P_i(x)는 항상 P_{i+1}(x)를 의미한다).

단조성 때문에, 우리는 의 진리표에 벡터를 추가하기만 하며, 가능한 벡터가 n^k개밖에 없으므로 n^k 반복 전에 항상 고정점을 찾을 것이다. 닐 이머만과 모셰 바르디가 독립적으로 보인 이머만-바르디 정리는 FO(LFP,X)가 모든 정렬된 구조에서 P를 특징짓는다는 것을 보여준다.

최소 고정점 논리의 표현성은 데이터베이스 질의 언어인 Datalog의 표현성과 정확히 일치하며, 정렬된 구조에서 Datalog가 다항 시간 안에 실행 가능한 질의를 정확히 표현할 수 있음을 보여준다.

## 팽창 고정점 논리
고정점 구성의 단조성을 보장하는 또 다른 방법은 반복의 모든 단계에서 새 튜플을 P에 추가하고, 더 이상 P가 유지되지 않는 튜플을 제거하지 않는 것이다. 공식적으로, 우리는 \operatorname{IFP}(\phi_{P,x})를 \psi(P,x)=\phi(P,x)\vee P(x)인 \operatorname{PFP}(\psi_{P,x})로 정의한다.

이 팽창 고정점은 후자가 정의되는 곳에서 최소 고정점과 일치한다. 처음에는 팽창 고정점 논리가 더 넓은 범위의 고정점 인수를 지원하므로 최소 고정점 논리보다 더 표현력이 풍부해야 하는 것처럼 보이지만, 사실 모든 FO[IFP](X)-공식은 FO[LFP](X)-공식과 동등하다.

## 동시 귀납
지금까지 도입된 모든 고정점 연산자는 단일 술어의 정의에 대해서만 반복했지만, 많은 컴퓨터 프로그램은 여러 술어에 대해 동시에 반복하는 것으로 더 자연스럽게 생각된다. 고정점 연산자의 항수를 늘리거나 중첩함으로써, 모든 동시 최소, 팽창 또는 부분 고정점은 사실 위에서 논의된 해당 단일 반복 구성을 사용하여 표현될 수 있다.

## 전이 폐포 논리
임의의 술어에 대한 귀납을 허용하는 대신, 전이 폐포 논리는 전이 폐포만 직접 표현할 수 있도록 한다.

FO[TC](X)는 1차 연결사 및 술어, 2차 변수, 그리고 [\operatorname{TC}_{\vec{x},\vec{y}} \varphi]\vec{s}\vec{t} 형식의 공식을 형성하는 데 사용되는 전이 폐포 연산자 \operatorname{TC}를 사용하여 X로부터 형성된 공식들의 집합이다. 여기서 \vec{x}와 \vec{y}는 쌍으로 구별되는 1차 변수들의 튜플이고, \vec{t}와 \vec{s}는 항들의 튜플이며, \vec{x}, \vec{y}, \vec{s}, \vec{t}의 길이는 일치한다.

TC는 다음과 같이 정의된다: 를 양의 정수라 하고, u,v,x,y를  변수들의 벡터라 하자. 그러면 개의 변수 벡터 (z_i)가 존재하여 z_1=x, z_n=y이고, 모든 i에 대해 \phi(z_i,z_{i+1})이 참이면 \mathsf{TC}(\phi_{u,v})(x,y)는 참이다. 여기서 는 FO(TC)로 작성된 공식이며, \phi(x,y)는 변수 와 가 와 로 대체됨을 의미한다.

정렬된 구조에서, FO[TC]는 복잡도 클래스 NL을 특징짓는다. 이 특징화는 NL이 보수 하에서 닫혀 있다는 이머만 증명(NL = co-NL)의 중요한 부분이다.

## 결정적 전이 폐포 논리
FO[DTC](X)는 전이 폐포 연산자가 결정적인 FO(TC,X)로 정의된다. 이는 \operatorname{DTC}(\phi_{u,v})를 적용할 때, 모든 에 대해 \phi(u,v)가 참이 되는 가 최대 하나만 존재한다는 것을 의미한다.

우리는 \operatorname{DTC}(\phi_{u,v})가 \psi(u,v)=\phi(u,v)\wedge \forall x (x=v \vee \neg \phi(u,x))인 \operatorname{TC}(\psi_{u,v})의 신택틱 슈거라고 가정할 수 있다.

정렬된 구조에서, FO[DTC]는 복잡도 클래스 L을 특징짓는다.

## 반복
지금까지 정의한 고정점 연산은 고정점에 도달할 때까지 공식에 언급된 술어의 귀납적 정의를 무한정 반복한다. 구현 시에는 계산 시간을 제한하기 위해 반복 횟수를 제한해야 할 수도 있다. 결과로 나오는 연산자는 복잡도 클래스를 특징짓는 데 사용될 수 있으므로 이론적 관점에서도 흥미롭다.

우리는 반복을 포함하는 1차 논리 \mathsf{FO}[t(n)]를 정의할 것이다. 여기서 t(n)은 정수에서 정수로의 함수 (또는 함수들의 클래스)이며, t(n)의 다른 함수 클래스에 대해 다른 복잡도 클래스 \mathsf{FO}[t(n)]를 얻을 것이다.

이 섹션에서 (\forall x P) Q는 (\forall x (P\Rightarrow Q))를 의미하고 (\exists x P) Q는 (\exists x (P \wedge Q))를 의미한다. 우리는 먼저 양화자 블록(QB)을 정의해야 한다. 양화자 블록은 (Q_1 x_1, \phi_1)...(Q_k x_k, \phi_k)와 같은 목록으로, \phi_i는 양화자 없는 FO-공식이고 Q_i는 \forall 또는 \exists이다. 만약 가 양화자 블록이라면 우리는 [Q]^{t(n)}을 반복 연산자라고 부를 것이며, 이는 를 t(n)번 반복하여 작성한 것으로 정의된다. 여기에는 목록에 k*t(n)개의 양화자가 있지만, 변수는 개뿐이며 각 변수는 t(n)번 사용된다는 점에 주의해야 한다.

이제 \mathsf{FO}[t(n)]을 지수가 t(n) 클래스에 속하는 반복 연산자를 가진 FO-공식으로 정의할 수 있으며, 다음 등식을 얻는다.

* \mathsf{FO}[(\log n)^i]는 FO-균일 AC<sup>i</sup>와 같으며, 사실 \mathsf{FO}[t(n)]은 깊이 t(n)의 FO-균일 AC이다.
* \mathsf{FO}[(\log n)^{O(1)}]는 NC와 같다.
* \mathsf{FO}[n^{O(1)}]는 PTIME과 같다. 이는 FO(IFP)를 작성하는 또 다른 방법이기도 하다.
* \mathsf{FO}[2^{n^{O(1)}}]는 PSPACE와 같다. 이는 FO(PFP)를 작성하는 또 다른 방법이기도 하다.

## 내용주

## 각주
* 
* 

분류:데이터베이스 이론
분류:술어 논리