선형 논리
선형 논리(Linear logic)는 장-이브 지라르(Jean-Yves Girard)가 고전 및 직관 논리의 개선으로 제안한 하위 구조 논리로 전자의 쌍대성을 후자의 구성주의적 속성과 결합한다.[1] 논리학도 그 자체로 연구되었지만, 보다 넓게는 선형 논리학의 아이디어가 프로그래밍 언어, 게임 의미론, 양자 물리학, 언어학 같은 분야에 영향을 미쳤다. (선형 논리는 양자 정보 이론 의 논리라고 볼 수 있기 때문이다.)[2]
선형 논리는 다양한 프레젠테이션, 설명 및 직관에 적합하다. 증명 이론상, 그것은 시퀀트 계산의 분석에서 파생된다. 이것은 논리적 추론이 더 이상 계속해서 확장되는 지속적인 "진리"의 모음에 관한 것이 아니라, 마음대로 복제하거나 버릴 수 없는 자원을 조작하는 방법이라는 것을 의미한다. 단순 표시적 의미론 관점에서 선형 논리는 데카르트 닫힌 범주를 대칭 모노이드 범주로 대체하거나 불 대수를 C*-대수로 대체하여 고전 논리의 해석을 개선하는 것으로 볼 수 있다.
고전 선형 논리 (CLL)의 언어는 BNF 표기법에 의해 귀납적으로 정의된다.
| A | ::= | p ∣ p⊥ |
| ∣ | A ⊗ A ∣ A ⊕ A | |
| ∣ | A & A ∣ A ⅋ A | |
| ∣ | 1 ∣ 0 ∣ ⊤ ∣ ⊥ | |
| ∣ | !A ∣ ?A |
여기서 p 및 p⊥ 는 논리적 원자 범위이다. 다음 용어를 추가로 사용할 수 있다.
| Symbol | Name | ||
|---|---|---|---|
| ⊗ | multiplicative conjunction | times | tensor |
| ⊕ | additive disjunction | plus | |
| & | additive conjunction | with | |
| ⅋ | multiplicative disjunction | par | |
| ! | of course | bang | |
| ? | why not | ||
이항 접속사 ⊗, ⊕, & 및 ⅋는 결합 및 교환 가능하다. 1은 ⊗의 단위, 0은 ⊕의 단위, ⊥는 ⅋의 단위, ⊤는 &의 단위이다.
CLL의 모든 명제 A에는 다음과 같이 정의된 A⊥가 있다.
| (p)⊥ = p⊥ | (p⊥)⊥ = p | ||||
| (A ⊗ B)⊥ = A⊥ ⅋ B⊥ | (A ⅋ B)⊥ = A⊥ ⊗ B⊥ | ||||
| (A ⊕ B)⊥ = A⊥ & B⊥ | (A & B)⊥ = A⊥ ⊕ B⊥ | ||||
| (1)⊥ = ⊥ | (⊥)⊥ = 1 | ||||
| (0)⊥ = ⊤ | (⊤)⊥ = 0 | ||||
| (!A)⊥ = ?(A⊥) | (?A)⊥ = !(A⊥) |
| add | mul | exp | |
|---|---|---|---|
| pos | ⊕ 0 | ⊗ 1 | ! |
| neg | & ⊤ | ⅋ ⊥ | ? |
(-)⊥ 는 대합이다. 즉, 모든 명제에 대해 A⊥⊥ = A A⊥ 선형 부정이라고한다.
표의 열은 극성 이라고 하는 선형 논리의 연결자를 분류하는 또 다른 방법을 제안한다. ⊗, ⊕, 1, 0, !는 positive라고 하고, ⅋, &, ⊥, ⊤, ?는 negative라고 한다.
A ⊸ B := A⊥ ⅋ B로 정의할 수 있다.
주석 편집
- ↑ Girard, Jean-Yves (1987). “Linear logic” (PDF). 《Theoretical Computer Science》 50 (1): 1–102. doi:10.1016/0304-3975(87)90045-4.
- ↑ Baez, John; Stay, Mike (2008). Bob Coecke, 편집. “Physics, Topology, Logic and Computation: A Rosetta Stone” (PDF). 《New Structures of Physics》.
외부 링크 편집
위키미디어 공용에 선형 논리 관련 미디어 분류가 있습니다.- A Linear Logic Prover (llprover) Archived 2016년 4월 4일 - 웨이백 머신, available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan
