계산가능성 논리학

이 글의 모든 언급은 단 한 명의 저자인 G. Japaridze가 독점적으로 하고 있다. 관련 토론은 토크 페이지에서 찾을 수 있다. 추가 출처에 인용구를 도입하여 이 기사를 개선할 수 있도록 도와주십시오. 출처 찾기: "컴퓨팅 논리" – 뉴스 · 신문 · 책 · 학자 · JSTOR(2020년 5월)

계산가능성 논리(CoL)는 형식적 진리의 이론인 고전적 논리와는 반대로, 계산가능성의 체계적 형식 이론으로서 논리를 재개발하기 위한 연구 프로그램이자 수학적 프레임워크다.2003년에 Giorgi Japaridze에 의해 소개되었고 그렇게 이름이 지어졌다.^[1]

고전적 논리학에서 수식은 참/거짓 문장을 나타낸다.CoL에서 공식은 계산 문제를 나타낸다.고전적 논리학에서 공식의 타당성은 그 형식에 따라 달라지지만 그 의미에 따라 달라지지 않는다.CoL에서 유효성은 항상 계산 가능하다는 것을 의미한다.보다 일반적으로, 고전적 논리는 우리에게 주어진 진술의 진리가 항상 주어진 다른 진술들의 진리에서 따라올 때를 말해준다.마찬가지로, CoL은 주어진 문제 A의 연산성이 항상 주어진 다른₁ 문제 B,...,B의_n 연산성에서 따라올 때 우리에게 알려준다. 더욱이, CoL은 B₁,...,B의_n 알려진 솔루션으로부터 그러한 A에 대한 해법(알고리즘)을 실제로 구축할 수 있는 균일한 방법을 제공한다.

CoL은 가장 일반적인 상호작용적 의미에서 컴퓨터 문제를 형성한다.CoL은 컴퓨터 문제를 기계가 그 환경에 대항하여 하는 게임으로 정의한다.그러한 문제는 환경의 모든 가능한 행동에 대항하여 게임을 이기는 기계가 있다면 계산할 수 있다.이러한 게임 플레이 기계는 Church-Turing 논문을 대화형 수준으로 일반화한다.고전적인 진리의 개념은 특별한 상호작용이 없는 계산성의 사례로 판명된다.이것은 고전적 논리를 CoL의 특별한 조각으로 만든다.따라서 CoL은 고전적 논리의 보수적인 확장이다.계산가능성 논리는 고전적 논리보다 더 표현적이고 건설적이며 계산적으로 의미가 있다.고전적 논리 외에도 독립 친화적(IF) 논리와 선형 논리와 직관적 논리의 일정한 적절한 확장 또한 CoL의 자연 파편인 것으로 판명된다.^[2][3]따라서 "직관적 진리", "선형 논리 진리" 및 "IF 논리 진리"의 의미 개념은 CoL의 의미론에서 도출될 수 있다.

CoL은 계산될 수 있는 것과 어떻게 계산될 수 있는지에 대한 근본적인 질문에 체계적으로 대답한다. 따라서 CoL은 건설적인 응용 이론, 지식 기반 시스템, 계획과 행동을 위한 시스템 등 많은 응용 프로그램을 가지고 있다.이 중에서, constructive에 애플리케이션만 이론을 광범위하게 지금까지 탐구되어 왔다:CoL-based 수 이론들을 시리즈,"clarithmetics",classical-logic-based 페아노 산술에 computationally과 complexity-theoretically 의미 있는 대안과 시스템 같은 변화로 constructed[4][5] 왔다 한 것도 신청했다.boun추론 산술

자연공제, 미적분과 같은 전통적인 증명시스템은 CoL의 비경쟁 파편을 공리화하기에 불충분하다.이것은 대체적인, 보다 일반적이고 유연한 증명 방법들을 개발할 필요가 있었다. 예를 들어, 권선 미적분학 같은.^[6][7]

언어

CoL의 전체 언어는 고전적인 1차 논리학의 언어를 확장한다.그것의 논리 어휘는 여러 종류의 접속사, 불분열, 정량자, 함축, 부정, 그리고 소위 재발 연산자를 가지고 있다.이 컬렉션은 고전적 논리의 모든 연결자 및 정량자를 포함한다.그 언어는 또한 두 종류의 비논리적 원자를 가지고 있다: 기초와 일반이다.고전적 논리의 원자에 지나지 않는 초등 원자는 기본적인 문제, 즉 참일 때는 기계가 자동으로 이기고 거짓일 때는 지는 동작이 없는 게임을 나타낸다.반면에 일반 원자는 초급 또는 비원격의 어떤 게임으로도 해석될 수 있다.의미론적으로나 구문론적으로나 고전적 논리는 그 언어에서 일반 원자를 금지하고, ¬, ∧, ∧, ∨, → ∀, ∃ 이외의 모든 연산자를 금지함으로써 얻은 CoL의 단편일 뿐이다.

