선형 논리

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요
2. 선형 결합 기호
3. 선형 논리의 변종
4. 다른 증명 시스템
- 4.1. 증명망 (Proof nets)
5. 의미론 (Semantics)
- 5.1. 대수적 의미론 (Algebraic semantics)
6. 함의 관계의 결정 가능성/복잡도
참조

1. 개요

선형 논리는 전통적인 논리 체계와 달리 자원(resource)의 개념을 도입하여, 자원의 소비와 생성을 명시적으로 다루는 논리 체계이다. 곱(multiplicative)과 가법(additive)의 개념을 통해 논리 결합자를 재해석하며, 자동판매기 예시를 통해 직관적인 이해를 돕는다. 선형 논리는 다양한 변종을 가지며, 고전 선형 논리(CLL), 직관 선형 논리(ILL) 등이 있다. 선형 논리의 변종들은 구조 규칙의 허용 여부에 따라 아핀 논리, 엄격한 논리 등으로 나뉜다. 선형 논리는 시퀀트 계산, 증명망 등의 시스템으로 정의되며, 콴탈을 이용한 대수적 의미론을 갖는다. 선형 논리의 함의 관계는 논리 체계에 따라 결정 가능성 및 복잡도가 다르다.

2. 선형 결합 기호

선형 논리에서는 기존 논리 결합 기호의 의미를 재해석하고, 자원의 제약과 흐름을 명확하게 나타내기 위해 새로운 결합 기호를 도입한다. 각 결합 기호는 곱셈적인 것과 덧셈적인 것으로 나뉘며, 각각 동시적 발생과 택일적 발생에 대응한다.

연결사의 분류
	덧셈	곱셈	지수
양수	⊕, 0	⊗, 1	!
음수	&, ⊤	⅋, ⊥	?

곱셈 결합 기호 (Multiplicatives): 자원의 동시적, 병행적 발생을 나타낸다. (⊗, ⅋, 1, ⊥)
덧셈 결합 기호 (Additives): 자원의 택일적 발생을 나타낸다. (&, ⊕, ⊤, 0)
지수 결합 기호 (Exponentials): 일반 논리와 선형 논리의 연결. (!, ?)

각 결합 기호에 대한 자세한 내용은 하위 섹션을 참고할 수 있다.

2. 1. 곱셈 결합 기호 (Multiplicatives)

곱셈 결합 기호(⊗, ⅋, 1, ⊥)는 선형 논리에서 자원의 동시적, 병행적 발생을 나타낸다. 자동판매기를 예로 들면, 여러 물품을 동시에 구매하는 상황에 대응된다.^[6] 곱셈 논리곱(⊗)과 곱셈 논리합(⅋)은 결합 법칙과 교환 법칙을 따르며, 1은 ⊗에 대한 단위원이고, ⊥은 ⅋에 대한 단위원이다.^[6] 곱셈 결합과 분리에 대한 규칙은 고전적 해석 하에서 일반적인 ''결합'' 및 ''분리''에 대해 허용 가능하며, LK에서 허용되는 규칙과 같다.

2. 1. 1. 곱셈 논리곱 (Tensor, ⊗)

곱셈 논리곱(⊗)은 소비자가 사용할 수 있는 자원이 동시에 발생함을 나타낸다. 예를 들어, 껌 한 개와 청량음료 한 병을 모두 구매하는 것은 로 표현할 수 있다.^[6]

이진 연결사 ⊗는 결합 법칙과 교환 법칙을 만족한다. 1은 ⊗에 대한 단위원인데, 이는 아무런 자원이 없음을 의미한다.^[6]

2. 1. 2. 곱셈 논리합 (Par, ⅋)

곱셈 논리합(⅋, par)은 공급자(기계) 측에서 제어하는 자원의 동시 발생을 나타낸다. 예를 들어 자동판매기에서 특정 버튼을 누르면 껌과 음료수가 동시에 나오는 경우(gum ⅋ drink)를 생각해 볼 수 있다. 곱셈 논리곱(⊗)과 달리, 순서가 중요할 수 있다. (예: 커피와 컵의 순서)^[6]

