선형 논리

선형 논리(Linear logic)는 장-이브 지라르(Jean-Yves Girard)가 고전 및 직관 논리의 개선으로 제안한 하위 구조 논리로 전자의 쌍대성을 후자의 구성주의적 속성과 결합한다. 논리학도 그 자체로 연구되었지만, 보다 넓게는 선형 논리학의 아이디어가 프로그래밍 언어, 게임 의미론, 양자 물리학, 언어학 같은 분야에 영향을 미쳤다. (선형 논리는 양자 정보 이론 의 논리라고 볼 수 있기 때문이다.)

선형 논리는 다양한 프레젠테이션, 설명 및 직관에 적합하다. 증명 이론상, 그것은 시퀀트 계산의 분석에서 파생된다. 이것은 논리적 추론이 더 이상 계속해서 확장되는 지속적인 "진리"의 모음에 관한 것이 아니라, 마음대로 복제하거나 버릴 수 없는 자원을 조작하는 방법이라는 것을 의미한다. 단순 표시적 의미론 관점에서 선형 논리는 데카르트 닫힌 범주를 대칭 모노이드 범주로 대체하거나 불 대수를 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로 정의할 수 있다.

같이 보기

• 직관 논리

외부 링크

• 위키미디어 공용에 선형 논리 관련 미디어 분류가 있습니다.
• A Linear Logic Prover (llprover) Archived 2016년 4월 4일 - 웨이백 머신, available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan