고정점 논리

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

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

부분 고정점 논리

관계적 기호 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$ 의 항수와 일치한다.

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

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

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

최소 고정점 논리

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

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

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

팽창 고정점 논리

고정점 구성의 단조성을 보장하는 또 다른 방법은 반복의 모든 단계에서 새 튜플을 $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)-공식과 동등하다.^[10]

동시 귀납

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

전이 폐포 논리

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

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

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

결정적 전이 폐포 논리

FO[DTC](X)는 전이 폐포 연산자가 결정적인 FO(TC,X)로 정의된다. 이는 $\operatorname {DTC} (\phi _{u,v})$ 를 적용할 때, 모든 $u$ 에 대해 $\phi (u,v)$ 가 참이 되는 $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을 특징짓는다.^[12]

반복

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

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

이 섹션에서 $(\forall xP)Q$ 는 $(\forall x(P\Rightarrow Q))$ 를 의미하고 $(\exists xP)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$ 가 양화자 블록이라면 우리는 $[Q]^{t(n)}$ 을 반복 연산자라고 부를 것이며, 이는 $Q$ 를 $t(n)$ 번 반복하여 작성한 것으로 정의된다. 여기에는 목록에 $k*t(n)$ 개의 양화자가 있지만, 변수는 $k$ 개뿐이며 각 변수는 $t(n)$ 번 사용된다는 점에 주의해야 한다.^[14]

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

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

내용주