Japaridze는 CoL의 언어가 개방되어 있으며, 더 많은 연장이 있을 수 있다고 반복적으로 지적해 왔다.이 언어의 표현력 때문에, 공리화 구축이나 CoL 기반의 응용 이론 구축과 같은 CoL의 발전은 보통 언어의 하나 또는 다른 적절한 조각에 국한되어 왔다.

의미론

CoL의 의미론의 기초가 되는 게임을 정적 게임이라고 한다.그러한 게임들은 턴 오더가 없다; 다른 선수들이 "생각"하는 동안 플레이어는 항상 움직일 수 있다.그러나 정적인 게임은 너무 오래 생각한다고 해서(자신의 움직임을 지연시킨다고) 선수를 처벌하지 않기 때문에, 그러한 게임은 결코 속도의 경쟁이 되지 않는다.모든 초등 게임은 자동적으로 정적이 되며, 일반 원자의 해석도 허용된다.

정적 게임에는 기계와 환경이라는 두 명의 플레이어가 있다.기계는 환경의 동작에 제한이 없는 반면 알고리즘 전략만 따를 수 있다.각 경기(플레이)는 이들 선수 중 한 명이 이기고 다른 한 명이 진다.

CoL의 논리적 운영자는 게임에 대한 운영으로 이해된다.여기서 우리는 비공식적으로 그 운영들 중 일부를 조사한다.단순성을 위해 우리는 담론의 영역이 항상 모든 자연수의 집합이라고 가정한다: {0,1,2,...}.

부정의 ¬("not")작전은 두 선수의 역할을 전환시켜, 기계에 의한 움직임과 승리를 환경에 의한 것으로 바꾸며, 그 반대의 경우도 마찬가지다.예를 들어 체스가 백인 플레이어의 관점에서 체스 게임(그러나 동점이 배제된 상태)이라면, ¬체스는 흑인 플레이어의 관점에서 같은 게임이다.

병렬접속사 ∧("팬드")과 병렬분리 ∨("포르")는 게임을 병렬적으로 결합한다.A∧B 또는 A∨B의 연주는 두 결막의 동시극이다.그 기계는 둘 다 이기면 A ifB를 얻는다.그 기계는 그들 중 적어도 한 명이라도 이기면 A aB를 얻는다.예를 들어 체스 ¬체스는 두 판의 게임으로, 하나는 흰색, 하나는 검은색, 그리고 하나는 기계의 임무는 적어도 한 판에서 이기는 것이다.이런 게임은 한 판에서 다른 판으로 그의 움직임을 베끼면 상대가 누구인지에 상관없이 쉽게 이길 수 있다.

병렬 함축 연산자 → ("피복제")는 A→B = ¬A∨B로 정의된다.이 작전의 직관적인 의미는 B를 A로 축소하는 것, 즉 상대가 B를 해결하는 한 A를 해결하는 것이다.

병렬 정량자 ∧("pall")과 ∨("pexist")은 ∧xA(x) = A(0)∧A(2)∧...와 ∨xA(x) = A(0)∨A(1)∨A(2)∨A(2)∨A(2)∨...로 정의할 수 있다.따라서 이것들은 A(0), A(1), A(2), ...의 동시 재생이며 각각 별도의 보드에 있다.이 기계는 이 모든 게임에서 이기면 ∧xA(x)를, somexA(x)를 이기면 ∨xA(x)를 얻는다.

반면에 블라인드 정량자 ∀("blall")과 ∃("blexist")은 싱글보드 게임을 생성한다.∀xA(x) 또는 ∃xA(x)의 런은 A의 단일 런입니다.이러한 실행이 가능한 x 값 모두를 위해 A(x)의 원 런이면 기계는 winsxA(x) (resp. ∃xA(x))를 획득하고, 이것이 하나 이상에 대해 사실이면 ∃xA(x)를 획득한다.

