번치 논리학

뭉치논리는^[1] 피터 오힌과 데이비드 핌이 제안한 다양한 하부구조 논리학이다.뭉친 논리는 컴퓨터와 다른 시스템의 구성 분석에 도움이 되는 자원 구성에 대한 추론을 위한 원시적 요소를 제공한다.범주-이론적·진실적 기능적 의미론을 가지고 있는데, 이는 자원의 추상적 개념으로 이해할 수 있으며, 대부분의 교정적 계산에서와 같이 목록이나 (다중) 집합이 아닌 수반적 판단에서 맥락 Ⅱ를 나무와 같은 구조(분지)로 보는 증명 이론이 있다.번치 논리는 관련 유형 이론을 가지고 있으며, 그것의 첫 번째 적용은 명령적 프로그램에서 앨리어싱과 다른 형태의 간섭을 제어하는 방법을 제공하는 것이었다.^[2]이 논리는 분리논리의 주장언어의 기초가 되는 프로그램 검증과 ^[3]시스템의 구성요소가 사용하는 자원을 분해하는 방법을 제공하는 시스템 모델링에서 추가 응용을 보았다.^[4][5][6]

파운데이션

고전적 논리의 공제 정리는 연결과 함축에 관련된다.

$A\wedge B\vdash C\quad {\mbox{iff}\quad A\vdash B\Rightarrow C}$

번치 논리학에는 다음과 같은 두 가지 버전의 공제 정리가 있다.

$[\displaystyle A*B\vdash C\quad {\mbox{iff}}\quad A\vdash B{-\!\!]!*}C\qquad {\mbox{and}}\qquad A\wedge B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Rightarrow C}$

${\displaystyle }$${\displaystyle A}$ ${\displaystyle \ast }$ ${\displaystyle B}$ ${\displaystyle A*B}$ 및 $B$ -${\displaystyle \ast }$ C ${\displaystyle$ B${-\!\!$$*}C}$은(는) 자원을 고려하는 연결 및 함축의 형식이다(아래 설명 참조).이러한 결합형 번데기 논리에는 공식이 있으며, 때로는 *의 단위인 I 또는 emp가 쓰여 있다. 원래의 번데기 논리 $\wedge {\displaystyle }$ ${\displaystyle \wedge }$과 $\Rightarrow {\displaystyle }$ ${\displaystyle \Rightarrow }$은 직관적 논리에서 나온 결합형인$$ 반면, 부울 변형은$\$ {\$displaystytylease$\wise \$wedge$\wisease stypector \wedge }과$$ \displaystone \displaystypective \d${\displaystyle }$전통적인 부울 논리처럼${\displaystyle }$as ${\displaystyle \Rightarrow }($및 $\neg {\displaystyle \mathrm{}}$ ${\displaystyle \neg$}$$)그러므로 뭉친 논리는 건설적 원리와 양립할 수 있지만, 그것들에 의존하는 것은 결코 아니다.

진리 기능적 의미론(리소스 의미론)

이러한 공식들을 이해하는 가장 쉬운 방법은 그 사실적인 기능적 의미론적 측면에 있다.이 의미론에서 공식은 주어진 자원과 관련하여 참이거나 거짓이다.${\displaystyle \ast }$ ${\displaystyle B}$ ${\displaystyle A*B}$은(는) 현재 있는 $자원$을 A$${\$displaystyle A}$ 및 $B$ ${\displaystyle$ B$}$을(를) 만족하는 자원으로 분해할 수 있다고$$ 주장한다$.$ B -${\displaystyle c}$ C$${\$displaystystyle B{-\!\!$$*}C}$은(는)$$B {\$displaystyle$B}을$($를) 만족하는 추가 리소스로 자원을 동시에 구성하면 결합된 $자원$이 C ${\\displaystyle$ C$}$을(를) 만족시킨다고 말한다.$$$\wedge {\displaystyle }$ ${\displaystyle$ $\$$wedge }$ 및$$ $\Rightarrow {\displaystyle }$ ${\displaystystyley$ \$Rightarrowe}$은 익숙한 의미를$$ 갖는다.

이 공식 판독의 기초는 Pym이 진일보한$$ 강제 의미론 r${\displaystyle r}$ A ${\displaystyle r\models A}$에 의해 제공되었다. 강제 관계는 'A hold of resource r'를 의미한다.의미론은 직관적 또는 모달적 논리의 크립케의 의미론과 유사하지만, 모델의 요소들은 서로 접근 가능한 가능한 세계라기 보다는 구성되고 분해될 수 있는 자원으로 간주된다.예를 들어, 접속사에 대한 강제 의미론은 형식이다.

${\displaystyle r\models A*B\quad {\mbox{iff}}\quad \exists r_{A}r_{B}.\,r_{A}\models A,\,r_{B}\models B,\,{\mbox{and}}\,r_{A}\bullet r_{B}\leq r}$