곱셈 논리합은 결합 법칙과 교환 법칙이 성립한다. 단위 원소 ⊥(바텀)은 빈 골을 의미한다.^[6]

2. 2. 덧셈 결합 기호 (Additives)

덧셈 결합은 자원의 택일적 발생을 나타낸다. 예를 들어 자동판매기에서 여러 물품 중 하나를 선택하는 상황에 대응된다.^[6] 덧셈 결합에는 덧셈 논리곱(&, with)과 덧셈 논리합(⊕, plus)이 있다.

2. 2. 1. 덧셈 논리곱 (With, &)

덧셈 논리곱(&, with)은 소비자가 제어하는 자원의 택일적 발생을 나타낸다. 예를 들어 자동 판매기에서 칩 한 봉지, 사탕 한 개, 청량음료 한 캔이 각각 1달러일 때, 이 제품 중 정확히 하나를 1달러에 살 수 있다. 이를 선형 논리로 표현하면 이다.^[6]

라고 쓰지 않는 이유는 1달러로 세 가지 제품을 모두 살 수 있다는 의미가 되기 때문이다. 그러나 에서 를 올바르게 추론할 수 있다. 여기서 이다.^[6]

덧셈적 결합(&)은 결합 법칙과 교환 법칙을 따른다. 덧셈적 결합의 단위원 ⊤ (톱)은 선택지가 없거나 선택할 수 없음을 의미하며, 불필요한 자원을 위한 쓰레기통으로 볼 수 있다. 예를 들어 를 써서 3달러로 사탕 한 개와 다른 물건(칩과 음료, 또는 2달러, 또는 1달러와 칩 등)을 얻을 수 있다는 것을 더 구체적으로 명시하지 않고 표현할 수 있다.^[6]

2. 2. 2. 덧셈 논리합 (Plus, ⊕)

덧셈 논리합(plus, ⊕)은 공급자(기계) 측에서 제어하는 자원의 택일적 발생을 나타낸다. 예를 들어 자동판매기에 1달러를 넣으면 사탕, 칩, 음료수 중 하나가 나오는 경우를 로 표현할 수 있다.^[6] ⊕는 결합 법칙과 교환 법칙을 만족한다. 0은 아무것도 출력되지 않는 상황을 의미하며, ⊕의 단위 원소이다. 즉, A 또는 0을 생성할 수 있는 기계는 0을 생성하는 데 실패하더라도 항상 A를 생성하는 기계만큼은 좋다.^[6]

2. 3. 지수 결합 기호 (Exponentials)

지수 결합 기호(Exponentials)는 일반적인 논리(무제한 재사용 가능)와 선형 논리(제한된 사용)를 연결하는 역할을 한다. 선형 논리에서 지수 결합 기호는 "!" (물론, bang)와 "?" (왜 안 돼, quest) 두 가지가 있다.^[5]

! (물론, bang): 명제 앞에 붙어 해당 명제가 여러 번 사용될 수 있음을 나타낸다. 즉, 자원으로서 무제한 복제 및 사용이 가능하다는 의미이다.
? (왜 안 돼, quest): 명제 앞에 붙어 해당 명제가 약화(weakening)될 수 있음을 나타낸다. 즉, 자원으로서 필수가 아니며, 다른 것으로 대체되거나 추가될 수 있다는 의미이다.

지수 결합 기호는 약화와 축약 규칙을 제어하여, 자원의 사용을 명시적으로 관리한다.

지수 동형성에 관한 식은 다음과 같다.

다음은 등식이 아니고 함의 관계만 있는 분배 공식이다.

2. 3. 1. 물론 (Of course, !)

'물론'(!)은 약화(weakening)와 축약(contraction)을 제어하여 접근할 수 있게 해주는 지수 연산자이다. 구체적으로, !가 붙은 명제에 대한 약화 및 축약의 구조 규칙을 추가한다.^[5]

