유한 모형 이론
Finite model theory유한 모델 이론은 모델 이론의 하위 영역이다. 모델 이론은 형식 언어(합성어)와 그 해석(수식어)의 관계를 다루는 논리의 한 분야다. 유한 모델 이론은 유한한 우주를 가진 유한 구조에 대한 해석에 대한 모델 이론의 제한이다.
모델 이론의 많은 중심 이론은 유한한 구조로 제한될 때 유지되지 않기 때문에 유한 모델 이론은 그 입증 방법에서 모델 이론과 상당히 다르다. 유한 모델 이론에 따라 유한한 구조물에 실패하는 고전적 모델 이론의 중심 결과로는 콤팩트성 정리, 괴델의 완전성 정리, 1차 논리(FO)에 대한 초고속화 방법 등이 있다. 모델 이론이 수학적 대수학에 많은 응용을 하는 반면, 유한 모델 이론은 컴퓨터 과학에서 "보통으로 효과적이지 않은"[1] 도구가 되었다. 즉, "수학적 논리학의 역사에서 대부분의 관심은 무한한 구조에 집중되어 왔다. [...] 그러나 컴퓨터가 가지고 있고 보유하고 있는 물체는 항상 유한하다. 연산을 연구하기 위해서는 유한구조 이론이 필요하다."[2] 따라서 유한 모델 이론의 주요 적용 영역은 서술적 복잡성 이론, 데이터베이스 이론 및 형식 언어 이론이다.
기본 과제
유한 모델 이론에서 공통적인 동기 부여 질문은 주어진 구조 부류가 주어진 언어로 설명될 수 있는가 하는 것이다. 예를 들어, FO 문장으로 그래프 간에 순환 그래프 클래스를 구분할 수 있는지 여부를 물을 수 있으며, 이는 순환도가 FO-expressible인지 여부를 묻는 것으로도 표현될 수 있다.
단일 유한 구조는 항상 1차 논리학에서 공리화할 수 있는데, 여기서 언어 L로 공리화된 구조는 단일 L-센턴스에 의해 이소모르프리즘에 고유하게 기술된 것을 의미한다. 마찬가지로 유한 구조의 모든 유한한 수집은 언제나 1차 논리로 공리화할 수 있다. 전부는 아니지만 일부 유한 구조물의 무한 수집도 단 하나의 1차 문장으로 공리화할 수 있다.
단일 구조물의 특성화
L언어는 하나의 유한구조 S를 공리화할 만큼 충분히 표현되어 있는가?
문제
그림에서 (1)과 같은 구조는 FO 문장으로 설명될 수 있다.
- 노드에는 다른 노드에 대한 에지가 있다:: x ( x, ).
- edge, (( , ) ).
- 다른 모든 노드와 되는 노드는 최소한 하나 : x y( ( , y) . }\y\ G)).
그러나 구조물의 경우 (1)과 (1)은 이형성이 아니므로 이러한 특성들은 구조물을 공리화하지 않는다.
비공식적으로 문제는 충분한 속성을 추가함으로써 이러한 특성들이 정확히 (1)을 기술하고 다른 구조(이형성까지)에 대해 유효한지 여부다.
접근하다
단일 유한 구조물의 경우, 구조를 단일 FO 문장으로 정밀하게 설명할 수 있다. 이 원리는 하나의 이항 관계 과 상수가 없는 구조물에 대해 여기에 설명되어 있다.
- 요소가 있다고 한다: : = i ¬(= ) j
- 의{\ 요소가 있다고 한다: : = y i i= y)
- 관계 의 모든 요소를 설명하십시오. 3= , j) ( i, )
- {\의 모든 비요소: 4= (, ) , ) {
모두 동일한 튜플 .. x }에 대해, yielding the FO sentence .
고정된 수의 구조로 확장
1차 문장으로 단일 구조를 설명하는 방법은 어떤 구조든 어느 정도 고정된 수만큼 쉽게 확장할 수 있다. 각 구조물에 대한 설명을 분리하여 고유한 설명을 얻을 수 있다. 예를 들어, 정의 문장이 및 인 두 의 경우 이는 다음과 같다.
무한구조로 확장
정의상 무한 구조를 포함하는 세트는 FMT가 다루는 영역 밖에 있다. 무한 모델을 가진 어떤 1차 이론도 이소모르프까지 독특한 모델을 가질 수 없다는 것을 암시하는 뢰웬하임-스콜렘 정리 때문에 FO에서는 무한구조가 결코 차별될 수 없다는 점에 유의한다.
가장 유명한 예는 아마도 스콜렘의 정리일 것인데, 산술에는 헤아릴 수 있는 비표준 모델이 있다.
구조물의 종류 특성화
언어 L은 특정 속성 P를 가진 유한한 구조를 정확히 (이소모르프까지) 설명할 수 있을 만큼 표현력이 있는가?
문제
지금까지 주어진 설명들은 모두 우주의 원소 수를 명시하고 있다. 불행히도 대부분의 흥미로운 구조들은 나무인 모든 그래프들이 연결되어 있거나 반복되어 있는 것처럼 특정한 크기로 제한되지 않는다. 따라서 한정된 수의 구조물을 구별하는 것은 특별한 중요성이 있다.
접근하다
일반적인 진술 대신, 다음은 차별받을 수 있는 구조와 차별할 수 없는 구조를 구별하는 방법론의 밑그림이다.
1. 핵심 아이디어는 재산 P가 FO로 표현될 수 있는지 보고 싶을 때마다 A가 P가 있고 B가 없는 구조 A와 B를 선택한다는 것이다. A와 B에 대해 동일한 FO 문장이 유지된다면, P는 FO로 표현될 수 없다. 요컨대:
- , P 및
여기서 은 (는) FO-ssentity α α α α αα α α 의 속기이고, P는 속성 P를 가진 구조물의 클래스를 나타낸다.
2. 방법론은 언어 자체의 결합을 이루는 언어의 하위 집합을 셀 수 없이 많이 고려한다. 예를 들어, FO의 경우 각 m에 대한 FO[m] 클래스를 고려한다. 각각의 m에 대해 위의 핵심 아이디어가 제시되어야 한다. 즉,
- , 및
각 및 FO[m]의 α(인치 α)에 대해 쌍 인 경우. 언어의 파티션을 구성하기 위해 FO[m] 클래스를 선택하는 것이 적절할 수 있다.
3. FO[m]를 정의하는 한 가지 일반적인 방법은 FO 공식 α의 정량자 순위 qr(α)를 통해 정량자 내포 깊이를 나타낸다. 예를 들어, 혼전 정상 형태의 공식의 경우, qr은 단순히 정량자의 총 수입니다. 그 다음 FO[m]는 qr(α) ≤ m을 가진 모든 FO 공식 α(또는 파티션이 필요한 경우, 정량자 등급이 m과 같은 FO 공식으로 정의할 수 있다.
4. 따라서 이 모든 것은 하위 집합 FO[m]에 α α 을(를) 표시하는 것으로 귀결된다. 여기서의 주된 접근법은 에렌페우흐트-프라우제 게임이 제공하는 대수적 특성화를 이용하는 것이다. 비공식적으로, 이것들은 A와 B에 대해 하나의 부분 이형성을 취하며, 누가 게임을 이기느냐에 따라 를 입증하거나 반증하기 위해 m을 확장한다.
예
우리는 주문된 구조 A = (A, size)의 크기가 짝수라는 속성은 FO로 표현할 수 없다는 것을 보여주고 싶다.
1. 아이디어는 A ∈ EVEN과 B ∉ EVEN을 선택하는데, 여기서 EVEN은 짝수 크기의 모든 구조물의 등급이다.
2. 우주를2 A2 = {1, 2, 3, 42}, B = {1, 2, 3}, 그리고 {1, 22, 3}. 분명히 A with2 EVEN과 B2 ∉ EVEN.
3. m = 2의 경우, 이제 우리는 A와2 B의2 2-move Ehrenfeucht-Frassssé 게임에서 복제자가 항상 승리하므로, 따라서 A와2 B는2 FO[2]에서 차별을 받을 수 없다는 것을 보여줄 수 있다*. 모든2α α FO[2]에 대해αα ⇔ B2 style α.
4. 다음으로 m을 증가시켜 구조물의 크기를 늘려야 한다. 예를 들어, m = 3의 경우, 우리는 반드시 A와3 B를3 찾아야만 중복자가 항상 3 무브 게임에서 승리할 수 있다. 이는3 A = {1, ..., 8} 및 B3 = {1, ..., 7}에 의해 달성될 수 있다. 보다 일반적으로 우리는m Am = {1, ...} 및 Bm = {1, ..., 2-1m}을 선택할 수 있다. 어떤 경우든 중복자는 항상 이 구조 쌍에 대해 m-m-move 게임을 승리한다*.
5. 따라서 유한 순서 구조의 EVEN은 FO로 표현할 수 없다.
(*) 여기서는 주안점이 아니기 때문에 에렌페우흐트-프라우제 경기 결과에 대한 증거가 누락되었다는 점에 유의한다.
적용들
데이터베이스 이론
SQL의 상당한 부분(명칭 관계 대수)은 1차 논리(Codd의 정리를 통해 도메인 관계적 미적분학에서 보다 정밀하게 번역할 수 있음)에 근거한 것으로, 다음 예에서 알 수 있다. "FIRST_NAME" 및 "LAST_NAME" 열이 있는 데이터베이스 테이블 "GIRLS"를 생각해 보십시오. 이것은 2진수 관계에 해당하며, 예를 들어 FIRST_NAME X LAST_NAME에서 G(f, l)라고 한다. 이름이 'Judy'인 모든 성을 반환하는 FO 쿼리 {l : G('Judy'), l)}은 다음과 같이 SQL을 들여다본다.
GIRLS에서 LAST_NAME을 선택하고 여기서 FIRST_NAME = 'Judy'
여기서 우리는 모든 성이 한 번만 나타난다고 가정한다(또는 우리는 관계와 대답이 가방이 아니라 세트라고 가정하기 때문에 SELECT DICTION을 사용해야 한다).
다음으로 우리는 좀 더 복잡한 진술을 하고 싶다. 따라서 "GIRLS" 테이블 외에도 "FIRST_NAME" 및 "LAST_NAME" 컬럼이 있는 "Boys" 테이블이 있다. 이제 우리는 적어도 한 소년과 성이 같은 모든 소녀들의 성을 묻고 싶다. FO 쿼리는 {(f,l) : ∃h(G(f, l) ∧ B(h, l) )}이며, 해당하는 SQL 문은 다음과 같다.
FIRST_NAME, LAST_NAME from GIRLS(여기서 LAST_NAME IN)(소년에서 LAST_NAME 선택);
"선택"을 표현하기 위해 후속 선택 문구와 함께 새로운 언어 요소 "IN"을 도입했다는 점에 유의하십시오. 이것은 언어를 배우고 구현하기 위한 더 높은 난이도의 가격에 대해 더 표현하게 만든다. 이것은 공식적인 언어 디자인에서 흔히 볼 수 있는 트레이드오프다. 위에 표시된 방법("IN")은 언어를 확장하는 유일한 방법이 아니다. 다른 방법은 예를 들어 "JOIN" 연산자를 도입하는 것이다. 즉, 다음과 같다.
고유 g를 선택하다FIRST_NAME, g.GIRLS g에서 LAST_NAME, BOYS b where g.LAST_NAME=b.LAST_NAME;
예를 들어, 1차 로직은 타동적 폐쇄를 표현할 수 없기 때문에 일부 데이터베이스 애플리케이션에는 너무 제한적이다. 이로 인해 SQL:1999의 재귀 WITH와 같이 데이터베이스 쿼리 언어에 더 강력한 구성이 추가되었다. 따라서 고정점 로직과 같은 보다 표현력 있는 로직들은 데이터베이스 이론과 응용 프로그램과의 관련성 때문에 유한한 모델 이론으로 연구되어 왔다.
쿼리 및 검색
서술적 데이터에는 정의된 관계가 없다. 따라서 텍스트 검색 질의의 논리적 구조는 다음과 같이 제안적 논리로 표현될 수 있다.
("Java" 및 "섬"이 아님) 또는 ("C#" 및 "음악"이 아님)
전체 텍스트 검색의 난제는 결과의 순위와 같은 데이터베이스 쿼리와는 다르다는 점에 유의하십시오.
역사
- 트라히텐브로트 1950: 1차 논리에서의 완전성 정리 실패
- Solz 1952: 1차 논리에서의 스펙트럼 특성화
- Fagin 1974: 실존적 2차 논리학에서 표현 가능한 모든 속성 집합은 정확하게 복잡도 등급 NP이다.
- Chandra, Harel 1979/80: Transitive closure -> 쿼리를 FMT의 중심 개체로 표현할 수 있는 데이터베이스 쿼리 언어에 대한 고정 포인트 1차 로직 확장
- IMmerman, Vardi 1982: 순서 구조에 대한 고정점 로직은 PTIME -> 서술적 복잡성을 캡처한다(Emmerman-Szelpcsnei 정리).
- 에빙하우스, 플럼 1995: 첫 번째 종합서 "완료 모형 이론"
- 아비테불, 헐, 비아누 1995: 책 "데이터베이스의 기초"
- Immerman 1999: 책 "설명적 복잡성"
- 쿠퍼, 리브킨, 파레다인스 2000: "Constraint Database" 책
- 다르슈타트 2005/아헨 2006: "알고리즘 모델 이론"에 대한 첫 국제 워크숍
인용구
- ^ Fagin, Ronald (1993). "Finite-model theory – a personal perspective" (PDF). Theoretical Computer Science. 116: 3–31. doi:10.1016/0304-3975(93)90218-I.
- ^ Immerman, Neil (1999). Descriptive Complexity. New York: Springer-Verlag. p. 6. ISBN 0-387-98600-6.
참조
- Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995). Finite Model Theory. Springer. ISBN 978-3-540-60149-4.
- Abiteboul, Serge; Hull, Richard; Vianu, Victor (1995). Foundations of Databases. Addison-Wesley. ISBN 0-201-53771-0.
- Immerman, Neil (1999). Descriptive Complexity. New York: Springer. ISBN 0-387-98600-6.
추가 읽기
- Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. ISBN 978-3-540-00428-8. Zbl 1133.03001.
외부 링크
![]() | Wikibooks에는 다음과 같은 주제의 책이 있다. 유한 모형 이론 |
- Libkin, Leonid (2009). "The finite model theory toolbox of a database theoretician". PODS 2009: Proceedings of the twenty-eighth ACM SIGACT–SIGMOD symposium on Principles of database systems. pp. 65–76. doi:10.1145/1559795.1559807. 일반적인 소개 및 개요로도 적합함.
- 레오니드 리브킨. "유한 모델 이론의 요소"의 소개 장. 데이터베이스, 복잡성 및 공식 언어의 세 가지 주요 애플리케이션 영역에 대한 동기 부여
- 요우코 베네넨 유한 모델 이론에 관한 짧은 코스. 헬싱키 대학 수학학부. 1993-1994년 강의에 근거하여.
- 아누지 다와르. 무한하고 유한한 모델 이론, 슬라이드, 2002년 캠브리지 대학교
- "Algorithmic Model Theory". RWTH Aachen. Archived from the original on 17 July 2012. Retrieved 7 November 2013. 열린 FMT 문제 목록을 포함한다.