‘쿠폰 한 장이 있으면 음료 한 잔을 받을 수 있다’는 전제에서 음료 두 잔을 얻어도 될까요? 일상 명제처럼 쿠폰 전제를 두 번 복사하면 그렇게 보일 수 있습니다. Jean-Yves Girard의 선형논리는 전제가 증명 과정에서 몇 번 쓰이는지 추적합니다. 전제를 마음대로 버리거나 복제하는 구조 규칙을 기본값으로 두지 않아, 정보뿐 아니라 자원·행동·상태 변화를 논리식 안에 드러낼 수 있습니다.
연구를 읽는 두 가지 질문
왜 전제의 복사와 폐기를 따로 표시하는가?
Girard는 고전논리와 직관주의 논리에서 암묵적으로 허용되는 수축과 약화 규칙을 분리합니다. 수축은 같은 전제를 여러 번 쓸 수 있게 하고, 약화는 전제를 쓰지 않고 버릴 수 있게 합니다. 선형논리의 기본 연결사는 이러한 복제·폐기를 자동 허용하지 않습니다. 필요할 때는 ‘!’ 지수로 다시 쓸 수 있는 자원임을 표시합니다. 이 구분은 같은 문장이라도 일회성 표, 반복 가능한 규칙, 반드시 소비해야 하는 의무가 서로 다른 추론 행동을 가진다는 점을 보여 줍니다. [1]
자원 해석은 비유일 뿐인가?
원 논문은 선형 부정, 곱셈적·덧셈적 연결사, 지수, 위상 의미론과 코히어런스 공간 등 완전한 형식 체계를 제시합니다. 자원 해석은 이 체계를 이해하는 강력한 관점이지만 선형논리의 모든 수학적 의미를 물건 소비 하나로 환원할 수는 없습니다. 또한 실제 프로그램이나 업무 절차가 선형논리 공식을 정확히 따르는지는 별도 형식화가 필요합니다. 이 글은 일회성 전제와 재사용 전제의 차이에 초점을 좁힙니다. [1]
행사 쿠폰과 반복 규칙
LTCT 가상 행사에서 쿠폰 3장은 음료 3잔으로 바꿀 수 있습니다. ‘쿠폰 하나를 음료 하나로’라는 교환 규칙은 여러 참가자에게 반복 적용할 수 있지만, 개별 쿠폰은 한 번 교환하면 사라집니다.
아래 활동에서 보유 쿠폰 수와 교환 횟수, 재사용 허용 여부를 바꾸면 남은 자원과 규칙 위반이 달라집니다. 수치는 원 논문의 실험값이 아니라 선형 사용을 설명하는 가상 장부입니다.
학생은 각 증명 줄 옆에 소비한 전제와 남은 전제를 씁니다. 같은 쿠폰을 두 줄에서 사용했다면 결론의 내용이 그럴듯해도 증명 장부는 실패합니다.
반복 가능한 교환 규칙과 일회성 쿠폰을 같은 상자에 넣지 않습니다. 무엇을 ‘!’로 표시할지 토론하면 규칙과 사례, 유형과 토큰을 구분하는 연습이 됩니다.
쿠폰 수와 교환 횟수를 바꾸어 자원 장부를 확인해 보세요
쿠폰은 일회성 자원, 교환 규칙은 반복 가능한 규칙인 교육용 장부입니다.
| 지급 음료 | 남은 쿠폰 | 중복 사용 |
|---|---|---|
| 2 | 1 | 아니요 |
현재 장부의 사용 횟수가 가정과 맞습니다.
어디까지 말할 수 있을까요?
- 자원 비유만으로 선형논리의 모든 연결사와 의미론을 설명할 수 없습니다.
- 현실의 자원은 분할·대체·시간 변화가 있어 별도 모형이 필요합니다.
- 재사용 가능 표시가 실제 제도에서 무제한 사용을 정당화하는 것은 아닙니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
한 번 쓰면 사라지는 자원 카드와 여러 번 사용할 수 있다고 명시한 규칙 카드를 구분합니다. 학생은 목표를 만들 때 사용한 자원과 남은 자원을 줄마다 장부에 적습니다.
같은 자원을 두 번 쓴 풀이와 사용 횟수를 지킨 풀이를 비교합니다. 교사는 결론의 모양만 보지 않고 각 단계의 자원 사용이 주어진 규칙과 맞는지 설명하게 합니다.
수학 정리도 한 번 쓰면 사라지나요?
생각을 비교할 해설 펼치기
보통 수학 정리는 재사용 가능한 규칙으로 다룹니다. 선형논리는 모든 전제가 사라진다고 말하는 것이 아니라, 무엇이 재사용 가능한지 명시하게 합니다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
선형논리 (Linear Logic)
Jean-Yves Girard (1987). Theoretical Computer Science, 50(1), 1–101.
- 자료 성격
- 동료심사 학술지 논문 · 출판사 본문
- 읽은 버전
- 1987년 출판본
- 확인 범위
- 출판사 본문의 초록과 논문 전문에서 구조 규칙의 분해, 지수, 선형 부정과 자원 해석의 형식적 범위를 확인
- 원문 확인일
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준
같은 연구 흐름에서 이어 읽기
같은 원문, 저자·연구 흐름, 공통 개념 태그를 기준으로 연결한 관련 해설입니다.