{| class="wikitable"

|-

| style="text-align: center;" |

style="border-top:2px solid black;" |

| width="50" |

| style="text-align: center;" |

style="border-top:2px solid black;" |

|}

그리고 다음 논리 규칙을 사용한다. 여기서 는 각 명제 앞에 ?가 붙은 명제의 목록을 나타낸다.

{| class="wikitable"

|-

| style="text-align: center;" |

style="border-top:2px solid black;" |

| width="50" |

| style="text-align: center;" |

style="border-top:2px solid black;" |

|}

지수에 대한 규칙은 시퀀트 계산 형식화에서 정규 양상 논리 S4와 유사하게 양상 논리(modalities)를 관리하는 추론 규칙의 패턴을 따르는데, 이는 다른 연결사(connectives)에 대한 규칙과는 다르다. 이중 명제 !와 ? 사이에는 더 이상 명확한 대칭이 없다.

지수 연산자를 통해 공식을 필요에 따라 여러 번 사용할 수 있도록 하여, 직관적 함의와 고전적 함의를 선형 함의에서 복구할 수 있다. 직관적 함의는 로 인코딩되는 반면, 고전적 함의는 또는 (또는 다양한 대체 번역)로 인코딩될 수 있다.^[7]

2. 3. 2. 왜 안 돼 (Why not, ?)

Why not, ?^영어는 선형 논리에서 사용되는 연결사 중 하나로, '왜 안 돼'라고 불린다. 기호는 물음표(?)를 사용한다. 이 연결사는 주어진 명제에 임의의 추가적인 귀결을 포함시켜 약화(weakening)시키는 역할을 한다. 예를 들어, 명제 A에 ?를 붙여 ?A를 만들면, A뿐만 아니라 다른 어떤 명제도 함께 성립할 수 있다는 의미가 된다. 이는 자원 해석 관점에서 보면, ?A는 A라는 자원을 반드시 사용해야 하는 것은 아니고, 필요에 따라 다른 자원으로 대체하거나 추가할 수 있음을 의미한다.

2. 4. 선형 함의 (Linear implication, Lolli, ⊸)

선형 함의(⊸)는 자원 A를 소비하여 자원 B를 생성하는 것을 의미한다. Linear implication^영어 기호 ⊸는 그 모양 때문에 "롤리팝"이라고도 불린다.^[6] 예를 들어, 동전 파쇄기의 작동은 penny^영어 ⊸ smashed penny^영어 (동전 ⊸ 찌그러진 동전)로 나타낼 수 있다.^[7]

3. 선형 논리의 변종

선형 논리는 구조 규칙(약화, 축약, 교환)의 허용 여부에 따라 다양한 변종으로 나뉜다.

아핀 논리: 수축은 금지하지만 전역 약화는 허용한다.
엄격한 논리 또는 관련 논리: 약화는 금지하지만 전역 수축은 허용한다.
비가환 논리 또는 순서 논리: 약화와 수축을 금지하는 것 외에 교환 규칙을 제거한다. 순서 논리에서 선형 함축은 왼쪽 함축과 오른쪽 함축으로 더 나뉜다.

이 외에도, 특정 결합자의 유무, 다루는 논리의 복잡성에 따라 다양한 변종이 존재한다. 예를 들어 직관주의적 선형 논리(ILL)에서는 연결사 ⅋, ⊥, ?가 없으며, 선형 함의가 기본 연결사로 처리된다. 반면, 전체 직관주의적 선형 논리(FILL)에서는 이러한 연결사들이 모두 존재한다.

선형 논리는 1차 및 고차 확장도 가능하다(1차 논리, 고차 논리 참조).

3. 1. 고전 선형 논리 (Classical Linear Logic, CLL)

지라르(Girard)가 처음 제안한 선형 논리이다. 고전 선형 논리(CLL)에서는 모든 결합자에 쌍대가 존재한다.

다음은 CLL을 시퀀트 계산으로 나타낸 것이다.

증명은 모두 컷 규칙을 사용하지 않는 형태로 변환할 수 있다.^[4]

선형 함의는 이 표에 나타나 있지 않지만, 선형 부정과 곱셈 논리곱을 사용하면 CLL에서도 ''A'' ⊸ ''B'' ≡ ''A''^⊥ ⅋ ''B''로 정의할 수 있다. 이는 고전 논리에서 익숙한 형태이다. 예를 들어, 일반적인 함의 ⇒는 ''A'' ⇒ ''B'' ≡ ?''A''^⊥ ⅋ ''B''로 정의할 수 있다.

이러한 정의에는 "선형 부정" 표기법이 필요하지만, 고전 논리에서는 쌍대를 사용할 수도 있다. ''A''의 쌍대는 ''A''^⊥로 표기되며, 다음과 같이 정의된다.

(A ⊗ B)^⊥	=	A^⊥ ⅋ B^⊥
(A & B)^⊥	=	A^⊥ ⊕ B^⊥
(A ⊕ B)^⊥	=	A^⊥ & B^⊥
(A ⅋ B)^⊥	=	A^⊥ ⊗ B^⊥

논리 단위원도 유사한 쌍대를 가진다. 예를 들어, ⊤^⊥ = 0이며, !와 ?는 쌍대이다. 쌍대 규칙은 어떤 항을 한쪽 변에서 다른 쪽으로 옮길 경우, 그 쌍대로 변환된다는 것이다.

3. 2. 직관 선형 논리 (Intuitionistic Linear Logic, ILL)

직관 선형 논리(ILL)는 귀결이 하나뿐인 단일 결론 시퀀트 계산을 기반으로 한다. 고전 선형 논리(CLL)와 달리, ILL의 결합자에는 완전한 쌍대성이 없다. 실제로 ⅋ (par), ? (why not) 연산자와 명제 상수 "⊥"(바닥)은 도입 규칙의 귀결이 여러 개 필요하기 때문에 ILL에는 존재하지 않는다. 결과적으로, ILL에서는 선형 함의가 기본적인 결합자가 된다.

3. 3. 곱셈 선형 논리 (Multiplicative Linear Logic, MLL)

곱셈 선형 논리(Multiplicative Linear Logic, MLL)는 곱셈 결합자와 그 단위 원소만 허용하는 선형 논리의 변종이다. MLL의 결정 문제는 NP-완전이다.^[10]

MLL은 곱셈 연결사(⊗)와 분리(⅋)만을 사용한다. 이들에 대한 규칙은 다음과 같다.

{| class="wikitable"

|-

|


Γ, A			Δ, B
colspan="4" style="border-top:2px solid black;" \|
Γ, Δ, A ⊗ B

|


Γ, A, B
style="border-top:2px solid black;" \|
Γ, A ⅋ B

|}

단위(1과 ⊥)에 대한 규칙은 다음과 같다.

{| class="wikitable"

|-

|



style="border-top:2px solid black;" \|
1

|


Γ
style="border-top:2px solid black;" \|
Γ, ⊥

|}

곱셈 결합과 분리에 대한 규칙은 고전적 해석 하에서 일반적인 ''결합'' 및 ''분리''에 대해 허용 가능하다. 즉, 이는 LK에서 허용되는 규칙이다.

MLL의 함의는 순수 함축적 부분에서 혼 규칙으로 제한하거나,^[9] 원자 없는 공식으로 제한하더라도 NP-완전이다.^[10]

3. 4. 곱셈-덧셈 선형 논리 (Multiplicative-Additive Linear Logic, MALL)

곱셈-덧셈 선형 논리(MALL)는 곱셈 선형 논리(MLL)에 덧셈 결합자를 추가한 것이다. 덧셈 결합자에는 논리곱(&)과 논리합(⊕)이 있다.^[8]

덧셈 결합(&)과 논리합(⊕)에 대한 규칙은 다음과 같다.

{| class="wikitable"

|-

|


colspan="4" style="border-top: 2px solid black;" \|
colspan="4" align="center" \|

|

style="border-top: 2px solid black;" |

|

style="border-top: 2px solid black;" |

|}

단위에 대한 규칙은 다음과 같다.

{| class="wikitable"

|-

|

colspan="4" style="border-top: 2px solid black;" |

colspan="4" align="center" |

| (||에 대한 규칙 없음)

|}

곱셈 연결사(⊗)의 경우, 결론의 맥락은 전제들 사이에서 분할되는 반면, 덧셈 연결사(&)의 경우 결론의 맥락은 전체가 두 전제로 전달된다.

MALL의 결정 문제는 PSPACE-완전이다.^[8]

3. 5. 곱셈-지수 선형 논리 (Multiplicative-Exponential Linear Logic, MELL)

곱셈-지수 선형 논리(Multiplicative-Exponential Linear Logic, MELL)는 곱셈 선형 논리(MLL)에 지수 결합자를 추가한 것이다. MELL의 결정 가능성 문제는 오랫동안 풀리지 않은 문제였으나, 최근 결정 불가능하다는 주장이 제기되었다.^[11] 2015년에 결정 가능성 증명이 ''이론 전산 과학''에 게재되기도 했지만,^[12] 후에 오류가 있는 것으로 밝혀졌다.^[13]

지수(Exponentials)는 약화(weakening)와 축약(contraction)에 대한 제어된 접근을 제공한다. 구체적으로, ?가 붙은 명제에 대해 약화 및 축약의 구조 규칙을 추가한다.^[5]

그리고 다음 논리 규칙을 사용한다. 여기서 ?Γ는 각 명제 앞에 ?가 붙은 명제의 목록을 나타낸다.

지수에 대한 규칙은 시퀀트 계산 형식화에서 양상 논리(modalities)를 관리하는 추론 규칙, 즉 정규 양상 논리 S4와 유사하게 다른 연결사(connectives)에 대한 규칙과 다른 패턴을 따른다. 이중 명제 !와 ? 사이에는 더 이상 명확한 대칭이 없다.

3. 6. 곱셈-덧셈-지수 선형 논리 (Multiplicative-Additive-Exponential Linear Logic, MAELL)

곱셈-덧셈-지수 선형 논리(MAELL)는 선형 논리의 모든 결합자를 포함하는 변형이다. MAELL의 함의 관계는 결정 불가능하다.^[8] MAELL은 곱셈-지수 선형 논리(MELL)에 덧셈 결합자를 추가한 논리 체계이다.

3. 7. 완전 직관 선형 논리 (Full Intuitionistic Linear Logic, FILL)

완전 직관 선형 논리(Full Intuitionistic Linear Logic, FILL)는 곱셈 결합자인 텐서(tensor), 파(par)와 선형 함의를 허용한다. 이는 논리곱, 논리합, 함의가 있다는 것을 의미하며, 직관 논리에 가깝다.

3. 8. 기타 부분 구조 논리

아핀 논리: 약화를 허용하는 선형 논리의 확장이다. 1과 는 아핀 논리에서 구별되지 않는다.^[14]
적절성 논리: 축약을 허용하는 선형 논리의 확장이다.
비가환 논리: 선형 논리에서 교환 규칙(전치)을 제거한 것이다. 곱셈 논리곱은 두 개(''left fuse''와 ''right fuse'')로 나뉜다.

4. 다른 증명 시스템

장-이브 지라르가 도입한 증명망은 논리적 관점에서는 다르지만 "도덕적" 관점에서는 그렇지 않은 모든 것들, 즉 ''관료주의''를 피하기 위해 만들어졌다.

예를 들어, 아래 두 증명은 "도덕적으로" 동일하다.

{| class="wikitable" style="margin:auto"

|-

| style="text-align: center;" |

style="border-top:2px solid black;" |

| style="text-align: center;" |

style="border-top:2px solid black;" |

|}

증명망의 목표는 이들을 그래픽 표현을 생성하여 동일하게 만드는 것이다.

4. 1. 증명망 (Proof nets)

장-이브 지라르가 도입한 증명망은 논리적 관점에서는 다르지만 "도덕적" 관점에서는 그렇지 않은 모든 것들, 즉 ''관료주의''를 피하기 위해 만들어졌다.

예를 들어, 다음 두 증명은 "도덕적으로" 동일하다.

{| class="wikitable" style="margin:auto"

|-

| style="text-align: center;" |

style="border-top:2px solid black;" |

| style="text-align: center;" |

style="border-top:2px solid black;" |

|}

증명망의 목표는 이들을 그래픽 표현을 생성하여 동일하게 만드는 것이다.

5. 의미론 (Semantics)

의미론 부분은 내용 보강이 필요하다.

5. 1. 대수적 의미론 (Algebraic semantics)

콴탈(Quantale^영어)

6. 함의 관계의 결정 가능성/복잡도

전체 CLL에서의 함의 관계는 결정 불가능하다.^[8] CLL의 일부분을 고려할 때, 결정 문제는 다양한 복잡성을 가진다.

곱셈 선형 논리(MLL): 곱셈 연결사만 사용. MLL 함의는 순수 함축적 부분에서 혼 규칙으로 제한하더라도^[9], 혹은 원자 없는 공식으로 제한하더라도 NP-완전이다.^[10]
곱셈-덧셈 선형 논리(MALL): 곱셈과 덧셈 연결사만 사용(즉, 지수 없음). MALL 함의는 PSPACE-완전이다.^[8]
곱셈-지수 선형 논리(MELL): 곱셈과 지수 연결사만 사용. 페트리 망의 도달 가능성 문제로부터의 환원을 통해^[11], MELL 함의는 최소한 EXPSPACE-어렵다가 되어야 하지만, 결정 가능성 자체는 오랫동안 해결되지 않은 문제였다. 2015년, 결정 가능성 증명이 저널 ''이론 전산 과학''에 게재되었지만,^[12] 나중에 오류가 있는 것으로 밝혀졌다.^[13]
약화를 가진 선형 논리인 아핀 선형 논리(부분이 아닌 확장)는 1995년에 결정 가능함이 밝혀졌다.^[14]

참조

_[1] 학술지 Linear logic http://girard.perso.[...]
_[2] 학술지 Physics, Topology, Logic and Computation: A Rosetta Stone http://math.ucr.edu/[...]
_[3] 학술지 Dagstuhl Seminar 99341 on Linear Logic and Applications http://www.dagstuhl.[...] Schloss Dagstuhl – Leibniz-Zentrum für Informatik
_[4] 문서 Girard (1987), p.22, Def.1.15
_[5] 문서 Girard (1987), p.25-26, Def.1.21
_[6] 문서 J. [[Robin Cockett]] and Robert Seely "Weakly distributive categories" [[Journal of Pure and Applied Algebra]] 114(2) 133-173, 1997
_[7] 문서 Di Cosmo, Roberto. ''[http://www.dicosmo.org/CourseNotes/LinLog/ The Linear Logic Primer]''. Course notes; chapter 2.
_[8] 학술지 Decision Problems for Propositional Linear Logic
_[9] 학회자료 Horn programming in linear logic is NP-complete 1992-06-22
_[10] 학술지 Constant-only multiplicative linear logic is NP-complete
_[11] 기술보고서 Nets as Tensor Theories http://seclab.illino[...]
_[12] 학술지 The decidability of the intensional fragment of classical linear logic 2015-09-13
_[13] 학술지 On the decision problem for MELL 2019-05-10
_[14] 학회자료 Decidability of linear affine logic 1995-06-01
_[15] 학술지 Linear logic http://girard.perso.[...]
_[16] 학술지 Physics, Topology, Logic and Computation: A Rosetta Stone http://math.ucr.edu/[...]

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com