요약

  • Edinburgh LCF에서는 프로그래밍 가능한 택틱이 목표로부터 역방향으로 탐색할 수 있었지만, 성공한 탐색이라도 보호된 추론 규칙으로 구성된 검증(validation)을 통과해야 했습니다. 택틱이 실패하거나 잘못되더라도 정리(theorem) 값을 만들어내는 두 번째 경로를 얻지는 못했습니다.
  • 정리 추상 타입은 정리 구성을 위해 직접 신뢰하는 코드의 양을 줄였습니다. 그러나 이는 선택된 논리의 무결성, 명세의 충실성, 그리고 추상화 아래에 있는 컴파일러·런타임·하드웨어의 정확성을 증명하지는 못했습니다.
  • 이 역사는 협업의 산물입니다. Dana Scott이 기반 논리를 제공했고, Stanford LCF가 Edinburgh LCF에 앞섰으며, Michael Gordon, Christopher Wadsworth, Lockwood Morris, Malcolm Newey와 더 넓은 연구 공동체가 시스템과 그 메타언어 구축에 기여했습니다. 이후의 정리 증명기들은 하나의 동일한 구조를 공유하기보다 이 아이디어를 계승하면서 변형시켰습니다.

마지막 단계는 그 이전의 모든 단계와 다릅니다

자동화된 택틱이 하나의 목표를 여러 하위 목표로 전개하고, 다시 쓰기를 시도하며, 되돌아가기(backtracking)를 수행하고, 전략들을 결합한다고 상상해 보십시오. 그 흔적은 길고 설득력 있을 수 있고, 심지어 모든 분기가 처리되었다는 메시지로 끝날 수도 있습니다. 그러나 그러한 사건들 자체는 결과를 LCF적 의미의 정리로 만들어 주지 못합니다.

전환은 그 이후에 일어납니다. 택틱은 검증(validation)을 반환하는데, 이는 제안된 하위 목표들에 대한 정리 값을 받아 원래 목표의 정리를 만들어 내는 함수입니다. 하위 목표들이 증명된 뒤에 이 검증은 보호된 정리 인터페이스를 통해 순방향 추론을 수행합니다. 그렇게 하지 못한다면, 탐색 기록이 아무리 매력적이어도 탐색은 승인을 얻지 못한 것입니다.

이 구분은 어려운 설계 문제에 대한 실용적 답변이었습니다. 대화형 증명기는 사용자가 새로운 증명 방법을 표현할 수 있을 만큼 확장 가능해야 합니다. 그런 방법은 복잡하고, 실험적이며, 오류를 포함할 수 있습니다. 그러나 모든 새 절차에 정리 생성 권한을 무제한으로 주면 확장할 때마다 신뢰하는 표면이 커집니다. 대신 LCF는 정리 구성을 통상thm으로 불리는 추상 타입 뒤에 두었습니다. 공리와 원시 추론 규칙만이 그 타입의 값을 반환할 수 있는 연산이었습니다.

이 구조는 택틱을 올바르게 만들지는 않습니다. 택틱은 부적절한 하위 목표를 고르거나, 무한히 실행되거나, 예외를 던지거나, 약속된 결론을 내놓지 않는 검증을 제공할 수 있습니다. Larry Paulson의 회고적 서술은 그 가능성을 명시적으로 인정합니다. 중요한 부정적 권한은 더 좁습니다. 평범한 코드는 자신의 탐색 절차가 정교하다는 이유만으로 별도의 생성자를 얻지 못합니다. 오류는 보통 요청한 정리를 얻지 못하는 실패로 나타나며, 정리를 만들 권한으로 나타나지 않습니다.

증명 검사기에서 프로그래밍 가능한 증명기로

Milner의 1972년 서술은 Dana Scott의 Logic for Computable Functions에 대해 구현된 증명 검사기를 다뤘습니다. Stanford의 그 작업이 무대를 마련했지만, 긴 증명은 심각한 비용을 드러냈습니다. 저수준 검사는 번거로웠고, 완전한 증명 이력을 유지하는 것은 당시의 기계에 큰 부담이었습니다. Milner가 1973년 Edinburgh로 옮긴 뒤, 이 프로젝트는 더 프로그래밍 가능한 환경을 발전시켰습니다.

정사(正史)는 단독 발명가 서사가 아닙니다. 1979년의 책Edinburgh LCF는 Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth의 저작입니다. 1978년의 메타언어 논문에는 Lockwood Morris와 Malcolm Newey도 이름을 올리고 있습니다. Paulson의 역사적 논평은 이 협력자들과 그 순서를 기록하고, Gordon 자신의 서술은 이전의 Stanford 시스템을 Edinburgh 작업과, 다시 HOL과 연결합니다. Dana Scott의 논리가 기계화의 원래 대상을 제공했습니다.

ML—원래 “Meta Language”—는 증명 절차를 프로그래밍 가능하게 만들었습니다. 항(term), 논리식, 목표, 전략을 데이터와 함수로 다룰 수 있었습니다. Milner의 다형적 타입 체계는 이후 의미론적·통사적 건전성 결과와 Algorithm W로 분석되었고, 그 자체로 프로그래밍 언어 분야의 주요 기여가 되었습니다. 그러나 역사적 공로는 정확하게 두어야 합니다. LCF, ML, 택틱 설계, 대화형 정리 증명은 팀과 연구 공동체를 통해 성장했으며, 다만 Milner의 구조적 통찰이 너무 중심적이라 그의 1991년 ACM Turing Award 시상 근거의 일부가 되었습니다.

순방향 추론과 역방향 탐색은 이후 서로 다른 역할을 맡았습니다. 추론 규칙은 정리 값을 소비하여 정리 값을 반환합니다. 택틱은 목표를 보고 하위 목표를 제안하며, 그 검증은 하위 목표들에 대한 정리 값으로 목표의 정리를 어떻게 조립할 수 있는지를 기록합니다. 택티컬(tactical)—순서화, 반복, 선택을 위한 고차 조합자—은 택틱을 조직합니다. 택티컬은 보호된 구성 경계 밖에서 표현력을 높이는 것이며, 추가적인 공리가 아닙니다.

이 분리 덕분에 거대한 탐색 절차는 정리 생성자와 같은 방식으로 신뢰될 필요가 없습니다. 승인 인터페이스가 비교적 안정적으로 유지되는 동안 탐색 코드는 교체되거나, 조정되거나, 폐기될 수 있습니다. 유용한 유비는 “자동화는 안전하다”가 아니라 “자동화는 제안할 수 있으나, 더 작은 인터페이스만이 영속적인 타입을 부여할 수 있다”입니다.

추상 타입이 주는 것

추상 데이터 타입은 자신의 표현을 숨기고 선별된 연산만 노출합니다. 정리에 이 아이디어를 적용하면, 사용자 코드는 정리 값을 가지고 허가된 함수에 전달할 수 있되, 내부 필드를 편집해 다른 값을 만들어 낼 수 없습니다. 언어의 타입 추상화가 이 경계를 단속합니다.

보장의 이득은 구조적입니다. 검토는 지금까지 작성된 모든 택틱이 아니라 더 작은 공리·추론 규칙 구현의 모음에 집중될 수 있습니다. 새로운 자동화는 최종 산물이 공통 경로를 반드시 거쳐야 한다는 조건 아래 풍성해질 수 있습니다. 복잡한 코드의 양이 더 이상 정리 값의 존재를 직접 결정하는 코드의 양과 동일하지 않게 됩니다.

그러나 “작은 커널”을 “신뢰 불필요”로 낭만화해서는 안 됩니다. 첫째, 공리와 규칙은 의도된 논리에 대해 실제로 건전해야 합니다. 추상 타입은 우회를 막지만, 원시 규칙이 올바르게 선택되고 구현되었는지를 증명하지는 않습니다. 둘째, 타입 추상화는 구현이 그것을 보존하는 데 의존합니다. 컴파일러 결함, 안전하지 않은 탈출구, 런타임 오류, 하드웨어 오류는 논리적 인터페이스 아래에 있습니다. 셋째, 저장된 정리 값이 올바르게 구성되었더라도 파서와 프린터는 사용자를 오도할 수 있습니다. 신뢰 기반은 좁혀지는 것이지 폐지되는 것이 아닙니다.

커널의 건전성이 논리적 무결성과 같지도 않습니다. 건전한 원시 규칙은 의미론이나 형식적 설명에 상대적으로 타당성을 보존할 뿐이고, 무결성 주장은 모순이 유도 가능한지를 다룹니다. 이 관계는 추상 타입만으로는 해소되지 않는 전제에 의존합니다. “이 값은 이 함수들로만 만들어질 수 있다”는 것은 구성에 관한 출처(provenance) 주장이지, 모든 함수가 타당한 규칙을 구현한다는 독립된 증명이 아닙니다.

같은 주의는 증명과 명세를 분리합니다. 모델에 대한 정리는 그 형식화 안에서의 결과를 확립할 뿐, 모델이 의도된 시스템, 환경, 위협, 규제, 인간의 결정을 담아낸다는 것을 확립하지 않습니다. 명세가 실제 제약을 빠뜨렸다면, 완벽한 커널은 잘못된 형식적 질문을 완벽하게 증명할 수 있습니다. 검증은 명시된 계약을 강화할 뿐, 빠져 있는 의도를 공급하지 못합니다.

왜 검증이 경첩인가

검증 함수는 흔히 일반적인 “검사”로 평평하게 만들어지지만, 그 역할은 더 정확합니다. 택틱은 역방향 변환을 수행합니다. 하나의 목표에서 하위 목표의 목록으로. 검증은 순방향으로 진행합니다. 하위 목표들에 대한 정리 값이 주어지면 원래 목표의 정리를 구성합니다. 따라서 역방향 탐색은 성공이 어떻게 정당화될지에 대한 미이행된 설명을 함께 지니고 갑니다.

이것은 증명 상태 전이를 인터페이스의 시각적 변화 이상으로 만듭니다. 단지 목표를 지우는 절차는 그것을 증명한 것이 아닙니다. 빈 하위 목표 목록을 반환하는 절차는 발명된 전제 없이 목표의 정리를 산출할 수 있는 검증도 함께 제공해야 합니다. 약속된 조립이 무효라면 최종 순방향 구성은 실패합니다.

택티컬은 전략을 조합하면서도 이 규율을 보존합니다. 순차 택티컬은 한 택틱을 적용한 뒤 그 결과 하위 목표에 또 다른 택틱을 적용할 수 있고, 반복 택틱은 진전이 가능한 동안 계속할 수 있습니다. 그 조합은 검증도 함께 조합해야 합니다. 제어 계층은 정교해질 수 있지만, 승인 근거는 그 구조를 따라 원시 추론 연산까지 거슬러 올라갑니다.

이것이 도입부 장면의 요점입니다. 탐색 로그, 초록 상태 표시, 다듬어진 스크립트는 유용한 기록이지만 정리 값 자체는 아닙니다. 현대 공학 언어로 말하면, 활동 증거와 승인 권한이 의도적으로 분리된 것입니다. 그 경계는 계산량에 좌우되지 않고, 보호된 생성자가 수용된 전제로부터 주장된 결론을 재현할 수 있는지를 묻습니다.

후손들은 관련되어 있으되 동일하지는 않다

LCF 접근은 넓은 증명기 계보에 영향을 주었습니다. Gordon은 이 구조적 계보를 HOL로 이어갔고, Paulson은 Cambridge LCF를 거쳐 Isabelle을 발전시켰습니다. Cambridge의 HOL Light 소개는 여전히 건전성이 작은 신뢰 코어에 의존하는 확장 가능한 시스템으로 이를 서술합니다. 이들은 진짜 후손입니다.

계승이 동일성을 뜻하지는 않습니다. Paulson의 Isabelle 서술에 따르면 Isabelle은 규칙과 증명 상태가 하나의 표현을 공유하며, 그 순방향·역방향 추론은 고전적 LCF의 규칙당 하나의 함수라는 설계와 다른 원리에 기반합니다. 구성적 타입 이론에 기반한 시스템은 증명 항을 유지하고 타입 검사기를 다른 방식으로 신뢰할 수 있습니다. 일부 시스템은 독립 검사를 위해 인증서를 내보냅니다. LCF 전통 내에서도 안전하지 않은 기능, 증명 기록, 커널 언어, 재검사에 대한 선택이 신뢰 기반을 바꿉니다.

따라서 신중한 주장은 역사적이고 구조적인 것입니다. Milner와 Edinburgh 팀은 강한 타입 추상화가 확장 가능한 증명 탐색과 보호된 정리 구성을 어떻게 분리하는지 보여 주었습니다. 많은 이후 시스템이 그 교훈을 조정했습니다. 모든 현대 증명 보조 도구가 동일한 작은 커널을 구현한다거나, 택틱의 사용 자체가 LCF 구조를 식별한다고 말하는 것은 부정확합니다.

출처와 한계

이 글은 원저 논문, 대학 기록 보관소, 기술적 회고를 사용합니다. 현재 운용 중인 증명기를 감사하거나 측정된 커널 크기를 주장하지는 않습니다. 마지막 거버넌스 비유—공통 승인 규칙을 최소한으로, 검증 가능하게 유지하면서 미래의 탐색 방법은 개방적으로 두라는 것—는 Lu Heng의 최소 초기 명세 원리에서 영향을 받은 편집적 독해이며, Milner의 정치적·제도적 견해에 대한 주장이 아닙니다.