↑ Moschovakis, Yiannis N. (1974). 《Elementary Induction on Abstract Structures》. 《Studies in Logic and the Foundations of Mathematics》 77. doi:10.1016/s0049-237x(08)x7092-2. ISBN 9780444105370. ISSN 0049-237X.
↑ Aho, Alfred V.; Ullman, Jeffrey D. (1979). 〈Universality of data retrieval languages〉. 《Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '79》. New York, New York, USA: ACM Press. 110–119쪽. doi:10.1145/567752.567763. S2CID 3242505.
↑ Ebbinghaus and Flum, p. 121
↑ Ebbinghaus and Flum, p. 121
↑ Immerman 1999, p. 161
↑ Abiteboul, S.; Vianu, V. (1989). 〈Fixpoint extensions of first-order logic and datalog-like languages〉. 《[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science》. IEEE Comput. Soc. Press. 71–79쪽. doi:10.1109/lics.1989.39160. ISBN 0-8186-1954-6. S2CID 206437693.
↑ Immerman, Neil (1986). 《Relational queries computable in polynomial time》 (영어). 《Information and Control》 68. 86–104쪽. doi:10.1016/s0019-9958(86)80029-8.
↑ Vardi, Moshe Y. (1982). 〈The complexity of relational query languages (Extended Abstract)〉. 《Proceedings of the fourteenth annual ACM symposium on Theory of computing - STOC '82》. New York, NY, USA: ACM. 137–146쪽. CiteSeerX 10.1.1.331.6045. doi:10.1145/800070.802186. ISBN 978-0897910705. S2CID 7869248.
↑ Ebbinghaus and Flum, p. 242
↑ Yuri Gurevich and Saharon Shelah, Fixed-pointed extension of first order logic, Annals of Pure and Applied Logic 32 (1986) 265--280.
↑ Ebbinghaus and Flum, pp. 179, 193
↑ ^가 ^나 Immerman, Neil (1983). 〈Languages which capture complexity classes〉. 《Proceedings of the fifteenth annual ACM symposium on Theory of computing - STOC '83》. New York, New York, USA: ACM Press. 347–354쪽. doi:10.1145/800061.808765. ISBN 0897910990. S2CID 7503265.
↑ Immerman, Neil (1988). 《Nondeterministic Space is Closed under Complementation》. 《SIAM Journal on Computing》 17. 935–938쪽. doi:10.1137/0217058. ISSN 0097-5397.
↑ Immerman 1999, p. 63
↑ Immerman 1999, p. 82
↑ Immerman 1999, p. 84
↑ Immerman 1999, p. 58
↑ Immerman 1999, p. 161

각주

Ebbinghaus, Heinz-Dieter; Flum, Jörg (1999). 《Finite Model Theory》 2판. Perspectives in Mathematical Logic. Springer. doi:10.1007/978-3-662-03182-7. ISBN 978-3-662-03184-1.
Neil, Immerman (1999). 《Descriptive complexity》. Springer. ISBN 0-387-98600-6. OCLC 901297152.

[1] Moschovakis, Yiannis N. (1974). 《Elementary Induction on Abstract Structures》. 《Studies in Logic and the Foundations of Mathematics》 77. doi:10.1016/s0049-237x(08)x7092-2. ISBN 9780444105370. ISSN 0049-237X.

[2] Aho, Alfred V.; Ullman, Jeffrey D. (1979). 〈Universality of data retrieval languages〉. 《Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '79》. New York, New York, USA: ACM Press. 110–119쪽. doi:10.1145/567752.567763. S2CID 3242505.

[3] Ebbinghaus and Flum, p. 121

[4] Ebbinghaus and Flum, p. 121

[5] Immerman 1999, p. 161

[6] Abiteboul, S.; Vianu, V. (1989). 〈Fixpoint extensions of first-order logic and datalog-like languages〉. 《[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science》. IEEE Comput. Soc. Press. 71–79쪽. doi:10.1109/lics.1989.39160. ISBN 0-8186-1954-6. S2CID 206437693.

[7] Immerman, Neil (1986). 《Relational queries computable in polynomial time》 (영어). 《Information and Control》 68. 86–104쪽. doi:10.1016/s0019-9958(86)80029-8.

[8] Vardi, Moshe Y. (1982). 〈The complexity of relational query languages (Extended Abstract)〉. 《Proceedings of the fourteenth annual ACM symposium on Theory of computing - STOC '82》. New York, NY, USA: ACM. 137–146쪽. CiteSeerX 10.1.1.331.6045. doi:10.1145/800070.802186. ISBN 978-0897910705. S2CID 7869248.

[9] Ebbinghaus and Flum, p. 242

[10] Yuri Gurevich and Saharon Shelah, Fixed-pointed extension of first order logic, Annals of Pure and Applied Logic 32 (1986) 265--280.

[11] Ebbinghaus and Flum, pp. 179, 193

[:0-12] 가 ^나 Immerman, Neil (1983). 〈Languages which capture complexity classes〉. 《Proceedings of the fifteenth annual ACM symposium on Theory of computing - STOC '83》. New York, New York, USA: ACM Press. 347–354쪽. doi:10.1145/800061.808765. ISBN 0897910990. S2CID 7503265.

[13] Immerman, Neil (1988). 《Nondeterministic Space is Closed under Complementation》. 《SIAM Journal on Computing》 17. 935–938쪽. doi:10.1137/0217058. ISSN 0097-5397.

[14] Immerman 1999, p. 63

[15] Immerman 1999, p. 82

[16] Immerman 1999, p. 84

[17] Immerman 1999, p. 58

[18] Immerman 1999, p. 161

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

v t e 수리논리학
일반	형식 언어 Formation rule 형식 체계 형식 증명 형식 의미론 논리식 집합 원소 모임 고전 논리 공리 자연 연역 추론 규칙 관계 정리 논리적 결과 공리계 유형 이론 논리기호 통사 Theory
명사논리학	명제 추론 논증 타당성 Cogency 삼단논법 대당관계 벤 다이어그램
명제 논리 불 논리	불 함수 명제 논리 규범논리 논리 연산 진리표
술어 논리	1차 논리 양화 술어 2차 논리 Monadic predicate calculus
소박한 집합론	집합 공집합 원소 열거 외연성 무한 집합 부분집합 멱집합 가산 집합 비가산 집합 재귀 집합 정의역 공역 상 사상 함수 이항연산 순서쌍
집합론	수학기초론 체르멜로-프렝켈 집합론 선택 공리 General set theory 크립키-플레이텍 집합론 폰 노이만-베르나이스-괴델 집합론 모스-켈리 집합론 타르스키-그로텐디크 집합론
모형 이론	모형 해석 비표준 모형 유한 모형 이론 진릿값 타당성
증명 이론	형식 증명 연역 체계 형식 체계 정리 논리적 귀결 추론 규칙 구문
계산 가능성 이론	계산 가능성 이론 처치-튜링 논제 재귀 재귀 집합 재귀 열거 집합 결정 문제 정지 문제 계산 가능한 수 μ-재귀 함수 원시 재귀 함수