증명 탐색·타입 검사·Curry–Howard

증명을 찾는 것과 제시된 증명을 검사하는 것

언어 모델이 증명을 제안한 일, 탐색기가 증명을 못 찾은 일, 검사기가 항을 거부한 일은 서로 다른 사건입니다. 이 실습은 타입 주석이 있는 단순 타입 람다 항으로 차이를 살펴봅니다. 원자 타입 P,Q,R과 함수 타입만 사용하며 의존 타입·재귀·산술 공리·암묵적인 고전 논리 원리는 추가하지 않습니다.

판정에는 가정, 항, 타입이 함께 들어갑니다.

$$\Gamma\vdash t:A.$$

“문맥 Γ의 가정 아래 항 t의 타입이 A이다”라고 읽습니다. 명제와 타입의 대응에서 t는 명제 A의 증거입니다. A→B는 A의 증거를 받아 B의 증거를 만드는 함수입니다. 가정도 주장의 일부입니다. f:P→Q와 g:Q→R을 가정한 증명이 그 함수들을 빈 문맥에서 만들어냈다는 뜻은 아닙니다.

세 가지 지역 규칙

변수는 문맥에서 타입을 가져옵니다. λ는 매개변수를 가정에 넣고 본문을 검사한 뒤 함수 타입을 만듭니다. 적용은 함수의 입력 타입과 인수 타입이 같아야 합니다.

$$\frac{x:A\in\Gamma}{\Gamma\vdash x:A} \qquad \frac{\Gamma,x:A\vdash t:B}{\Gamma\vdash\lambda x:A.t:A\to B} \qquad \frac{\Gamma\vdash f:A\to B\quad\Gamma\vdash u:A} {\Gamma\vdash f\,u:B}.$$

매개변수 주석 덕분에 항의 문법 구조를 따라 타입을 추론할 수 있습니다. 검사기는 정리를 추측하는 대신 문맥에 없는 변수, 함수가 아닌 값의 적용, 입력 타입 불일치를 구분합니다. 전제가 실패하면 그 전제를 사용하는 상위 노드도 실패합니다. 함수 위치가 이미 원자 타입이면 인수를 더 검사할 필요 없이 거부할 수 있습니다. 회색 노드는 이때 방문하지 않은 문법이며 임의로 오류라고 판단한 것이 아닙니다.

트리는 제시한 후보의 실제 AST입니다. 노드마다 추론 타입 또는 실패가 표시되고, 선택한 검사 단계의 규칙은 별도로 보입니다. 긴 노드 타입은 줄여 표시하지만 표에는 전체 타입을 남깁니다.

결합된 변수를 정확하게 가리키기

내부 변수는 de Bruijn 번호로 저장합니다. 0은 가장 가까운 결합입니다. λ에 들어가면 새 매개변수가 문맥의 앞에 추가되어 이전 변수 번호가 하나씩 밀립니다. 읽기 쉬운 이름은 표시할 때만 만듭니다.

[f:P→Q,g:Q→R]에서 λx:P에 들어가면 [x:P,f:P→Q,g:Q→R]이 됩니다. 따라서 g는 2, f는 1, x는 0입니다. 번호 이동을 잘못 적용하면 다른 항이 되거나 타입 검사를 실패합니다. 화면의 이름이 같다고 결합 관계를 무시해도 되는 것은 아닙니다.

한도 안에서 실제로 탐색하는 문법

탐색은 정확한 항 노드 수를 1부터 늘립니다. 변수·λ·함수 적용이 각각 한 노드이고 타입 주석의 크기는 세지 않습니다. 문법은 β-정상형에 한정합니다. 정상형 본문을 가진 λ이거나, 문맥 변수를 머리로 삼아 정상형 인수들을 적용한 항입니다. 함수 자리에 λ를 바로 놓는 β-redex는 탐색하지 않습니다.

목표가 화살표이면 λ를 도입할 수 있습니다. 문맥의 함수에서 화살표를 차례로 따라가 목표 타입에 도달하는 머리도 살펴보고, 남은 크기를 인수들에게 나눕니다. 이 방법은 명시한 정상형 문법을 다룹니다. 가장 작은 크기부터 찾으므로 발견한 크기는 해당 문법과 한도 안의 최소값입니다. 정상화가 항 크기를 바꿀 수 있어 이 한도를 임의의 증명 문법 전체의 크기 한도와 같다고 말하면 안 됩니다.

실패의 뜻은 이 한도 안에서 정상형 항을 찾지 못했다입니다. 거짓·UNSAT·증명 부재·타입의 비거주를 뜻하지 않습니다. 찾은 결과도 별도의 타입 검사기에 보내 목표 타입과 같은지 확인합니다. 직접 제시한 후보의 검사는 탐색 한도와 독립이므로 후보가 한도보다 커도 유효한 증명일 수 있습니다.

조작에 사용하는 목표·문맥·후보 표

화살표는 오른쪽으로 결합합니다. P→Q→P는 P→(Q→P)입니다.

목표 번호	타입
0,1,2	각각 P,Q,R
3	P→P
4	P→Q
5	P→R
6	(P→Q)→P→Q
7	P→Q→P
8	(P→Q)→(Q→R)→P→R
9	((P→Q)→P)→P

문맥 0은 빈 목록, 1은 [f:P→Q,g:Q→R], 2는 [p:P,f:P→Q], 3은 [p:P], 4는 [f:P→Q]입니다. 가까운 변수부터 나열하며 숨겨진 사실을 추가하지 않습니다.

후보 0은 λx:P.x, 후보 1은 λx:P.g(fx)이며 문맥 1을 기대합니다. 후보 2는 변수 0을 자기 자신에 적용하고, 3은 변수 0 자체이며, 4는 변수 1을 변수 0에 적용합니다. 후보 5는 λx:P.λy:Q.x입니다. 후보 6은 λf:P→Q.λg:Q→R.λx:P.g(fx)인 닫힌 합성이고, 7은 λf:P→Q.f인 함수 항등입니다. 같은 후보도 문맥을 바꾸면 의미나 가능 여부가 달라집니다.

손계산: 탐색 실패와 실제 증명의 공존

목표 5, 문맥 1, 한도 5, 후보 1을 선택합니다.

$$\lambda x:P.\ g\,(f\,x):P\to R.$$

변수 세 개, 적용 두 개, λ 한 개라서 크기는 6입니다. g:Q→R, f:P→Q, x:P를 확인한 뒤 안쪽 적용에서 Q, 바깥쪽에서 R을 얻습니다. λ로 x의 가정을 해제하면 P→R입니다. 후보는 목표를 증명하지만 한도 5의 탐색은 놓칩니다. f와 g의 가정은 Γ에 남습니다.

한도만 6으로 올리면 크기 6의 정상형 증명을 찾고 다시 검사합니다. 직접 제시한 후보의 타입은 바뀌지 않습니다. 그림의 파랑은 각 독립 탐색 한도에서의 발견 여부이고 주황은 고정한 후보가 전체 목표를 증명하는지입니다. 시간이나 확률 곡선이 아닙니다. 곡선은 아홉 한도를 비교하며 현재 증명 결과는 선택한 한도만 사용합니다.

손계산: 잘 타입화되지만 다른 정리를 증명하는 항

빈 문맥 0, 목표 4, 후보 0을 사용합니다. 항등 항의 타입은 P→P라서 지역 검사는 모두 통과합니다. 하지만 요청한 정리 P→Q와 다릅니다. 파란 타입 트리만 보고 요청한 정리를 증명했다고 보고하면 안 됩니다.

P가 참이고 Q가 거짓인 Boolean 배정은 P→Q를 거짓으로 만듭니다. P=1,Q=2,R=4 비트로 나타내면 반례는 1과 5입니다. 이는 탐색 실패와 별개의 의미적 반박입니다. 반대로 Boolean 반례가 없다는 사실이 증명 항을 만들어주지는 않습니다. 이 진리표는 필요한 의미적 검사이지 구성적 증명 탐색의 완전한 oracle이 아닙니다. 목표 9는 Boolean에서는 타당하지만 이 한도 안에서 항을 못 찾는 예입니다. 그 탐색 실패만으로 증명 부재를 주장하지 않습니다.

연습 문제와 해설

문제: 문맥 1에서 후보 2인 f를 f에 적용한 항을 검사하세요. 무엇이 맞지 않나요?

해설: 두 f의 타입은 각각 P→Q입니다. 함수가 요구하는 인수 타입은 P이므로 마지막 적용에서 타입이 맞지 않습니다. 변수들은 개별적으로 타입을 갖지만 적용은 유효하지 않고 루트 타입도 없습니다.

이제 문맥 3=[p:P]에서 같은 후보를 검사하세요. 함수 자리가 원자 P라서 인수를 검사하기 전에 거부합니다. 문법 노드는 셋이지만 검사 단계는 둘이고 남은 인수는 회색입니다. 미검사 노드가 잘못되었다고 선언한 것이 아닙니다.

추가 결합 문제: 후보 5의 닫힌 타입은 P→Q→P입니다. λ 두 개 안에서 바깥 매개변수는 0이 아니라 1입니다. 번호를 0으로 바꾸면 Q를 반환해 증명하는 타입도 바뀝니다.

신뢰 경계와 AI 연구

탐색 휴리스틱은 바꾸면서도 검사 규칙은 유지할 수 있습니다. 생성된 증명을 증거로 쓰려면 가정, 상세한 항, 요청한 문장을 의도한 체계에서 확인해야 합니다. 이 실습은 명시한 단순 타입 조각만 검사하며 Lean의 커널이나 임의의 의존 타입 증명 검사기가 아닙니다. 정확 하위 문제 방문 수는 메모된 탐색 상태 수이지 시간이나 가능한 모든 유도의 개수가 아닙니다.

주석이 있는 변수·λ·적용의 문법 지향 추론은 Programming Language Foundations in Agda: Inference, 명제와 타입 및 함의와 함수의 대응은 Lean의 Propositions and Proofs에서 살펴볼 수 있습니다. 제한된 정상형 탐색과 문맥·후보 표·진단 비교는 교재를 위해 직접 구성했습니다.