의존형을 왜 사용하지 않는가

• 의존형(type theory) 은 증명 객체를 포함하지만, 저자는 이를 불필요하고 비효율적인 구조로 평가함
• AUTOMATH와 Martin-Löf 형식 체계 등 과거 의존형 기반 시스템을 직접 연구했으나, Isabelle은 일반적(generic) 논리 프레임워크로 발전함
• 단순형 이론(higher-order logic) 을 기반으로 한 Isabelle/HOL은 자동화·대규모 라이브러리·가독성에서 강점을 보임
• ALEXANDRIA 프로젝트를 통해 고차 논리만으로도 고급 수학 정리의 형식화가 가능함을 입증
• Lean 등 의존형 시스템의 성숙에도 불구하고, 성능 문제와 복잡성 때문에 저자는 여전히 고차 논리 접근법의 실용성을 선호함

의존형과 증명 객체

• 의존형 이론에서는 증명 객체(proof objects) 가 필수적이지만, 저자는 이를 공간 낭비로 간주
  • LCF 구조에서는 논리 내부가 아닌 구현 언어 수준의 타입 검사로 정당한 증명 단계만 실행 가능
  • Robin Milner의 통찰로 proof kernel 개념이 도입되어 Isabelle의 기반이 됨
• 저자는 “의존형을 사용하지 않았다”는 질문에 대해 “오랫동안 사용했다”고 답함

AUTOMATH 경험

• 1977년 Caltech에서 N. G. de Bruijn의 AUTOMATH 강의를 들었으며, 시스템 자체는 직접 사용하지 못함
  • 당시 Eindhoven 대학 시스템이 ARPAnet에 연결되지 않았고, ALGOL 60 기반 컴퓨터가 필요했기 때문
• AUTOMATH는 의존형 시스템이지만 Curry–Howard 대응을 구현하지 않음
  • 사용자가 원하는 논리의 기호와 추론 규칙을 공리로 추가해야 했음
  • de Bruijn은 이를 “모든 음식을 제공하는 큰 레스토랑”에 비유
• Isabelle은 이 개념을 이어받아 논리 프레임워크로서의 일반성을 추구
  • 그러나 de Bruijn은 집합론을 혐오하고 수학을 본질적으로 타입 기반으로 보았음
• 저자는 AUTOMATH의 정당성 검증을 질문했고, de Bruijn은 언어 이론서(300쪽) 를 보냈으나 만족스럽지 않았음

Martin-Löf 형식 이론

• Göteborg의 Chalmers 대학에서 Martin-Löf 형식 이론을 연구하며 프로그램 합성 가능성에 매료됨
  • Heyting의 직관주의 논리 원리를 직접 구현한 점에서 “옳음”이 명확하다고 평가
• 수년간 연구를 진행하며 Isabelle의 초기 버전을 Martin-Löf 이론으로 구현
  • 현재도 Isabelle/CTT로 배포에 포함됨
• 그러나 Per Martin-Löf 중심의 교조적 분위기와 강제된 내재적 동치(intensional equality) 전환으로 연구가 무너짐
• 이후 등장한 Calculus of Constructions(CoC) , Rocq, Lean 등도 같은 의문을 남김
  • CoC는 수십 년간 여러 변형과 선택적 공리를 거듭함

연구 선택과 Isabelle의 방향

• 연구자들은 새로운 형식 체계 개발과 기존 체계의 확장 활용 중 선택해야 함
  • Isabelle은 일반화된 프레임워크로 설계되어 다양한 논리를 수용
• 1985년 Mike Gordon은 Church의 단순형 이론으로 하드웨어 검증을 수행
  • 이후 John Harrison이 벡터 차원 인코딩을 고안
• Isabelle/HOL은 Church 이론에 공리적 타입 클래스와 locale 모듈 시스템을 추가
• Lean 커뮤니티는 CoC 기반으로 방대한 수학 형식화(mathlib) 를 달성

ALEXANDRIA 프로젝트와 고차 논리의 한계 실험

• ERC 지원 ALEXANDRIA 프로젝트는 Isabelle의 자동화·라이브러리·가독성을 강조
• 초기에는 고차 논리로는 한계가 있을 것이라 예상했으나, 실제로는 Grothendieck 스킴 등 고급 수학도 성공적으로 형식화
  • Paulo Emílio de Vilhena와 Martin Baillon이 모든 체가 대수적으로 닫힌 확장을 가짐을 증명
• 프로젝트는 Balog–Szemerédi–Gowers 정리 등 고급 결과까지 확장
  • “의존형 없이는 수학 형식화가 불가능하다”는 주장은 사라지고, “의존형이 더 깔끔하다”는 주장만 남음

Lean과 의존형에 대한 현재 입장

• Lean의 커뮤니티 규모와 Blueprint 도구는 부럽지만, 성능 문제와 복잡성은 여전
  • intensional equality와의 충돌, 의존형 사용 시기 판단의 어려움이 반복적으로 보고됨
• 저자는 의존형을 Tesla의 완전자율주행(Full Self-Driving) 에 비유하며, 과도한 기대와 실제 불편함을 지적

부록: 고차 논리의 이론적 한계

• 일부에서는 고차 논리가 증명 이론적으로 약하다고 주장하지만, 이는 ZF 집합론 대비 약함을 의미할 뿐
• ALEXANDRIA 결과에 따르면, 고차 논리로도 Grothendieck 스킴 등 복잡한 수학 구조를 다룰 수 있음
  • 단 두 개의 증명만이 ZF 공리 추가를 필요로 했으며, 이는 ZF 객체를 직접 언급하는 정리였음

각주

• 직관주의는 언어를 단순한 기록 수단으로 보는 철학으로, 오늘날의 구성적 수학(constructive mathematics) 과는 다름