여기서 $r{\displaystyle {}_{}}$ ${\displaystyle A_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle r_{}}$ B ${\$은(는) 자원을 결합하는 방법이고${\displaystyle }$and ${\displaystyle \leq$}은$$근사치의 관계다.

이 묶음논리의 의미론들은 관련 논리(특히 루틀리의 운영 의미론)에서 선행작업에 의존한다.–Meyer)는 ${\displaystyle \bullet }$ ${\displaystyle r}$ ${\displaystyle \bullet }$ ${\displaystyle r}$ $\$ r {\$displaystyle r\bullet$ r$\leq$$$ r}을(를) 요구하지 않고$$ $\wedge {\displaystyle }$ ${\displaystyle \wedge }$ 및 $\Rightarrow {\displaystyle }$ ${\displaystyle \Rightarrow }$의 표준 직관적 또는 고전적 버전의 의미론을 수용함으로써 그것과 다르다$.$$r{\displaystyle }$ ${\displaystyle \bullet }$ ${\displaystyle r}$ ${\displaystyle \le }$ ${\displaystyle r}$ ${\displaystyle r\bullet r\leq$ r$}$ 속성은 관련성을 생각할 때 정당화되지만$$ 자원의 고려에 의해 거부된다. 한 자원의 복사본이 두 개 있는 것은 한 개 있는 것과 같지 않으며, 일부 모델(예: 힙 모델)에서는 r ${\displaystyle \bullet }$ ${\displaystyle r}$ ${\displaystyle r\bullet$ r$}$이 정의되지 않을 수도$$ 있다.⇒ ${\displaystyle \Rightarrow }($또는 부정)의 표준 의미론은 모델링 자원의 관점에서 문제가 되지 않고 따라서 일괄 논리로 거부되지 않는 '물질적 함의 패러독스'를 벗어나기 위해 관련론자들에 의해 종종 거부된다.의미론도 선형논리의 '위상 의미론'과 관련이 있지만, 다시 $\wedge {\displaystyle }$ ${\displaystyle \wedge }$과 $\Rightarrow {\displaystyle }$ ${\displaystyle \Rightarrow }$의 표준(이른 부울) 의미론을 수용함으로써 구별되는데$,$ 이 의미론은 건설적이기 위해 선형논리에서 거부된다.이러한 고려사항은 Pym, O'Hearn, Yang의 자원 의미론 기사에서 자세히 논의된다.^[7]

범주형 의미론(더블 클로즈드 범주)

번데기 논리의 공제 정리의 이중 버전은 그에 상응하는 범주-이론적 구조를 가지고 있다.직관적 논리의 증거는 데카르트 폐쇄 범주, 즉 홈 세트와 관련된 (자연적 A와 C) 결합 서신을 만족하는 유한한 제품을 가진 범주로 해석될 수 있다.

${\displaystyle Hom(A\wedge B,C)\quad {\mbox{is imbox to}}\quad Hom(A,B\Rightarrow C)}$

묶인 논리는 두 개의 그러한 구조를 가진 범주로 해석될 수 있다.

군집화된 논리학의 범주형 모델은 닫힌 두 개의 구조물을 가진 단일 범주로서, 하나는 대칭 단면체이고 다른 하나는 닫힌 데카르트 구조를 가진 것이다.

Day의 텐서 제품 구조를 사용하여 다수의 분류 모델을 제공할 수 있다.^[8]또한, 뭉친 논리의 관계적 파편에는 게임 의미론도 주어졌다.^[9]

대수적 의미론

군집 논리의 대수적 의미론은 그 범주적 의미론의 특수한 경우지만, 진술이 간단하고 좀더 접근가능할 수 있다.