지금까지 특징지어졌던 모든 운영자들은 그들이 초등(무모) 게임에 적용되었을 때 그들의 고전적인 운영자들과 똑같이 행동하고, 같은 원리를 검증한다.그렇기 때문에 CoL은 고전적 논리와 같은 기호를 그러한 연산자에 사용하는 것이다.그러나 이러한 운영자들이 비초등 게임에 적용될 때, 그들의 행동은 더 이상 고전적이지 않다.따라서 예를 들어 p가 기초 원자이고 P가 일반 원자라면 p→p∧p는 유효하지만 P→P∧P는 유효하지 않다.그러나 배제된 중간 P∨P의 원칙은 여전히 유효하다.동일한 원칙은 다른 세 종류의 분리(선택, 순차, 토글)에 모두 유효하지 않다.

A bB라고 쓰여진 A와 B 게임의 선택 분리 ("("chor")은 기계가 이기기 위해서는 두 개의 분리 중 하나를 선택한 다음 선택된 구성 요소에서 이기기 위해 해야 하는 게임이다.순차적 분리("sor") AHB는 A로 시작하며, 또한 기계가 "스위치"를 하지 않는 한 A로 끝나게 되는데, 이 경우 A는 포기되고 게임은 다시 시작되어 B로 계속된다.토글 분리("토르") A⩛B에서 기기는 A와 B 사이에서 제한된 횟수만큼 전환될 수 있다.각 분리 운영자는 두 선수의 역할을 서로 바꾸어 얻은 이중 접속사를 가지고 있다.해당 정량자는 더 나아가 병렬 정량자의 경우와 같은 방법으로 무한 접속사 또는 분리로 정의할 수 있다.각 분류 구분은 또한 병렬 시사 →의 경우와 동일한 방식으로 해당 시사 연산을 유도한다.예를 들어 선택적 함축성("치메plication") AbB는 aAbB로 정의된다.

A의 평행 반복("사전")은 무한 평행 접속사 A∧A∧A∧...로 정의할 수 있다.순차적("반복")과 토글링("반복")의 종류는 유사하게 정의될 수 있다.

코어커런스 연산자는 무한 분리라고 정의할 수 있다.가장 강력한 종류의 재발인 분기재발("Breurance") ⫰은 해당 접속사가 없다.⫰A는 A로 시작하고 진행하는 게임이다.그러나 환경은 언제든지 "복제적인" 움직임을 할 수 있게 되어, 당시 A의 위치의 2개의 사본을 만들어, 공통의 과거가 있지만 아마도 다른 미래 발전이 있는 두 개의 평행 쓰레드로 플레이를 분할한다.같은 방식으로, 환경은 어떤 실의 어떤 위치도 더 복제할 수 있고, 따라서 점점 더 많은 A의 실을 만들 수 있다.그 실들은 병렬로 연주되며, 기계는 모든 실에서 A를 획득해야 aA에서 우승자가 된다.분기 코어커런스("코브레커런스") ⫯은 "기계"와 "환경"을 상호 교환하여 대칭적으로 정의된다.

각 종류의 재발은 그에 상응하는 약한 버전의 암시와 약한 버전의 부정을 더욱 유도한다.전자는 구문이라고 하고, 후자는 반박이라고 한다.가지치기법("brimplication") A⟜B는 ⫰A→B에 지나지 않으며, A의 가지치기법("brefutation")은 A⟜⊥이며, 여기서 ⊥은 항상 잃어버리는 초등 게임이다.다른 모든 종류의 복제와 리퓨테이션에서도 유사하다.

문제 사양 도구로 사용

CoL 언어는 문헌에 이름이 정립되어 있든 없든 무한히 다양한 연산 문제를 명시할 수 있는 체계적인 방법을 제공한다.다음은 몇 가지 예다.

f를 단일한 함수가 되게 하라.f를 계산하는 문제는 ⊓x⊔y(y=f(x))로 쓰일 것이다.CoL의 의미론에 따르면, 이것은 x에 대한 값 m을 선택해야 하는 환경에 의해 첫 동작("입력")이 이루어지는 게임이다. 직관적으로 이것은 기계에게 f(m)의 값을 말해달라고 요구하는 것과 같다.경기는 continuesy(y=f(m)이제 기계는 y에 대한 값 n을 선택할 수 있는 이동("출력")을 할 것으로 예상된다.이것은 n이 f(m)의 값이라고 말하는 것과 같다.게임은 이제 n이 f(m)의 값일 경우에만 기계가 이기는 n=f(m)로 내려온다.

p를 단수 술어로 하자.그러면 thenx(x)⊔p(x)는 p를 결정하는 문제를, ⊓x(p(x)&ᐁ¬p(x)는 semideciding p의 문제를, ⊓x(x)는 재귀근접 p의 문제를 나타낸다.

p와 q를 두 개의 단항 술어가 되게 하라.그러면 ⊓x(x)⊔¬p(x)⟜⊓x(q)⊔qq(x))는 튜링 감소 q~p의 문제를 표현한다(양방향 문제 ⊓x(p)x)p(x)⟜x(q(x)⊔q(x)가 계산 가능한 경우에만 p로 turing 환원 가능하다는 의미).⊓x(p(x)⊔¬p(x)→⊓x(q(x)⊔¬q(x))는 p에 대한 신탁을 한 번만 쿼리할 수 있는 강력한 버전의 튜링 축소를 위해 동일한 작업을 수행한다.⊓x⊔y(q)(x) ↔p(y)는 다원 감소 q 대 p의 문제에 대해서도 동일하게 한다.좀 더 복잡한 표현으로 모든 종류의 이름없지만 잠재적으로 의미 있는 연산 문제, 예를 들어, "다수가 qto p를 줄이는 문제에 대한 semideciding r의 문제를 줄이는 것"과 같은 계산 문제에 대한 모든 종류의 관계와 연산을 포착할 수 있다.기계의 작업에 시간 또는 공간 제한을 가하면, 그러한 관계와 운영의 이론적 상대인 복잡성을 더 많이 갖게 된다.

문제 해결 도구로서

CoL의 다양한 파편에 대해 알려진 연역 시스템은 시스템의 문제 증명에서 자동으로 해결책(알고리즘)을 추출할 수 있는 속성을 공유한다.이 속성은 그 시스템에 근거한 모든 응용 이론에 의해 더욱 계승된다.그래서 주어진 문제에 대한 해결책을 찾기 위해서는 그것을 CoL의 언어로 표현하고 나서 그 표현에 대한 증거를 찾는 것으로 충분하다.이 현상을 바라보는 또 다른 방법은 CoL의 공식 G를 프로그램 사양(골)으로 생각하는 것이다.그리고 G의 증거는 보다 정확하게는 그 규격에 부합하는 프로그램으로 해석된다.증명 자체가 사실 그런 검증이기 때문에 규격에 부합하는지 검증할 필요가 없다.

CoL 기반 응용 이론의 예는 이른바 클라리 산술학이다.이것들은 Peano 산술 PA가 고전적 논리에 기초하고 있는 것과 같은 의미로 CoL에 근거한 숫자 이론이다.그러한 시스템은 보통 PA의 보수적인 연장선상에 있다.일반적으로 모든 페이노 공리를 포함하며, 그 위에 후계 함수의 연산성을 나타내는 expressingx⊔y(y=x')와 같은 한두 개의 엑스트라 피아노 공리를 더한다.전형적으로 그것은 또한 유도나 이해의 건설적인 버전과 같은 하나 또는 두 개의 비논리적 추론 규칙을 가지고 있다.이러한 규칙의 일상적 변화를 통해 하나 또는 다른 대화형 계산 복잡성 등급 C를 특징짓는 건전하고 완전한 시스템을 얻을 수 있다.이것은 어떤 문제가 이론에 증거가 있는 경우에만 C에 속한다는 의미에서이다.따라서 그러한 이론은 알고리즘적인 솔루션뿐만 아니라 다항식 시간이나 로그 공간에서 실행되는 솔루션과 같이 필요에 따라 효율적인 솔루션을 찾는 데 사용될 수 있다.모든 명료한 산술적 이론은 동일한 논리적 공식을 공유하며, 대상 복잡도 등급에 따라 비논리적 공론만 다르다는 점을 지적해야 한다.이들의 두드러진 특징은 유사한 포부를 가진 다른 접근법(경계 산술 등)과 구별되는 것으로 PA를 약화시키기보다는 확장하여 후자의 완전한 연역력과 편리성을 보존한다는 점이다.

참고 항목

• 게임 의미론
• 인터랙티브 연산
• 논리학
• 계산가능성에 대한 로직

참조

외부 링크

• 계산가능성 논리 홈페이지 대상 종합조사.
• 기오르기야파리제
• 게임 의미론 또는 선형 논리?
• 계산논리에 대한 강의과정
• 추상적 자원 의미론 및 연산 논리 N의 비디오 강의.베레쉬차긴
• 위의 홈페이지와 동일한 다운로드 가능 로직 조사(PDF)