선형 논리

선형 논리(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로 정의할 수 있다.

 주석

  1. ↑ Girard, Jean-Yves (1987). “Linear logic” (PDF). 《Theoretical Computer Science》 50 (1): 1–102. doi:10.1016/0304-3975(87)90045-4. 
  2. ↑ Baez, John; Stay, Mike (2008). Bob Coecke, 편집. “Physics, Topology, Logic and Computation: A Rosetta Stone” (PDF). 《New Structures of Physics》. 

같이 보기

외부 링크