An algebraic model of bunched logic is a poset that is a Heyting algebra and that carries an additional commutative residuated lattice structure (for the same lattice as the Heyting algebra): that is, an ordered commutative monoid with an associated implication satisfying ${\displaystyle A*B\leq C\quad {\mbo$$x{iff}}\quad A\leq B{-\!\!$$*}C$ .

뭉친 논리의 부울 버전은 다음과 같은 모델을 가지고 있다.

부울 번치 논리의 대수적 모델은 부울 대수학이며 추가적인 잔류 정류 단면 구조를 가진 포셋이다.

증명 이론 및 유형 이론(번치)

뭉친 논리의 미적분은 평평한 목록과 같은 구조 대신 나무와 같은 가설의 맥락을 갖는다는 점에서 일반적인 순열 미적분학과는 다르다.연속적인 근거 증명 이론에서, 수반적 판단의$$ $\Delta {\displaystyle \mathrm{}}$ ${\displaystyle \Delta$ \Delta $}$ 컨텍스트 Δ ${\displaystyle a}$A ${\displaystyle$ \$Delta \vdash A}$는 잎이 명제이고 내부 노드에 두 개의 접속사에 해당하는 구성 모드를 라벨로 표시한 유한한 나무다.콤마와 세미콜론을 결합한 두 연산자는 두 개의 함축에 대한 도입 규칙에서 (예를 들어) 사용된다.

${\displaystyle {\frac {\Gamma ,A\vdash B}{\\\Gamma \vdash A{-\\!\!*}B}\qquad \qquad {\frac {\Gamma ;A\vdash B}{\Gamma \vdash A{\Rightarrow }}}}}$

두 구성 규칙의 차이는 여기에 적용되는 추가 규칙에서 비롯된다.

• 승법구성 $\Delta {\displaystyle \mathrm{}}$ ,${\displaystyle }$, ${\displaystyle \Delta ,\Gamma$}은$($는) 약화와 수축의 구조적 규칙을 부정한다$$.
• 가법성분 $\Delta {\displaystyle \mathrm{};}$ ${\displaystyle \mathrm{\gamma }}${\$displaystyle \Delta$;\$Gamma$}은(는) 전체 번치의 약화와 수축을 인정한다$$.

묶음에 대한 구조 규칙과 기타 연산은 종종 나무 컨텍스트 내에서 깊이 적용되며, 최상위 수준뿐만 아니라, 따라서 어떤 의미에서는 깊은 추론의 미적분이다.

뭉친 논리에 대응되는 것은 두 종류의 함수형을 가진 유형 이론이다.Curry-Howard 통신에 이어 함축에 대한 도입 규칙은 기능 유형에 대한 도입 규칙에 해당한다.

${\displaystyle {\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda x.M:A.{-\!*}B}\qquad \qquad {\frac {\Gamma ;x:A\vdash M:B}{\Gamma \vdash \alpha x.M:A{\Rightarrow }B}}$

여기서는 기능 유형별로 하나씩$$$one{\displaystyle }$ ${\displaystyle \lambda }$과 $\alpha {\displaystyle }$ ${\displaystyle \alpha }$ 두 개의 구별되는 바인더가 있다.

군집논리의 증명 이론은 관련 논리에 군집을 사용하는 데 역사적 부채가 있다.^[10]그러나 뭉친 구조는 어떤 의미에서 범주적 의미와 대수적 의미론에서 파생될 수 있다: -${\displaystyle \ast }$ ${\$$displaystyle *}}}$을(를) 왼쪽의 시퀀스 안에서 모방해야 하며$,{\displaystyle }$ ${\displaystyle \Rightarrow }$을(를) 도입하려면 $}{\displaystystyle \wedge }}$를 모방해야 한다$.$ 이러한 고려는 두 결합 연산자의 사용으로 이어진다.

James Brotherston은 Belnap의 디스플레이 논리 개념을 채택하면서 ^[11]뭉친 논리와 변형에 대한 통일된 증명 이론에 대해 더 많은 중요한 연구를 수행했다.^[12]

갈미쉬, 메리, 핌은 라벨로 표시된 표고를 바탕으로 완성도 및 기타 메타이론을 포함한 뭉친 논리의 종합적인 처리를 제공했다.^[13]

적용들

간섭제어

자원을 통제하기 위한 하부구조체형 이론의 첫 번째 사용에서, 존 C. 레이놀즈는 알골과 같은 프로그래밍 언어의 앨거싱과 다른 형태의 간섭을 제어하기 위해 아핀 타입 이론을 사용하는 방법을 보여주었다.^[14]오헤른은 간섭과 비간섭을 보다 유연하게 혼합할 수 있도록 하여 레이놀즈의 시스템을 확장하기 위해 번치형 이론을 사용했다.^[2]이것은 레이놀즈 시스템의 재귀와 점프에 관한 열린 문제를 해결했다.

분리논리

분리논리는 포인터를 사용하는 변이성 데이터 구조에 대한 추론을 용이하게 하는 호어 논리의 확장이다.Hoare 논리에 따라 분리 논리의 공식은${\displaystyle }${${\displaystyle P}$ r e${\displaystyle }$} ${\displaystyle p}$ r ${\displaystyle o}$ ${\displaystyle o}$ ${\displaystyle \mathrm{ro}}$ m${\displaystyle o}$ ${\displaystyle o}$ ${\displaystyle o}$ t$}$ {\$displaystyle$\{$Pre\}program\$ 형식이다.${Post$하지만 전제조건과 자세는 뭉친 논리의 모델로 해석된다.논리의 원판은 다음과 같은 모델에 기초하였다.

• ${\displaystyle H}$ ${\displaystyle e}$ ${\displaystyle a}$ ${\displaystyle s}$= ${\displaystyle L}$ ${\displaystyle {}_{}}$ f ${\displaystyle {}_{}}$ ${\$위치에서 값으로 부분 함수 완료)
• ${\displaystyle h_{}}$ ${\displaystyle {0\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$= ${\displaystyle h_{0}\display h_{1}=}$ 도메인 중복 시 정의되지 않은, 분리 도메인과의 힙$$ 결합.

분리 사상을 모형화하는 것은 겹치는 무더기에 대한 구성의 정의되지 않은 점이다.이것은 뭉친 논리의 부울 변종 모델이다.

분리논리는 원래 순차프로그램의 속성을 증명하기 위해 사용되었으나, 증명규칙을 사용하여 동시성으로 확장되었다.

${\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}}{\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}$

병렬 스레드로 액세스한 스토리지를 나누는 ^[15]기능

나중에 리소스 의미론의 일반성이 더 크게 활용되었다. 즉, 특정 힙 모델 대신 임의의 부분적 역교환 단노이드에 대해 전제조건과 자세조건이 해석되는 Hoare 3중 배열에 대해 추상적인 버전의 분리논리가 작용한다.^[16]적절한 동시적 단면체의 선택에 의해, 예를 들어, 의존 보증과 추적 기반 추론을 인코딩함으로써 동시적 프로세스를 방해하는 것에 대해 추론하는 데 동시적 분리 논리의 추상적 버전의 증명 규칙을 사용할 수 있다는 것이 놀랍게도 밝혀졌다.^[17][18]

분리논리는 프로그램에 대한 자동 및 반자동 추론을 위한 여러 도구의 기본이며, 현재 페이스북에 구축된 인페어 프로그램 분석기에 사용된다.^[19]

리소스 및 프로세스

헤네시-밀너(Hennessy-Milner)의 관점에서 동시 시스템의 구성 구조를 특징짓는 (모달) 논리를 제공하기 위해 (동기식) 자원 처리 미적분 SCRP와^[4][5][6] 연계하여 번치 논리를 사용해 왔다.

SCRP는 $A{\displaystyle \mathrm{composition}}$ B {\디스플레이 스타일 $A*B}$을(를) 시스템의 병렬 구성과 관련 자원의 구성 측면에서 모두$$ 해석하는 데 주목할 만하다.The semantic clause of SCRP's process logic that corresponds to separation logic's rule for concurrency asserts that a formula ${\displaystyle A*B}$ is true in resource-process state ${\displaystyle R}$, ${\displaystyle E}$ just in case there are decompositions of the resource ${\displaystyle R=S\bullet T$$}$ and process ${\displaystyle E}$ ~ ${\displaystyle F\times G}$, where ~ denotes bisimulation, such that ${\displaystyle A}$ is true in the resource-process state ${\displaystyle S}$, ${\displaystyle F}$ and ${\displaystyle B}$ is true in the resource-process state ${\displaystyle T}$,${\displaystyle G}$ ${\displaystyle$ G$\};$ 즉, $R{\displaystyle ,}$ ${\displaystyle E}$⊨ ${\displaystyle A}$ ${\displaystyle R,E\models$ A$}$ $ifff$, ${\displaystyle F}$ ${\displaystyle \models }$ ${\displaystyle A}$ ${\displaysty$ S$,F\model$ A$}$및 T , $G$ ${\displaystyle ,}$ ${\displaystyle B}${\$displaystyle$ T$,G\models B}$이다$.$

시스템 SCRP는^[4][5][6] 직접 묶인 로직의 자원 의미론 즉, 자원 요소의 순서가 정해진 모노이드에 기초한다.직접적이고 직관적으로 호소력이 있는 반면, 이러한 선택은 특정한 기술적 문제로 이어진다: 헤네시-밀너 완전성 정리는 승법적 함축성과 승법적 양식을 배제한 모달 로직의 단편만을 보유한다.이 문제는 자원-프로세스 미적분학을 두 개의 결합기(한 개는 동시 구성에 해당하고 한 개는 선택에 해당하는 결합기)를 사용하여 결합하는 자원 의미론에 기초하여 해결한다.^[20]

공간 로직

Cardelli, Caires, Gordon 등은 일련의 프로세스 캘커리 로직을 조사했는데, 여기서 접속사는 병렬 구성의 관점에서 해석된다.^{[citation needed]}SCRP에서 Pym 등의 작업과 달리 시스템의 병렬 구성과 시스템이 액세스하는 자원의 구성을 구분하지 않는다.

이들의 로직은 번들 논리의 부울 변종 모델을 발생시키는 자원 의미론의 예에 기초한다.이러한 로직은 부울 번치 논리의 예를 발생시키지만, 그것들은 독립적으로 도착한 것으로 보이며, 어떤 경우든 양식과 바인더의 방식에 있어서 유의미한 추가 구조를 가지고 있다.XML 데이터를 모델링하기 위해 관련 로직도 제안되었다.

참고 항목

• 분리논리
• 관련성 논리
• 선형 논리학

참조