맞는 답을, 감당할 수 있는 계산으로
정확성과 계산량을 구별하고, 입력의 크기가 바뀔 때 무엇을 비교할지 정합니다.
지난 편에서는 전제를 다시 쓰는 법을 배웠습니다. 이번에는 왜 계산시간을 묻나요?
정답을 내는 방법을 안다는 것과, 입력이 커져도 그 방법을 끝까지 실행할 수 있다는 것은 서로 다른 질문입니다. 명단에서 특정한 조건을 만족하는 사람이 있는지 확인하는 일을 생각해 보세요. 한 사람씩 한 번 살펴보면 되는 방법이 있습니다. 같은 명단을 여러 차례 다시 살펴보는 불필요한 절차를 넣어도 마지막 답은 같을 수 있습니다. 두 방법이 같은 답을 내더라도 입력이 늘어날 때 해야 할 일의 양은 크게 달라질 수 있습니다.
증명을 프로그램처럼 읽을 때도 계산량을 물을 수 있습니다. 중간 결론을 만드는 증명과 그것을 사용하는 증명을 연결한 뒤, 그 연결을 정리하는 과정이 계산에 대응합니다. 이때 특히 눈여겨볼 곳이 한 계산을 여러 곳에서 다시 사용하도록 만드는 규칙입니다. 복사가 겹치면 처음에 짧아 보이던 표현이 큰 계산으로 펼쳐질 수 있기 때문입니다.
정답 조건
결과가 요구한 조건을 만족하는가?
계산량 조건
입력이 커질 때 해야 할 일은 얼마나 늘어나는가?
정답의 조건과 계산량의 조건을 각각 확인합니다.
이 논문은 그 사이에 들어갈 논리를 찾습니다. 계산을 풍부하게 표현하면서도, 정해진 방식으로 만든 프로그램에는 계산량의 상한을 줄 수 있는 체계입니다. 1회에서 배운 자원 사용을 이제 계산을 얼마나 늘리는 사용인가라는 관점에서 읽게 됩니다.
‘다항시간’이라는 말부터 막힙니다. 무엇이 다항식처럼 늘어난다는 뜻인가요?
먼저 n을 실제로 입력된 자료의 길이라고 정하겠습니다. 비트문자열이라면 비트의 개수입니다. T(n)은 길이가 n인 모든 입력 가운데 가장 많은 연산이 필요한 경우의 연산 수입니다. 충분히 큰 입력에서 T(n) ≤ c·nd처럼 묶을 수 있고, 상수 c와 차수 d가 입력 길이에 따라 바뀌지 않으면 다항시간이라고 부릅니다.
한 항목마다 한 번 일하는 모형은 n, 각 항목을 다시 모든 항목과 대조하는 두 겹 반복 모형은 n²입니다. 매번 두 갈래를 고르는 길이 n의 선택에서 완성된 경로마다 한 번 일하면 2ⁿ번입니다. 아래에서 입력 길이를 바꾸어 보세요.
세 값의 단위는 ‘모형의 연산 수’입니다. 실제 프로그램의 실행 시간이나 이 논문의 정규화 단계 수를 측정한 값이 아닙니다. 막대는 가장 큰 값에 대한 정확한 비율이며, 작은 값의 막대를 인위적으로 늘리지 않습니다.
‘다항시간’은 특정 입력에서 항상 즉시 끝난다는 약속도 아닙니다. 차수와 계수가 크면 실제 비용이 큽니다. 여기서 얻으려는 것은 우선 입력이 늘어날 때의 증가 방식에 대한 증명입니다. 같은 프로그램을 놓고 입력 길이만 늘려야 이 비교가 의미를 갖습니다.
느낌표 !가 재사용의 허가라면, 그 표시만 잘 붙여도 계산량이 조절되는 것 아닌가요?
느낌표는 재사용이 가능한 자원을 구별하는 데 중요한 역할을 합니다. 여기에 어떤 규칙으로 그 자원을 꺼내고, 나누고, 다시 포장하는가라는 질문이 더해집니다. 같은 허가 표시가 있어도 사용 규칙의 조합에 따라 계산의 크기가 달라질 수 있습니다.
두 갈래로 나누는 장치만 생각해 봅시다. 한 층이면 두 갈래지만, 그 작업을 각 갈래 안에서 반복하면 네 갈래, 여덟 갈래가 됩니다. ‘매번 두 번만 복사한다’는 말만으로는 전체 계산량을 알 수 없습니다. 그 복제가 몇 층으로 겹치는지도 보아야 합니다.
앞선 연구들은 이 문제에 여러 방식으로 접근했습니다. 바운디드 선형논리는 다항식 정보를 타입에 드러내고, 라이트 선형논리는 느낌표와 관련된 규칙을 세심하게 바꿉니다. 라퐁은 익숙한 논리식 언어를 유지하면서 규칙을 간결하게 제한하는 길을 제안합니다. 그것이 이 논문의 소프트 선형논리입니다. 이름의 ‘소프트’가 계산 속도 측정값을 뜻하는 것은 아닙니다.
복제의 규칙에 비용을 붙이다
사용 횟수와 상자의 깊이를 구별하며, 펼쳐지는 계산을 세는 가중치를 만납니다.
그러면 !A를 쓰는 규칙을 어떻게 바꾸나요? 몇 번 쓰는지 눈으로 보여 주세요.
원문은 멀티플렉싱(multiplexing)이라는 규칙을 사용합니다. 여기서는 ‘여러 사용처로 분배하기’라고 읽겠습니다. 어떤 결론 C를 만드는 데 A가 k개 필요하다고 합시다. 그 사용처들을 하나의 !A 가정으로 묶는 규칙입니다. k는 그 규칙을 적용하는 자리에서 정하는 자연수입니다.
Γ는 함께 쓰는 나머지 가정들의 목록이고, ⊢는 ‘이 가정들에서 오른쪽 결론을 도출한다’고 읽습니다. 위의 Γ, A,…,A ⊢ C가 가능하면 아래의 Γ,!A ⊢ C로 묶을 수 있다는 뜻입니다. 아래 버튼은 사용처의 개수 k만 바꿉니다.
이 한 번의 규칙에서 A를 쓰는 자리 두 곳을 정합니다.
위쪽의 A(k)는 A가 k개 나열된 전제 목록입니다. 그림은 이 규칙에서 정한 사용처를 보여 주는 모형이며, 아무 때나 횟수 제한 없이 복사해도 된다는 허가는 아닙니다.
이 허가로 아무 재사용 규칙이나 되살리는 것은 아닙니다. 꺼낸 것은 A의 여러 사용처입니다. 다시 같은 재사용 허가를 무한히 만들어 주는 규칙까지 자동으로 생기는 것은 아닙니다. 다음 질문에서 그 차이를 만드는 다른 규칙을 함께 보겠습니다.
‘다시 포장하는 규칙’도 바뀐다고 했습니다. 느낌표를 한 겹 더 붙이면 안 되나요?
소프트 선형논리의 다른 핵심은 소프트 프로모션(soft promotion)입니다. Γ ⊢ A라는 증명이 있으면 !Γ ⊢ !A로 옮깁니다. 여기서 !Γ는 가정 목록 각각에 느낌표를 붙인 것입니다. 결론만 바꾸는 것이 아니라, 그 결론을 만들기 위해 쓰인 가정들도 함께 같은 층으로 옮깁니다.
그리고 일반적인 디깅(digging) 규칙을 채택하지 않습니다. 이 규칙은 !A ⊸ !!A라는 모양으로도 나타납니다. 이미 있는 한 겹의 재사용 허가를 더 깊은 재사용 층으로 자유롭게 바꾸는 길을 일반 규칙으로 주지 않는 것입니다.
소프트 프로모션
가정과 결론을 함께 같은 층으로 옮깁니다.
일반 디깅
일반 규칙으로 채택하지 않음
한 겹의 허가에서 두 겹의 허가로 자유롭게 옮기는 규칙을 주지 않습니다.
따라서 소프트 선형논리는 느낌표를 모두 없앤 체계가 아닙니다. 분배할 자원은 분배하고, 필요한 중첩도 표현합니다. 다만 그 중첩이 어떤 증명 구조에서 나왔는지가 남아 있도록 규칙을 고릅니다. 이 구조가 뒤에서 계산량을 세는 기준이 됩니다.
규칙을 바꾼 일이 실제 계산과 어떻게 이어지나요? 이번 논문에서도 증명망을 쓰나요?
이번에는 증명망을 계산의 연결을 드러내는 표현으로 사용합니다. 한 증명 조각이 A를 만들고, 다른 조각이 A를 받아 C를 만든다고 합시다. 앞의 출력과 뒤의 입력을 잇는 것이 컷에 대응합니다. 이 연결을 규칙에 따라 정리하는 과정이 계산입니다.
원문의 망에는 작은 셀과 그 안에 다른 망을 담는 상자가 있습니다. 선에는 논리식이 붙고, 셀에는 특별한 연결 지점인 주포트가 있습니다. 논문은 주포트끼리 만난 셀을 정해진 작은 구조로 바꾸는 외부 환원을 대상으로 계산 단계를 셉니다. 그림의 아무 부분이나 마음대로 지우는 작업이 아닙니다.
전체 증명망이 아닌, 입출력 연결의 개념도
u · 생성
증명 조각 u가
A를 만듭니다.
A · 입출력 연결
앞의 출력 A와
뒤의 입력 A를 잇습니다.
v · 사용
증명 조각 v가 A를 받아
C를 만듭니다.
연결을 정리하는 계산
허용된 외부 환원을 이어 가며 정규형에 도달합니다. 그림의 임의의 부분을 지우는 절차가 아닙니다.
상자가 분배기와 만나면 내부가 여러 벌로 펼쳐질 수 있습니다. 그러면 눈에 보이는 셀 수가 늘어나는 순간도 생깁니다. ‘계산을 한 단계 했으니 그림이 반드시 작아져야 한다’는 단순한 기준으로는 종료를 설명하기 어렵습니다. 그래서 다음에는 망의 크기와 별개로, 계산이 진행될 때 줄어드는 값을 찾습니다.
한 번에 몇 갈래로 나누는지와 상자가 몇 겹인지는 어떻게 구별하나요?
논문은 두 값을 따로 정의합니다. rank는 망 안의 분배기들이 요구하는 사용처 수 중 최댓값입니다. 이 글에서는 r로 쓰겠습니다. degree는 느낌표 상자의 최대 중첩 깊이이며, 여기서는 d로 쓰겠습니다. 상자가 여러 개 나란히 있는 것과, 한 상자 안에 다른 상자가 들어 있는 것도 구별해야 합니다.
한 상자를 세 갈래로 쓰는 구조는 사용처의 폭이 큽니다. 두 갈래로 쓰는 상자가 여러 겹 들어 있는 구조는 깊이가 큽니다. 두 수를 하나의 ‘복사 횟수’로 뭉뚱그리면 계산량을 읽는 중요한 정보가 사라집니다.
폭을 먼저 보기
가장 넓은 분배기의 사용처: 3개
상자의 최대 중첩: 1층
깊이를 먼저 보기
가장 넓은 분배기의 사용처: 2개
상자의 최대 중첩: 3층
두 독립적인 개념 모형입니다. 폭과 깊이를 구별하며, 두 구조의 실행량이 같다는 뜻은 아닙니다.
뒤에서 입력 길이 n이 등장하면 세 기호를 구별해 읽으면 됩니다. n은 입력의 길이, r은 망에서 정한 분배의 크기, d는 느낌표 구조의 깊이입니다. 원문이 선택한 데이터 표현에서는 문자열 길이가 분배기의 rank와 연결됩니다. 그 연결은 입력을 어떻게 표현했는지 확인한 뒤 사용해야 합니다.
상자가 펼쳐져 커지는데, 무엇이 줄어든다는 건가요?
그림에 지금 보이는 셀만 세는 대신, 상자가 앞으로 여러 번 쓰일 가능성까지 반영한 가중치를 붙입니다. 망 u의 가중치를 Wu(X)라고 쓰며, 이것은 X에 관한 다항식입니다. 실제 망의 rank가 r이면 X 자리에 r을 넣습니다.
느낌표 상자의 공식은 W!u(X)=X·Wu(X)+1입니다. 안쪽의 가중치에 사용 규모를 곱하고 상자 자신의 1을 더합니다. 모든 셀을 무조건 1로 세는 방식은 아닙니다. 원문에서는 오른쪽 논리규칙의 원자 셀에 1, 왼쪽 규칙의 원자 셀에 0을 주며, 분배기 자체의 가중치도 0입니다.
가중치 정의를 배우기 위한 계산 모형입니다. 실제 실행 시간이나 전체 증명망의 정당성을 검사하지 않습니다.
분배 수 r = 3을 가중치에 반영
r = 1을 넣으면 W₂(1) = 3 + 2 = 5입니다.
W₀ = 3, Wd(r) = rWd−1(r) + 1로 정한 가중치 학습용 국소 모형입니다. 버튼은 바깥 상자 하나와 r분배기를 펼치는 장면만 보여 줍니다. 완전한 증명망 실행기나 실제 계산 단계 수의 측정기가 아닙니다.
중요한 사실은 원문이 정한 외부 환원마다 Wu(r)라는 자연수가 줄어든다는 것입니다. 그래서 정리 2는 외부 환원이 그 처음 값보다 많이 계속될 수 없다고 말합니다. 같은 상자 모양을 설명하기 위해 붙인 비유적 점수가 아니라, 실제 환원 규칙과 맞물리게 정의한 값입니다.
r · 분배기의 rank
망 안 분배기들의 사용처 수 중 최댓값
d · 느낌표 상자의 깊이
! 상자가 겹치는 최대 층수
무엇을 늘리고 무엇을 고정했는지 함께 읽습니다.
위 실험에서는 Wd(1)=3+d입니다. r≥1이면 낮은 차수의 항도 rd 이하로 묶여 Wd(r)≤(3+d)rd를 얻습니다. 다항시간이라는 결론에는 이처럼 무엇을 변수로 늘리고 무엇을 고정했는지가 함께 들어 있습니다. 원문도 깊이가 달라지는 망 전체에 관한 정규화 논의와 고정 프로그램의 다항시간 논의를 구별합니다.
반복에서 숫자로, 숫자에서 판정으로
작은 계산 부품이 다항시간 판정문제 전체를 표현하는 구성으로 이어집니다.
여기까지는 상자 이야기였는데, 실제 숫자도 이 논리 안에 넣을 수 있나요?
논문은 숫자를 어떤 동작을 몇 번 반복할지 정하는 표현으로 넣습니다. 숫자 3을 예로 들면, 동작 f와 시작값 x를 받아 f(f(f(x)))를 만드는 방식입니다. 이런 표현을 처치 수(Church numeral)라고 부릅니다. 숫자 0은 동작을 한 번도 적용하지 않고 시작값을 돌려주는 경우입니다.
원문의 자연수 타입은 N=∀α.!(α⊸α)⊸α⊸α입니다. α⊸α는 같은 종류의 값을 받아 그 종류의 값을 만드는 한 단계 동작, 그 앞의 !는 반복에 쓰일 동작임을 나타냅니다. ∀α는 값의 종류가 바뀌어도 같은 반복 형식을 사용할 수 있게 하는 부분입니다.
설명용 예 · 시작값 x = 0, 동작 f는 1 더하기
여기서 3은 동작을 적용하는 횟수입니다. 숫자를 적는 자릿수와 구별합니다.
이 구별은 계산량에서 특히 중요합니다. 값이 m인 수를 동작 m번으로 표현했다면, 그 길이도 그 반복을 반영합니다. ‘숫자값만큼 반복하니 빠르다’는 말을 이진 입력의 자릿수에 관한 주장으로 바꿀 수는 없습니다. 논문은 먼저 데이터가 어떤 망으로 표현되는지 정하고, 그 표현과 rank의 관계를 이용합니다.
앞 절의 번역은 이런 연결을 설명합니다. 일정한 rank로 사용하는 !A를 여러 개의 A로 펼쳐 읽을 수 있지만, 표기를 펼치면 망의 크기가 커질 수 있습니다. 압축된 표현의 길이와 펼쳐진 계산의 양을 계속 구별하는 것입니다.
그 숫자로 덧셈과 곱셈을 하려면, 결국 또 복사해야 하지 않나요?
그래서 논문은 익숙한 산술 결과만 적지 않고, 어떤 타입의 입력을 몇 개 사용해 그 결과를 만들었는지를 함께 남깁니다. 보조정리 5는 덧셈과 곱셈을 표현하는 증명을 구성합니다. 두 반복을 이어 붙이면 합에 대응하는 반복이 되고, 한 반복을 다른 반복과 결합하는 구조를 만들면 곱에 대응하는 반복이 됩니다.
예를 들어 rank 3을 바탕으로 6이나 9를 표현할 수 있지만, 이때 쓰는 타입의 모양도 달라집니다. 원문은 이를 다항식 ‘표현’으로 구별합니다. 값이 같은 산술식이라고 해서 타입의 구조까지 모두 자유롭게 바꿀 수 있는 것은 아닙니다. 여기서는 그 형식 전체를 외우기보다, 같은 결과값과 같은 자원 사용 구조가 다르다는 점을 잡으면 됩니다.
합 · 반복을 이어 붙이기
3회 + 3회 = 6회
3회 다음 3회
곱 · 반복을 묶기
3 × 3 = 9회
3개씩 3묶음
이동 · 하나를 옮기기
ψ(4, 2) = (3, 3)
전체 합 6은 유지됩니다.
앞의 두 패널은 산술 뜻의 모형이며, 셋째 패널은 원문의 ψ 함수에 (4, 2)를 넣은 사례입니다. 원논문의 증명망을 옮긴 그림은 아닙니다.
다음 부품은 더 작아 보입니다. 쌍 (p,q)에서 p>0이면 (p−1,q+1)로, p=0이면 그대로 두는 함수 ψ입니다. 하나를 옮기되 전체 길이는 유지합니다. 이런 한 단계 변화가 다음 절에서 기계의 상태와 테이프를 바꾸는 계산의 바탕이 됩니다.
또한 원문의 제한 안에서는 보통의 자연수 타입 N을 아무 조건 없이 N⊗N으로 복제하는 generic 증명이 없습니다. 현실의 숫자를 복사할 수 없다는 말이 아니라, 이 타입과 이 증명 규칙 안에서 필요한 사용처를 명시해야 한다는 뜻입니다.
숫자와 한 칸 이동만으로, 컴퓨터가 하는 판단까지 표현할 수 있나요?
논문은 부품을 차례로 늘립니다. 먼저 0과 1에 해당하는 값을 만들고, 그 값에 따라 어느 계산을 진행할지 고르는 조건문을 만듭니다. 다음에는 001처럼 0과 1이 이어진 문자열을 표현합니다. 이때 길이 n의 문자열 표현은 rank n인 균질한 망과 연결됩니다.
계산 기계의 한 순간에는 현재 상태, 지금 읽는 기호, 읽는 곳의 왼쪽과 오른쪽에 남은 내용이 필요합니다. 원문은 이 요소들을 타입 안에 배치하고, 한 번의 전이를 수행하는 증명을 구성합니다. 무엇을 읽었는지에 따라 쓸 기호와 다음 상태, 이동 방향을 정하는 것입니다.
1을 읽고 0을 쓴 뒤, 상태를 q1로 바꾸고 오른쪽으로 이동합니다.
전이 전
상태 q0현재 읽는 칸: 2 · 기호: 1
전이 후
상태 q1현재 읽는 칸: 3 · 기호: 빈칸 (□)
R은 오른쪽 이동, □는 빈칸입니다. 인덱스는 0부터 셉니다. 이 한 단계는 설명용 예시이며 원문의 특정 기계가 아닙니다.
한 단계를 만들었다고 전체 계산이 저절로 완성되는 것은 아닙니다. 입력을 테이프에 놓고, 필요한 공간을 준비하고, 정해진 횟수만큼 전이를 반복하고, 마지막 상태에서 참·거짓을 읽는 구성까지 필요합니다. 논문이 앞 절에서 준비한 반복과 다항식 표현이 이 단계에서 함께 쓰입니다.
원문은 고정 크기의 유한 테이프를 가진 표현을 사용하고, 최종 상태에서도 전이 규칙이 정의되도록 둡니다. 이런 세부 조건이 있어야 ‘정해 둔 횟수만큼 반복한다’는 구성과 최종 판정이 맞물립니다.
제한을 이렇게 많이 두어도 모든 다항시간 문제를 표현할 수 있다는 건가요?
여기서는 두 방향을 분명히 나누어야 합니다. 첫째는 허용한 방식으로 만든 고정 프로그램이 계산량의 범위를 지킨다는 방향입니다. 둘째는 다항시간에 판정할 수 있는 비트문자열 문제를 이 체계 안에서 표현할 수 있다는 방향입니다. 규칙이 안전하기만 하고 표현할 수 있는 문제가 너무 적다면, 이 두 번째 방향은 성립하지 않겠지요.
정리 9는 두 번째 방향을 구성으로 보입니다. 어떤 문자열 판정이 시간 다항식 P(n)과 공간 다항식 Q(n) 안에서 가능하다면, 그 판정을 수행하는 generic 증명을 만들 수 있다고 합니다. 여기서 generic은 일상적인 ‘일반 프로그램’이 아니라, 프로그램 부분에 분배기가 들어 있지 않은 망을 가리키는 원문의 용어입니다.
01 프로그램에서 상한으로
+ 정해진 문자열 입력 표현다항식 계산량 상한
02 판정문제에서 표현으로
문자열 판정문제알맞은 입력 사본
+ 기계 구성그 판정을 하는
generic 증명
초기에 제공할 입력 사본 수
m = deg P + deg Q + 1
m = 2 + 1 + 1 = 4
같은 입력 문자열의 사본 4개를 처음부터 공급합니다. 실행 중 자유롭게 복사한다는 뜻이 아닙니다.
generic은 프로그램 부분에 분배기가 없는 망을 뜻합니다. 이 표현 정리가 기존 상용 코드를 자동 변환해 준다는 뜻은 아닙니다.
이 구성에는 같은 입력 문자열의 사본을 몇 개 제공할지도 포함됩니다. 정리에 나오는 가정 수는 deg P + deg Q + 1입니다. 예를 들어 시간 상한의 차수가 2이고 공간 상한의 차수가 1이면 이 구성에서는 입력 가정 네 개를 사용합니다. 이 수는 입력 길이가 늘 때마다 새로 늘어나는 수가 아니라, 그 판정 프로그램의 상한을 정하면 고정되는 수입니다.
첫 번째 방향에서는 이렇게 고정한 프로그램과 알맞은 입력 인코딩을 정리 2의 상한과 연결합니다. 결과적으로 다항시간 판정과 이 논리 안의 적절한 표현이 양쪽에서 만납니다. 임의의 복잡한 계산을 자동으로 빠르게 만드는 장치를 얻은 것은 아닙니다.
보증의 범위와 다음 연구
표현 가능성, 실제 프로그램 작성, 오늘의 적용 질문을 차례로 구별합니다.
‘표현할 수 있다’면, 지금 쓰는 프로그램에도 바로 이 보증을 붙일 수 있을까요?
어떤 판정을 수행하는 표현이 존재한다는 사실과, 우리가 이미 써 둔 프로그램에 그 표현을 자연스럽게 부여하는 일은 구별해야 합니다. 같은 결과를 내도록 다시 구성해야 할 수도 있고, 데이터를 담는 방식이나 반복의 모양을 바꾸어야 할 수도 있습니다. 이 논문의 완전성은 기존 코드의 모든 작성 방식을 그대로 받아들이는 정리가 아닙니다.
또 하나의 구별도 필요합니다. 제시된 증명이 규칙에 맞는지 확인하는 일, 프로그램에 맞는 타입과 증명을 찾아내는 일, 임의의 프로그램이 실제로 다항시간인지 알아내는 일은 서로 다릅니다. 계산량 보증을 얻을 수 있는 형식을 제시했다는 사실만으로 이 모든 작업이 간단해지지는 않습니다.
제시된 도출 확인
- 입력
- 이미 제시된 타입과 도출
- 묻는 것
- 각 단계가 정해진 규칙에 맞는가?
맞는 타입과 도출 찾기
- 입력
- 검토하려는 프로그램과 타입 체계
- 묻는 것
- 프로그램에 맞는 타입과 도출을 찾을 수 있는가?
기존 코드의 실제 계산량 분석
- 입력
- 기존 코드와 입력·비용 모형
- 묻는 것
- 입력이 커질 때 이 코드의 실제 계산량은 어떻게 늘어나는가?
바이요와 모그빌은 라퐁의 2002년 공개본을 바탕으로 소프트 람다 계산을 발전시켰습니다. 2003년에 공개하고 2004년에 발표한 논문에서는 리스트를 표현하는 자료형과 삽입정렬을 살핍니다. 같은 다항시간 함수를 표현하는 능력과, 프로그래머가 원하는 알고리즘을 자연스럽게 쓰는 능력 사이의 간격을 다룬 사례입니다.
타입을 자동으로 찾아 주는 문제에도 범위가 있습니다. Chrząszcz와 Schubert의 2016년 논문은 자신들이 다루는 다형적 소프트 타입 배정 체계에서 타입검사·타입추론의 판정불가능성을 보입니다. 이는 정해진 작은 언어에서 제한된 검사나 보수적인 보증을 개발할 수 없다는 뜻은 아닙니다. 적용할 언어와 허용 규칙을 먼저 밝혀야 합니다.
이 논문을 읽고 나면, 계산을 볼 때 무엇부터 물으면 좋을까요?
먼저 입력의 크기를 무엇으로 세는가를 물으면 됩니다. 항목 수인지, 문자열 길이인지, 숫자의 값인지에 따라 같은 반복을 다르게 평가하게 됩니다. 다음에는 입력을 늘릴 때 어떤 구조가 고정되어 있는가를 물어야 합니다. 이 논문에서는 프로그램과 느낌표 상자의 깊이를 고정하는 조건이 핵심이었습니다.
마지막으로 무엇을 한 단계의 비용으로 세었는가를 확인하세요. 원문의 정리 2는 외부 환원을 셉니다. 서버 응답 시간, 네트워크 지연, 메모리에 자료를 옮기는 실제 비용까지 자동으로 같은 숫자가 되는 것은 아닙니다. 증명된 모형의 상한과 실제 환경에서의 측정은 함께 살펴볼 수 있는 서로 다른 정보입니다.
입력 크기 n은 무엇인가?
입력예시 답 · 비트 수
실제 입력 표현의 길이를 셉니다.
고정 구조 d는 무엇인가?
구조예시 답 · 고정 프로그램의 ! 깊이
느낌표 상자의 최대 중첩을 확인합니다.
세는 단계는 무엇인가?
비용예시 답 · 원문의 외부 환원
상한이 어떤 계산 단위를 세는지 밝힙니다.
소프트 선형논리의 성과는 복사를 무조건 금지하지 않으면서, 복사가 계산을 늘리는 방식을 증명 구조 안에 남겨 둘 수 있다는 데 있습니다. 그리고 그 제한 안에서도 다항시간 판정문제를 표현할 수 있음을 보입니다. 무엇을 허용하는지가 분명해지면, 그 허용이 어떤 계산량을 만들어 내는지도 묻고 증명할 수 있게 됩니다.
한 가지 보증에서, 다른 비용과 결과의 성질로
소프트 선형논리의 후속 질문은 ‘이 규칙으로 프로그램을 어떻게 쓰는가’에서 멈추지 않습니다. 병렬로 일할 때 어떤 비용을 세어야 하는지, 계산량의 보증과 결과의 정확성을 한 프로그램 안에서 어떻게 함께 표현할지도 연구합니다.
시간·작업량·공간을 다시 구별하기
파울랭 자코베 드 노루아의 Parallelism in Soft Linear Logic은 새 병렬 양상을 더한 확장 체계를 다룹니다. PSPACE, 즉 사용하는 공간이 입력 길이의 다항식으로 제한되는 판정문제들의 범위를 특징짓습니다. 원래 SLL이 이 모든 문제를 순차 다항시간으로 푼다는 결론으로 옮길 수는 없습니다.
계산량과 결과의 조건
로버트 앳키의 Polynomial Time and Dependent Types는 다항시간을 통제하는 선형 타입과 값에 따라 달라지는 타입을 결합합니다. 계산이 정해진 범위에서 끝나는지와 결과가 요구한 성질을 만족하는지를 함께 묻는 관련 연구입니다. SLL을 그대로 제품에 옮긴 사례로 소개하는 것은 아닙니다.
LTCT의 교육에서도 ‘정답인가?’ 옆에 ‘입력이 두 배라면 해야 할 일이 어떻게 늘까?’라는 질문을 놓아 볼 수 있습니다. 먼저 항목 수와 비교 횟수를 직접 세어 보고, 어떤 구조를 고정했는지 말하게 하는 방식입니다. 이는 이 글에서 제안하는 수업 활동이며, 홈페이지 프로그램이 이미 소프트 선형논리로 검증되었다는 뜻은 아닙니다.
복제를 허용하는 규칙을 정밀하게 고르면,
계산이 얼마나 늘어날지도 증명의 질문이 됩니다.
기호를 다시 펼쳐 보기
- n
- 입력 길이이 글에서는 비트 수처럼 실제 인코딩의 길이로 사용합니다.
- !A
- 느낌표가 붙은 자원재사용을 다루는 양상. 꺼내는 횟수와 허용 규칙을 함께 읽습니다.
- Γ ⊢ A
- 가정에서 결론으로가정 목록 Γ에서 A를 도출한다는 표기입니다.
- k
- 해당 분배기의 사용처 수멀티플렉싱의 한 적용에서 정하며 0도 허용합니다.
- r
- 망의 rank그 망에 있는 분배기들의 사용처 수 중 최댓값입니다.
- d
- 느낌표 상자의 깊이! 상자가 겹치는 최대 층수. 다항식 상한에서 고정하는 구조입니다.
- Wᵤ(r)
- 가중치에 rank를 넣은 값정리 2에서 외부 환원 횟수의 상한으로 쓰입니다.
- generic
- 분배기가 없는 망이 논문의 프로그램 구성에서 쓰는 기술적 용어입니다.
- N
- 자연수의 타입같은 동작을 정해진 횟수만큼 반복하는 처치 수로 읽습니다.
- S · B
- 문자열 · 참거짓의 타입정리 9는 비트문자열을 받아 참·거짓을 판정하는 구성을 다룹니다.
읽은 내용을 적용하기
복제가 거듭될 때 무엇을 세어야 할까요?
입력의 크기와 복제가 중첩되는 깊이를 따로 적어 봅니다. 같은 계산 규칙을 유지한 채 입력만 늘리는 경우와 복제 구조 자체를 더 깊게 만드는 경우를 구분하면 계산량 보증의 조건을 읽기 쉽습니다.
본문 실험에서 입력 크기 하나만 바꾼 뒤 결과를 기록하세요. 다음에는 복제 구조를 바꾸고, 앞의 비교에서 고정했던 조건이 무엇인지 설명해 보세요.
학습 안내 · 위 사례는 본문 개념을 연습하도록 편집부가 구성했습니다. 원문의 정의와 정리의 적용 범위는 각 문답의 출처에서 확인할 수 있습니다.
원문과 참고자료
- Yves Lafont, Soft Linear Logic and Polynomial TimeTheoretical Computer Science 318(1–2), 163–180 (2004). DOI: 10.1016/j.tcs.2003.10.018.
본 대담의 주된 원문입니다. 저자 공식 목록에 연결된 2002년 2월 18일 공개 프리프린트 20쪽 전체를 확인했습니다. 질문 옆의 상세 쪽수는 이 공개본 기준이며 학술지 페이지와 혼용하지 않습니다. §1 규칙, §2 가중치·정리 2, §3 번역, §4 수 표현, §5 정리 9, 결론과 부록을 대조했습니다. - Jean-Yves Girard, Linear Logic / Light Linear Logic선형논리의 출발점과 계산량 연구의 선행 맥락입니다. Linear Logic(1987)은 이 연재 1회에서 다뤘습니다. Light Linear Logic, Information and Computation 143(2), 175–204 (1998)의 위치는 라퐁의 서론과 서지로 확인했습니다. 이번 글에서는 라이트 선형논리의 세부 정리를 별도로 재구성하지 않습니다.
- Patrick Baillot · Virgile Mogbil, Soft lambda-calculus: a language for polynomial time computation2003년 12월 7일 arXiv 공개. FoSSaCS 2004, LNCS 2987, 27–41. DOI: 10.1007/978-3-540-24727-2_4.
프로그램 표현의 자연스러움, 리스트 자료형, 삽입정렬이라는 후속 맥락을 확인했습니다. 공개 연혁을 학회 논문집 발표 연도와 구분하여 서술했습니다. - Jacek Chrząszcz · Aleksy Schubert, The role of polymorphism in the characterisation of complexity by soft typesInformation and Computation 248, 130–149 (2016). DOI: 10.1016/j.ic.2015.12.011.
지정된 다형적 소프트 타입 체계의 타입검사·타입추론 한계를 설명하는 출판사 초록을 확인했습니다. 모든 제한적 검사에 대한 불가능성으로 일반화하지 않습니다. - Paulin Jacobé de Naurois, Parallelism in Soft Linear LogicCSL 2022, LIPIcs 216, 26:1–26:16. DOI: 10.4230/LIPIcs.CSL.2022.26.
공식 출판 자료의 초록과 연구 맥락을 확인했습니다. 새 병렬 양상을 도입한 확장 체계의 결과로 소개하며, 원래 SLL의 순차 시간 보증과 구분합니다. - Robert Atkey, Polynomial Time and Dependent TypesProceedings of the ACM on Programming Languages 8(POPL), Article 76 (2024). DOI: 10.1145/3632918.
저자 공개본의 초록과 도입부를 확인했습니다. 계산량과 결과의 성질을 함께 다루는 관련 연구로 연결하며, SLL의 직접 구현 사례로 제시하지 않습니다.
구성·가상 대담·생각그림·실험: LTCT KOREA. 원논문의 문장이나 도판을 길게 옮기지 않고 학습을 위한 설명과 그림을 새로 작성했습니다. 모노그램 YL은 이름의 이니셜이며 인물 사진이 아닙니다.
자료 확인일: 2026년 10월 4일. 인용 횟수와 순위는 검증한 수치가 없어 제시하지 않습니다. 공개본과 학술판의 구분, 실험이 보여 주는 범위를 각 위치에 표시했습니다.
서체 · Noto Sans KR과 DejaVu Sans를 사용합니다.
포함된 서체의 라이선스 보기
Copyright 2014-2021 Adobe (http://www.adobe.com/), with Reserved Font Name 'Source'
This Font Software is licensed under the SIL Open Font License, Version 1.1.
This license is copied below, and is also available with a FAQ at:
https://scripts.sil.org/OFL
-----------------------------------------------------------
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
-----------------------------------------------------------
PREAMBLE
The goals of the Open Font License (OFL) are to stimulate worldwide
development of collaborative font projects, to support the font creation
efforts of academic and linguistic communities, and to provide a free and
open framework in which fonts may be shared and improved in partnership
with others.
The OFL allows the licensed fonts to be used, studied, modified and
redistributed freely as long as they are not sold by themselves. The
fonts, including any derivative works, can be bundled, embedded,
redistributed and/or sold with any software provided that any reserved
names are not used by derivative works. The fonts and derivatives,
however, cannot be released under any other type of license. The
requirement for fonts to remain under this license does not apply
to any document created using the fonts or their derivatives.
DEFINITIONS
"Font Software" refers to the set of files released by the Copyright
Holder(s) under this license and clearly marked as such. This may
include source files, build scripts and documentation.
"Reserved Font Name" refers to any names specified as such after the
copyright statement(s).
"Original Version" refers to the collection of Font Software components as
distributed by the Copyright Holder(s).
"Modified Version" refers to any derivative made by adding to, deleting,
or substituting -- in part or in whole -- any of the components of the
Original Version, by changing formats or by porting the Font Software to a
new environment.
"Author" refers to any designer, engineer, programmer, technical
writer or other person who contributed to the Font Software.
PERMISSION & CONDITIONS
Permission is hereby granted, free of charge, to any person obtaining
a copy of the Font Software, to use, study, copy, merge, embed, modify,
redistribute, and sell modified and unmodified copies of the Font
Software, subject to the following conditions:
1) Neither the Font Software nor any of its individual components,
in Original or Modified Versions, may be sold by itself.
2) Original or Modified Versions of the Font Software may be bundled,
redistributed and/or sold with any software, provided that each copy
contains the above copyright notice and this license. These can be
included either as stand-alone text files, human-readable headers or
in the appropriate machine-readable metadata fields within text or
binary files as long as those fields can be easily viewed by the user.
3) No Modified Version of the Font Software may use the Reserved Font
Name(s) unless explicit written permission is granted by the corresponding
Copyright Holder. This restriction only applies to the primary font name as
presented to the users.
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
Software shall not be used to promote, endorse or advertise any
Modified Version, except to acknowledge the contribution(s) of the
Copyright Holder(s) and the Author(s) or with their explicit written
permission.
5) The Font Software, modified or unmodified, in part or in whole,
must be distributed entirely under this license, and must not be
distributed under any other license. The requirement for fonts to
remain under this license does not apply to any document created
using the Font Software.
TERMINATION
This license becomes null and void if any of the above conditions are
not met.
DISCLAIMER
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
OTHER DEALINGS IN THE FONT SOFTWARE.
DejaVu Sans license and copyright:
Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: DejaVu fonts
Upstream-Author: Stepan Roh <src@users.sourceforge.net> (original author),
see /usr/share/doc/fonts-dejavu-core/AUTHORS for full list
Source: https://dejavu-fonts.github.io/
Files: *
Copyright: Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved.
Bitstream Vera is a trademark of Bitstream, Inc.
DejaVu changes are in public domain.
License: bitstream-vera
Permission is hereby granted, free of charge, to any person obtaining a copy
of the fonts accompanying this license ("Fonts") and associated
documentation files (the "Font Software"), to reproduce and distribute the
Font Software, including without limitation the rights to use, copy, merge,
publish, distribute, and/or sell copies of the Font Software, and to permit
persons to whom the Font Software is furnished to do so, subject to the
following conditions:
.
The above copyright and trademark notices and this permission notice shall
be included in all copies of one or more of the Font Software typefaces.
.
The Font Software may be modified, altered, or added to, and in particular
the designs of glyphs or characters in the Fonts may be modified and
additional glyphs or characters may be added to the Fonts, only if the fonts
are renamed to names not containing either the words "Bitstream" or the word
"Vera".
.
This License becomes null and void to the extent applicable to Fonts or Font
Software that has been modified and is distributed under the "Bitstream
Vera" names.
.
The Font Software may be sold as part of a larger software package but no
copy of one or more of the Font Software typefaces may be sold by itself.
.
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT,
TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME
FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING
ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES,
WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE
FONT SOFTWARE.
.
Except as contained in this notice, the names of Gnome, the Gnome
Foundation, and Bitstream Inc., shall not be used in advertising or
otherwise to promote the sale, use or other dealings in this Font Software
without prior written authorization from the Gnome Foundation or Bitstream
Inc., respectively. For further information, contact: fonts at gnome dot
org.
Files: debian/*
Copyright: (C) 2005-2006 Peter Cernak <pce@users.sourceforge.net>
(C) 2006-2011 Davide Viti <zinosat@tiscali.it>
(C) 2011-2013 Christian Perrier <bubulle@debian.org>
(C) 2013 Fabian Greffrath <fabian+debian@greffrath.com>
License: GPL-2+
This program is free software; you can redistribute it
and/or modify it under the terms of the GNU General Public
License as published by the Free Software Foundation; either
version 2 of the License, or (at your option) any later
version.
.
This program is distributed in the hope that it will be
useful, but WITHOUT ANY WARRANTY; without even the implied
warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR
PURPOSE. See the GNU General Public License for more
details.
.
You should have received a copy of the GNU General Public
License along with this package; if not, write to the Free
Software Foundation, Inc., 51 Franklin St, Fifth Floor,
Boston, MA 02110-1301 USA
.
On Debian systems, the full text of the GNU General Public
License version 2 can be found in the file
/usr/share/common-licenses/GPL-2'.