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

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

고전 선형 논리 (CLL)의 언어는 BNF 표기법에 의해 귀납적으로 정의된다.

A ::= pp
AAAA
A & AAA
1 ∣ 0 ∣ ⊤ ∣ ⊥
!A ∣ ?A

여기서 pp 는 논리적 원자 범위이다. 다음 용어를 추가로 사용할 수 있다.

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
(AB) = AB (AB) = AB
(AB) = A & B (A & B) = AB
(1) = ⊥ (⊥) = 1
(0) = ⊤ (⊤) = 0
(!A) = ?(A) (?A) = !(A)
add mul exp
pos ⊕ 0 ⊗ 1 !
neg & ⊤ ⅋ ⊥ ?

(-)대합이다. 즉, 모든 명제에 대해 A⊥⊥ = A A 선형 부정이라고한다.

표의 열은 극성 이라고 하는 선형 논리의 연결자를 분류하는 또 다른 방법을 제안한다. ⊗, ⊕, 1, 0, !는 positive라고 하고, ⅋, &, ⊥, ⊤, ?는 negative라고 한다.

AB := AB로 정의할 수 있다.

 주석

편집
  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》. 

같이 보기

편집

외부 링크

편집