커리-하워드 대응(Curry-Howard Correspondence)은 컴퓨터 프로그램과 수학적 증명 사이의 동형성(isomorphism)을 말한다. "명제는 타입이고, 증명은 프로그램이다"라고 요약된다.
핵심 대응표
| 논리 | 타입 이론 | 프로그래밍 |
|---|
| 명제 | 타입 | 타입 선언 |
| 증명 | 항(Term) | 프로그램/값 |
| P → Q | P → Q | 함수 타입 |
| P ∧ Q | P × Q | 곱 타입(튜플) |
| P ∨ Q | P + Q | 합 타입(Either) |
| ⊥ (거짓) | Void | 빈 타입 |
| ⊤ (참) | Unit | Unit 타입 |
| ∀x.P(x) | Πx:A.P(x) | 의존 함수 타입 |
| ∃x.P(x) | Σx:A.P(x) | 의존 쌍 타입 |
구현 예시 (Haskell)
haskell
-- P → Q (함수 타입)
-- 증명: "A이면 B" = A 타입 값을 받아 B 타입 값을 반환하는 함수
modus_ponens :: (a -> b) -> a -> b
modus_ponens f x = f x -- 증명 = 프로그램
-- P ∧ Q (곱 타입)
-- 증명: P의 증명과 Q의 증명을 함께 제공
data And p q = And p q -- (p, q)
and_intro :: p -> q -> And p q
and_intro = And
-- P ∨ Q (합 타입)
data Or p q = InL p | InR q -- Either
or_intro_l :: p -> Or p q
or_intro_l = InL
-- ¬P = P → ⊥
type Not p = p -> Void
배중률과 계속
고전 논리: P ∨ ¬P (배중률)
직관 논리: 증명 불가
계속(Continuation)과의 연결:
callcc :: ((a -> b) -> a) -> a
-- callcc가 있으면 고전 논리 명제 증명 가능
-- Peirce의 법칙: ((P→Q)→P)→P ↔ callcc
증명 보조기 (Proof Assistants)
Coq (갈리나 언어):
Theorem plus_comm : forall n m : nat,
n + m = m + n.
Proof.
intros n m.
induction n.
- simpl. rewrite <- plus_n_O. reflexivity.
- simpl. rewrite <- IHn. rewrite plus_n_Sm. reflexivity.
Qed.
Agda: 의존 타입 활용 증명
Lean 4: 수학 증명 자동화
관련 개념
