커리-하워드 대응

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요
2. 역사적 기원 및 발전
3. 일반적인 공식화
- 3.1. 논리식과 타입 수준의 대응
- 3.2. 증명 시스템과 계산 모델 수준의 대응
4. 대응하는 시스템
5. 관련 증명-프로그램 대응
6. 한국의 관점 및 영향
- 6.1. 주요 인물
- 6.2. 주요 사건
7. 추가 연구 및 응용 분야
참조

1. 개요

커리-하워드 대응은 형식적인 증명 시스템과 타입 시스템 간의 관계를 설명하는 개념으로, 논리식과 데이터 타입, 수학적 증명과 컴퓨터 프로그램 사이의 대응 관계를 보여준다. 이 대응은 1934년 해스켈 커리의 연구에서 시작되었으며, 1969년 윌리엄 하워드에 의해 자연 연역과 람다 계산 사이의 구문론적 유추가 명확하게 제시되면서 발전했다. 커리-하워드 대응은 힐베르트식 연역 시스템과 조합 논리, 자연 연역과 람다 계산 사이의 구조적 동일성을 보여주며, 고전 논리, 선형 논리, 호모토피 타입 이론, 유전자 프로그래밍 등 다양한 분야에 응용된다.

더 읽어볼만한 페이지

1969년 컴퓨팅 - 관계형 모델
관계형 모델은 에드거 F. 코드가 제안한 2차원 테이블 형태의 데이터 모델로, 튜플과 속성으로 데이터를 구성하며 관계 대수 또는 관계 논리를 통해 데이터 연산을 수행하고 SQL의 기반이 된다.
1969년 컴퓨팅 - 호어 논리
호어 논리는 프로그램의 실행 전후 조건을 명시하고 코드 조각이 조건을 어떻게 변화시키는지 추론하는 규칙을 제공하여 프로그램의 정확성을 형식적으로 검증하는 논리 시스템이다.

커리-하워드 대응

2. 역사적 기원 및 발전

해스켈 커리의 조합 논리 연구와 윌리엄 앨빈 하워드의 자연 연역과 람다 계산 간의 관계 연구는 커리-하워드 대응의 기원이다.

1934년 커리는 조합자의 타입이 직관주의 함축 논리에 대한 공리 체계로 간주될 수 있음을 보였다. 1958년에는 힐베르트식 연역 시스템이 조합 논리의 타입 지정된 조각과 일치한다는 것을 발견했다. 1969년 하워드는 자연 연역이 람다 계산의 타입 지정된 변형으로 해석될 수 있음을 보였다.^[2]

이러한 관찰들은 증명 시스템과 계산 모델 사이에 동형성이 존재한다는 커리-하워드 대응의 핵심 아이디어로 이어졌다.

2. 1. 커리의 초기 연구 (1934년)

1934년 해스켈 커리는 조합자의 타입이 직관주의 함축 논리에 대한 공리 체계로 간주될 수 있다는 것을 관찰했다.

2. 2. 커리의 추가 연구 (1958년)

해스켈 커리는 1958년에 힐베르트식 연역 시스템으로 알려진 특정 종류의 증명 계산(증명 시스템)이 조합 논리로 알려진 표준 계산 모델의 타입이 지정된 조각과 일부 일치한다는 것을 관찰했다.

이는 직관 논리와의 대응에 있어서 제한사항으로, 고전 논리의 항진식인 퍼스의 법칙 ((\alpha \to \beta)\to \alpha) \to \alpha 와 같은 식은 이 대응에서 제외된다는 것을 의미한다.

논리	프로그래밍
$\frac{\alpha \in \Gamma}{\Gamma \vdash \alpha} \text{Assum}$	$\frac{x:\alpha \in \Gamma}{\Gamma \vdash x:\alpha}$
$\frac{}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha)} \text{Ax}_K$	$\frac{}{\Gamma \vdash K: \alpha \rightarrow (\beta \rightarrow \alpha)}$
$\frac{}{\Gamma \vdash (\alpha\!\rightarrow\!(\beta\!\rightarrow\!\gamma))\!\rightarrow\!((\alpha\!\rightarrow\!\beta)\!\rightarrow\!(\alpha\!\rightarrow\!\gamma))}\text{Ax}_S$	$\frac{}{\Gamma \vdash S: (\alpha\!\rightarrow\!(\beta\!\rightarrow\!\gamma))\!\rightarrow\!((\alpha\!\rightarrow\!\beta)\!\rightarrow\!(\alpha\!\rightarrow\!\gamma))}$
$\frac{\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha}{\Gamma \vdash \beta}\text{Modus Ponens}$	$\frac{\Gamma \vdash E_1:\alpha \rightarrow \beta \qquad \Gamma \vdash E_2:\alpha}{\Gamma \vdash E_1\;E_2:\beta}\text{Application}$

더 추상적인 레벨에서 보면, 이 대응은 다음 표와 같이 다시 나타낼 수 있다.

논리	프로그래밍
가정	변수
공리	콤비네이터
모더스 포넨스	함수 적용
연역 정리	추상 제거

2. 3. 하워드의 연구 (1969년)

윌리엄 앨빈 하워드는 1969년에 자연 연역이라는 증명 시스템이 직관주의 버전의 람다 계산이라는 계산 모델로 해석될 수 있음을 발견했다.^[2] 이는 단순하게 형식화된 람다 계산과 자연 연역 간의 구문적 동형성을 보여주는 것이었다.

하워드는 자연 연역의 함의 단편을 형식화하고, 람다 계산의 타입 지정 규칙을 다음과 같은 표로 나타냈다.

논리	프로그래밍
$\frac{}{\Gamma_1, \alpha, \Gamma_2 \vdash \alpha} \text{Ax}$	$\frac{}{\Gamma_1, x:\alpha, \Gamma_2 \vdash x:\alpha}$
$\frac{\Gamma, \alpha \vdash \beta}{\Gamma \vdash \alpha \rightarrow \beta} \rightarrow I$	$\frac{\Gamma, x:\alpha \vdash t:\beta}{\Gamma \vdash \lambda x.t : \alpha \rightarrow \beta}$
$\frac{\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha}{\Gamma \vdash \beta} \rightarrow E$	$\frac{\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha}{\Gamma \vdash t\;u:\beta}$

이 표에서 $\Gamma,\Gamma_{1},\Gamma_{2}$ 는 논리식의 열을 나타내고, 우변에서는 람다 항으로 이름 붙여진 논리식 열을 나타낸다. 이 대응에 따르면, $\Gamma \vdash \alpha$ 를 증명하는 것은 타입 선언 열 $\Gamma$ 아래에서 타입 $\alpha$ 를 갖는 객체를 구성하는 것에 해당한다. 여기서 공리는 새 변수 도입(및 타입 선언)에, → I 규칙은 함수 추상화에, → E 규칙은 함수 적용에 대응된다.

하워드는 또한 다른 논리 결합자와 단순하게 형식화된 람다 항의 다른 구성 간의 대응을 확장할 수 있음을 보였다. 예를 들어 논리곱과의 대응은 다음과 같다.

논리	프로그래밍
$\frac{\Gamma \vdash \alpha \qquad \Gamma \vdash \beta}{\Gamma \vdash \alpha \wedge \beta}\wedge I$	$\frac{\Gamma \vdash t:\alpha \qquad \Gamma \vdash u:\beta}{\Gamma \vdash \langle t,u\rangle:\alpha \times \beta}$
$\frac{\Gamma \vdash \alpha_{1}\wedge\alpha_{2}}{\Gamma \vdash \alpha_{i}}\wedge E$	$\frac{\Gamma \vdash t:\alpha_{1}\wedge\alpha_{2}}{\Gamma \vdash \pi_{i}t:\alpha_{i}}$

더 추상적으로 보면, 이 대응은 다음과 같이 요약될 수 있다.

논리	프로그래밍
공리	변수
도입 규칙	생성자
제거 규칙	소멸자
정규 증명	정규 람다 항
증명의 정규화	람다 항의 약정규화
증명 가능성	타입의 구체성의 문제(type inhabitation problem)
직관 논리의 항진식	구체 타입(inhabited type)

2. 4. 드 브라윈의 역할

니콜라스 고베르트 드 브라윈은 오토마스(Automath)의 정리 검증기에 대한 증명을 나타내기 위해 람다 표기법을 사용했으며, 명제를 해당 증명의 "범주"로 나타냈다.^[6] 이는 하워드가 그의 원고를 작성했던 시기와 같은 1960년대 후반이었으며, 드 브라윈은 하워드의 연구를 알지 못했고, 독립적으로 대응 관계를 언급했다.^[6] 일부 연구자들은 커리-하워드 대응 대신 커리-하워드-드 브라윈 대응이라는 용어를 사용하기도 한다.^[6]

3. 일반적인 공식화

커리-하워드 대응은 증명 계산과 계산 모델의 형 시스템 간의 대응 관계이다.^[6] 이는 크게 두 가지 관점으로 나뉜다. 하나는 논리식과 형 수준의 대응으로, 특정 증명 체계나 계산 모델에 국한되지 않는다. 다른 하나는 형식적 증명과 프로그램 수준의 대응으로, 증명 체계 및 계산 모델의 선택에 따라 달라진다.

논리식과 형 수준의 대응, 그리고 증명 시스템과 계산 모델 수준의 대응은 각각 하위 섹션에서 더 자세히 설명한다.

3. 1. 논리식과 타입 수준의 대응

커리-하워드 대응은 논리식과 타입 수준에서 다음과 같이 대응된다.

논리 측면	프로그래밍 측면
수식	타입
증명	항
수식이 참임	타입에 요소가 있음
수식이 거짓임	타입에 요소가 없음
논리 상수 ⊤ (진리)	단위 타입
논리 상수 ⊥ (거짓)	빈 타입
논리적 함의	함수 타입
논리적 결합	곱 타입
논리적 분리	합 타입
전칭 양화사	종속 곱 타입
존재 양화사	종속 합 타입

이는 논리적 함의가 함수 타입과 동일하게 작동하고, 논리적 결합이 곱 타입(튜플, 구조체, 목록 등 언어에 따라 다르게 불림), 논리적 분리가 합 타입(공용체라고도 불림), 거짓 수식이 빈 타입, 참 수식이 단위 타입(유일한 멤버는 널 객체)으로 작동한다는 것을 의미한다. 정량자는 종속 타입 함수 공간 또는 곱에 해당한다.

3. 2. 증명 시스템과 계산 모델 수준의 대응

커리-하워드 대응에서 증명 시스템과 계산 모델 수준의 대응은 주로 다음과 같다.

논리 측면	프로그래밍 측면
힐베르트식 연역 시스템	조합 논리에 대한 타입 시스템
자연 연역	람다 계산에 대한 타입 시스템

자연 연역 시스템과 람다 계산 사이에는 다음과 같은 대응이 있다.

논리 측면	프로그래밍 측면
가설	자유 변수
함의 제거 (modus ponens)	적용
함의 도입	추상화

BHK 해석은 직관주의적 증명의 함의와 전칭화를 함수로 해석하지만, 해석에서 함수의 클래스가 어떤 것인지는 지정하지 않는다. 만약 함수의 클래스로 람다 계산을 취한다면, BHK 해석은 자연 연역과 람다 계산 사이의 대응과 같은 것을 말한다.

4. 대응하는 시스템

커리-하워드 대응은 증명 시스템과 계산 모델 사이에 동형성이 존재한다는 관찰에 기반한다. 이는 두 형식 체계가 본질적으로 동일하다는 것을 의미한다.

일반적으로 "증명은 프로그램이고, 증명하는 공식은 프로그램의 타입이다"라고 요약할 수 있다.^[6] 함수의 반환 타입이 논리적 정리와 유사하고, 함수를 계산하는 프로그램은 정리의 증명과 유사하다는 비유로 이해할 수 있다. 이는 논리 프로그래밍의 엄격한 기반을 제공하며, 증명이 프로그램(특히 람다 항)으로 표현되거나 실행될 수 있음을 보여준다.

커리-하워드 대응은 증명 계산과 타입이 지정된 함수형 프로그래밍 언어 모두로 작동하도록 설계된 새로운 종류의 형식 시스템 연구로 이어졌다. 마틴-뢰프의 직관주의적 타입 이론과 코캉의 구성의 계산이 대표적인 예시이며, 이들 시스템에서 증명은 일반적인 객체로 취급되고 프로그램처럼 속성을 가질 수 있다. 이러한 연구 분야는 현대 타입 이론으로 불린다.

커리-하워드 패러다임에서 파생된 타입이 지정된 람다 계산은 Coq과 같은 소프트웨어 개발로 이어졌으며, 여기서 증명은 프로그램으로 형식화, 검사 및 실행될 수 있다.

프로그램의 프로그램 정확성이 주어지면, 프로그램을 사용하여 증명을 추출하는 연구도 진행 중이다. 이는 증명 휴대 코드와 밀접하게 관련되며, 프로그래밍 언어의 타입 시스템이 풍부해야 가능하다. 이러한 타입 시스템 개발은 커리-하워드 대응을 실질적으로 활용하려는 노력의 일환이다.

커리-하워드 대응은 원래 다루지 않았던 증명 개념의 계산적 내용에 대한 새로운 질문을 제기했다. 고전 논리는 프로그램의 지속을 조작하는 능력과 시퀀트 계산의 대칭성을 보여주며, 이는 호출 방식과 값에 의한 호출이라는 두 가지 평가 전략 간의 이중성을 나타낸다.

튜링 완전 계산 모델은 종료되지 않는 프로그램을 작성할 수 있기 때문에, 단순하게 대응을 적용하면 일관성이 없는 논리로 이어질 수 있다. 논리적 관점에서 임의의 계산을 처리하는 방법은 여전히 연구 중이며, 모나드를 사용하여 증명 가능한 종료 코드와 잠재적으로 종료되지 않는 코드를 분리하는 접근 방식이 있다. 더 급진적인 접근 방식은 전체 함수형 프로그래밍에서 옹호하는 것으로, 무제한 재귀를 제거하고 코재귀를 사용한다.

커리-하워드 대응은 공식적인 증명 계산과 타입 시스템 사이의 계산 모델에 대한 대응으로 확장될 수 있다. 수식과 타입 수준, 증명과 프로그램 수준의 두 가지 대응으로 나뉜다.

수식과 타입 수준의 대응은 다음과 같이 요약할 수 있다.

논리 측면	프로그래밍 측면
수식	타입
증명	항
수식이 참임	타입에 요소가 있음
수식이 거짓임	타입에 요소가 없음
논리 상수 ⊤ (진리)	단위 타입
논리 상수 ⊥ (거짓)	빈 타입
논리적 함의	함수 타입
논리적 결합	곱 타입
논리적 분리	합 타입
전칭 양화사	종속 곱 타입
존재 양화사	종속 합 타입

증명 시스템과 계산 모델 수준의 대응은 주로 힐베르트식 연역 시스템과 조합 논리, 자연 연역과 람다 계산 사이의 구조적 동일성을 보여준다.

논리 측면	프로그래밍 측면
힐베르트식 연역 시스템	조합 논리에 대한 타입 시스템
자연 연역	람다 계산에 대한 타입 시스템

자연 연역과 람다 계산 사이의 대응 관계는 다음과 같다.

논리 측면	프로그래밍 측면
가정	자유 변수
함의 제거 규칙 (모두스 포넨스)	함수 적용
함의 도입 규칙	람다 추상

4. 1. 직관주의 힐베르트식 연역 시스템과 타입이 지정된 조합 논리

1958년 커리와 페이스(Feys)의 결합자 논리에 관한 책에서 결합자 논리의 기본 결합자인 K와 S의 가장 단순한 유형이 힐베르트 형식 연역 시스템에서 사용되는 공리 체계인 ''α'' → (''β'' → ''α'') 및 (''α'' → (''β'' → ''γ'')) → ((''α'' → ''β'') → (''α'' → ''γ''))에 각각 해당한다는 언급이 있었다. 이러한 이유로 이 체계는 현재 종종 공리 K와 S라고 불린다.

함축적 직관주의적 단편으로 제한하면, 힐베르트 형식 논리는 다음과 같이 공식화할 수 있다. Γ를 가설로 간주되는 공식의 유한 집합이라고 할 때, δ가 다음 조건 중 하나를 만족하면 Γ에서 ''유도 가능''하며, Γ ⊢ δ로 표시한다.

δ는 가설, 즉 Γ의 공식이다.
δ는 공리 체계의 인스턴스이다.
* δ는 ''α'' → (''β'' → ''α'') 형태이거나,
* δ는 (''α'' → (''β'' → ''γ'')) → ((''α'' → ''β'') → (''α'' → ''γ'')) 형태이다.
δ는 연역에 의해 따른다. 즉, 어떤 ''α''에 대해 ''α'' → ''δ''와 ''α''가 이미 Γ에서 유도 가능하다 (이는 전건 긍정의 규칙이다).

이는 추론 규칙을 사용하여 다음과 같이 공식화할 수 있다.

유형화된 결합자 논리는 유사한 구문을 사용하여 공식화할 수 있다. Γ를 유형으로 주석이 달린 변수의 유한 집합이라고 할 때, 항 T(유형으로 주석이 달림)는 다음 조건 중 하나를 만족하면 이러한 변수에 의존한다[Γ ⊢ T:''δ''].

T는 Γ에 있는 변수 중 하나이다.
T는 기본 결합자이다.
* T는 K:''α'' → (''β'' → ''α'')이다[여기서 ''α''와 ''β''는 인수의 유형을 나타낸다].
* T는 S:(''α'' → (''β'' → ''γ'')) → ((''α'' → ''β'') → (''α'' → ''γ''))이다.
T는 Γ에 있는 변수에 의존하는 두 개의 하위 항의 합성이다.

여기에 정의된 생성 규칙은 아래 표와 같으며 커리는 단순히 두 열이 일대일 대응 관계에 있다는 것을 나타낸다. 직관 논리로의 대응의 제한은 고전 논리 항진명제와 같은 피어스 법칙((''α'' → ''β'') → ''α'') → ''α''가 대응에서 제외됨을 의미한다.

힐베르트 형식 함축적 직관 논리	유형화된 결합자 논리
$\frac{\alpha \in \Gamma}{\Gamma \vdash \alpha} \qquad\qquad\text{가정}$	$\frac{x:\alpha \in \Gamma}{\Gamma \vdash x:\alpha}$
$\frac{}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha)} \qquad\text{Ax}_K$	$\frac{}{\Gamma \vdash K: \alpha \rightarrow (\beta \rightarrow \alpha)}$
$\frac{}{\Gamma \vdash (\alpha\!\rightarrow\!(\beta\!\rightarrow\!\gamma))\!\rightarrow\!((\alpha\!\rightarrow\!\beta)\!\rightarrow\!(\alpha\!\rightarrow\!\gamma))}\;\text{Ax}_S$	$\frac{}{\Gamma \vdash S: (\alpha\!\rightarrow\!(\beta\!\rightarrow\!\gamma))\!\rightarrow\!((\alpha\!\rightarrow\!\beta)\!\rightarrow\!(\alpha\!\rightarrow\!\gamma))}$
$\frac{\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha}{\Gamma \vdash \beta}\quad\text{전건 긍정}$	$\frac{\Gamma \vdash E_1:\alpha \rightarrow \beta \qquad \Gamma \vdash E_2:\alpha}{\Gamma \vdash E_1\;E_2:\beta}$

더 추상적인 수준에서 보면, 대응 관계는 다음 표와 같이 다시 기술할 수 있다. 특히, 힐베르트 형식 논리에 특정한 연역 정리는 결합자 논리의 추상 제거 과정과 일치한다.

논리 측면	프로그래밍 측면
가정	변수
공리 체계	결합자
전건 긍정	적용
연역 정리	추상 제거

4. 2. 직관주의 자연 연역과 타입이 지정된 람다 계산

하스켈 커리가 힐베르트식 체계와 콤비네이터 논리의 구문적 대응을 강조한 후, 윌리엄 앨빈 하워드는 1969년에 단순하게 형식화된 람다 계산과 자연 연역 간의 구문적 동형성을 명확히 했다. 아래는 좌변에서 직관주의적 자연 연역의 함의 단편을 형식화하고, 우변에서 람다 계산의 타입 지정 규칙을 나타낸다. 좌변에서는

\Gamma,\Gamma_{1},\Gamma_{2}

로 정렬된 논리식 열을 나타낸다. 우변에서는 람다 항으로 이름 붙여진 논리식 열을 나타낸다.

논리	프로그래밍
$\frac{}{\Gamma_1, \alpha, \Gamma_2 \vdash \alpha} \text{Ax}$	$\frac{}{\Gamma_1, x:\alpha, \Gamma_2 \vdash x:\alpha}$
$\frac{\Gamma, \alpha \vdash \beta}{\Gamma \vdash \alpha \rightarrow \beta} \rightarrow I$	$\frac{\Gamma, x:\alpha \vdash t:\beta}{\Gamma \vdash \lambda x.t : \alpha \rightarrow \beta}$
$\frac{\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha}{\Gamma \vdash \beta} \rightarrow E$	$\frac{\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha}{\Gamma \vdash t\;u:\beta}$

이 대응을 다시 말하면, $\Gamma \vdash \alpha$ 를 증명하는 것은 타입 선언 열 $\Gamma$ 아래에서 타입 $\alpha$ 를 갖는 객체를 구성하는 것에 해당한다. 공리는 새로운 변수의 도입(과 그 타입 선언)에, → I 규칙은 함수 추상화에, → E 규칙은 함수 적용에 대응한다. 만약 좌변의 문맥 $\Gamma$ 를 단순한 논리식의 집합으로 간주한다면(암묵적인 축약과 약화를 인정한다면), 이 대응은 정확하지 않다. 예를 들어, $\Gamma$ 안에 람다 항 $\lambda x.\lambda y.x$ 와 $\lambda x.\lambda y.y$ 로 이름 붙여진 논리식 $\alpha \to \alpha \to \alpha$ 가 속해 있었다면, 우변에서는 이것들을 구분하지만, 좌변에서는 이것을 같은 것으로 간주한다.

하워드는 다른 논리의 결합자와 단순하게 형식화된 람다 항의 다른 구성 간에 대응을 확장할 수 있음을 보였다. 예를 들어 논리곱과의 대응은 다음에 나타내는 표와 같다.

논리	프로그래밍
$\frac{\Gamma \vdash \alpha \qquad \Gamma \vdash \beta}{\Gamma \vdash \alpha \wedge \beta}\wedge I$	$\frac{\Gamma \vdash t:\alpha \qquad \Gamma \vdash u:\beta}{\Gamma \vdash \langle t,u\rangle:\alpha \times \beta}$
$\frac{\Gamma \vdash \alpha_{1}\wedge\alpha_{2}}{\Gamma \vdash \alpha_{i}}\wedge E$	$\frac{\Gamma \vdash t:\alpha_{1}\wedge\alpha_{2}}{\Gamma \vdash \pi_{i}t:\alpha_{i}}$

좀 더 추상적으로 보면, 이 대응은 다음 표로 정리될 수 있다. 특히 람다 계산에서의 정규형의 개념은 자연 연역에서의 프라위츠의 정규 증명에 대응한다. 타입이 지정된 람다 항은 정규형을 갖는다는 결과(정규화 정리)는 자연 연역의 무모순성이나 논리합 분리 특성의 증명에 이용할 수 있다. 타입의 구체성의 문제의 결정 절차를 직관주의적인 증명 가능성의 결정 절차로 변환할 수 있다.

논리	프로그래밍
공리	변수
도입 규칙	생성자
제거 규칙	소멸자
정규 증명	정규 람다 항
증명의 정규화	람다 항의 약정규화
증명 가능성	타입의 구체성의 문제(type inhabitation problem)
직관 논리의 항진식	구체 타입(inhabited type)

하워드의 대응은 자연 연역 및 람다 계산의 확장에 대해서도 자연스럽게 연장할 수 있다.

커리-하워드 대응에 따르면, 타입이 지정된 표현은 해당 논리식의 증명으로 간주될 수 있다. 다음은 몇 가지 예시이다.

다음 그림은 $(\beta \to \alpha) \to (\gamma \to \beta) \to \gamma \to \alpha$ 의 자연 연역에서의 증명이다. 간단히 하기 위해 문맥 $\Gamma \vdash$ 는 생략했다.

$\dfrac{\dfrac{ \begin{matrix} {} \\ x:\beta\rightarrow \alpha \end{matrix} \quad \dfrac{y:\gamma\rightarrow\beta\quad z:\gamma}{yz:\beta} }{\dfrac{x\,(yz):\alpha}{\lambda z.x\,(yz):\gamma \rightarrow\alpha} } }{\dfrac{ \lambda y.\lambda z.x\,(yz):(\gamma \rightarrow \beta) \rightarrow \gamma \rightarrow \alpha}{\lambda x.\lambda y. \lambda z.x\,(yz):(\beta \rightarrow \alpha) \rightarrow (\gamma \rightarrow \beta) \rightarrow \gamma \rightarrow \alpha} }$

이 증명이 타입이 지정된 람다 항 $\lambda x.\lambda y.\lambda z.x(yz)$ 로 해석될 수 있다는 것은 명백하다. 또한, 앞서 언급한 $(\beta \to \alpha) \to (\gamma \to \beta) \to \gamma \to \alpha$ 의 힐베르트 방식의 증명은 자연 연역에서의 이 증명에 대해 추상 제거와 η-변환을 여러 번 사용함으로써 얻을 수 있다.

4. 3. 고전 논리와 제어 연산자

고전 논리는 프로그램의 지속을 조작하는 능력과 시퀀트 계산의 대칭을 보여주는 것으로 나타났다.^[6]

커리-하워드 시대에는 "증명 = 프로그램" 대응은 직관주의 논리에서만 고찰되었다. 고전 논리를 포함하는 명확한 대응의 확장은 그리핀의 연구에 의한 것이다. 그리핀은 프로그램 실행에서의 평가 문맥(계속)을 캡처하여 재사용하는 제어 연산자를 가진 람다 계산이 고전 논리와 대응함을 지적했다. 기본적인 고전 논리의 커리-하워드 대응은 다음과 같다.

논리	프로그래밍
피어스 법칙: ((α → β) → α) → α	계속 호출
이중 부정 변환	CPS 변환

피어스 법칙 대신에 시퀀트의 결론에 여러 개의 논리식을 허용함으로써 고전 논리의 자연 연역을 정의할 수도 있다. 이 경우에도 역시 대응이 성립한다. 예를 들어, 어떤 종류의 고전 논리의 자연 연역과 M. 파리고의 λμ 계산 사이에 "증명 = 프로그램"의 대응이 존재한다.

"증명 = 프로그램" 대응은 겐첸의 시퀀트 계산에서도 확립되었지만, 힐베르트류의 체계나 자연 연역처럼 이미 알려진 계산 모델과의 대응 관계는 존재하지 않는다.

시퀀트 계산은 좌 도입 규칙, 우 도입 규칙, 그리고 제거 가능한 컷 규칙에 의해 특징지어진다. 시퀀트 계산의 구조는 일종의 추상 기계의 구조와 유사하다. 비형식적인 대응은 다음과 같다.

논리	프로그래밍
컷 제거	추상 기계에서의 축약
우 도입 규칙	코드의 생성자
좌 도입 규칙	평가 스택의 생성자
컷 제거에서 오른쪽 우선	이름 호출 축약 전략
컷 제거에서 왼쪽 우선	값 호출 축약 전략
컷 제거 정리	축약의 약한 정규성

5. 관련 증명-프로그램 대응

커리-하워드 대응 외에도 다음과 같은 증명-프로그램 대응이 존재한다.

BHK 해석: BHK 해석은 직관주의적 증명을 함수로 해석하지만, 해석에 사용되는 함수의 종류는 명시하지 않는다. 이 함수 종류로 람다 대수를 사용하면, BHK 해석은 자연 연역과 람다 대수 사이의 하워드 대응과 같은 내용을 갖는다.^[6]
실현 가능성: 클리니의 재귀적 실현 가능성은 직관적 산술의 증명을 재귀 함수와 그 함수가 "실현"함을 나타내는 공식의 증명, 이 두 가지로 나눈다. 즉, 초기 공식의 선언 및 존재 정량자를 올바르게 인스턴스화하여 공식이 참이 되도록 만든다.
커리-하워드-람벡 대응: 요아힘 람벡은 1970년대 초 직관주의 명제 논리의 증명과 형식화된 조합 논리의 조합자가 데카르트 닫힌 범주의 이론, 즉 공통적인 등식 이론을 공유함을 보였다.^[10] 일부 연구자들은 커리-하워드-람벡 대응이라는 용어를 사용하여 직관주의 논리, 형식화된 람다 계산, 데카르트 닫힌 범주 사이의 관계를 나타낸다. 이 대응에 따라 데카르트 닫힌 범주의 객체는 명제(타입)로, 사상은 일련의 가정(타입 컨텍스트)을 유효한 결론(잘 정의된 항)에 매핑하는 추론으로 해석될 수 있다.^[10]

5. 1. BHK 해석

BHK 해석은 직관주의적 증명을 함수로 해석하지만, 해석에 관련된 함수의 종류를 명시하지 않는다. 이 함수 종류로 람다 대수를 사용한다면, BHK 해석은 자연 연역과 람다 대수 사이의 하워드 대응과 동일한 내용을 말한다.^[6]

5. 2. 실현 가능성

클리니의 재귀적 실현 가능성은 직관적 산술의 증명을 재귀 함수와 그 함수가 "실현"함을 나타내는 공식의 증명 쌍으로 나눈다. 즉, 초기 공식의 선언 및 존재 정량자를 올바르게 인스턴스화하여 공식이 참이 되도록 한다.

5. 3. 커리-하워드-람벡 대응

요아힘 람벡은 1970년대 초 직관주의 명제 논리의 증명과 형식화된 조합 논리의 조합자가 데카르트 닫힌 범주의 이론, 즉 공통적인 등식 이론을 공유한다는 것을 보였다.^[10] 일부 사람들은 커리-하워드-람벡 대응이라는 표현을 직관주의 논리, 형식화된 람다 계산 및 데카르트 닫힌 범주 간의 관계를 지칭하는 데 사용한다. 이 대응에 따라 데카르트 닫힌 범주의 객체는 명제(타입)로 해석될 수 있으며, 사상은 일련의 가정(typing context, 타입 컨텍스트)을 유효한 결론(잘 정해진 항)에 매핑하는 추론으로 해석될 수 있다.^[10]

람벡의 대응은 등식 이론의 대응으로, 베타 감소 및 항 정규화와 같은 계산의 역학에서 추상화되며, 커리와 하워드의 각 대응에서와 같이 구조의 구문적 동일성을 표현하는 것이 아니다. 즉, 데카르트 닫힌 범주에서 잘 정의된 사상의 구조는 힐베르트 스타일 논리 또는 자연 연역법에서 해당 판단의 증명 구조와 비교할 수 없다. 예를 들어, 사상이 정규화되는지 여부를 명시하거나 증명하거나, 처치-로서 정리 유형을 설정하거나, "강하게 정규화된" 데카르트 닫힌 범주에 대해 말하는 것은 불가능하다. 이러한 구분을 명확히 하기 위해 데카르트 닫힌 범주의 기본 구문 구조는 아래와 같다.

객체(명제/타입)는 다음을 포함한다.

$\top$ 는 객체
$\alpha$ 및 $\beta$ 가 객체인 경우, $\alpha \times \beta$ 및 $\alpha \rightarrow \beta$ 는 객체

사상(추론/항)은 다음을 포함한다.

항등 사상: $\text{id}_\alpha : \alpha \to \alpha$
합성: $t : \alpha \to \beta$ 및 $u : \beta \to \gamma$ 가 사상인 경우, $u \circ t : \alpha \to \gamma$ 는 사상
종결 사상: $\star_\alpha : \alpha \to \top$
곱: $t : \alpha \to \beta$ 및 $u : \alpha \to \gamma$ 가 사상인 경우, $(t, u) : \alpha \to \beta \times \gamma$ 는 사상
투영: $\pi_{\alpha,\beta,1} : \alpha \times \beta \to \alpha$ 및 $\pi_{\alpha,\beta,2} : \alpha \times \beta \to \beta$
평가: $\text{eval}_{\alpha,\beta} : (\alpha \to \beta) \times \alpha \to \beta$
커링: $t : \alpha \times \beta \to \gamma$ 가 사상인 경우, $\lambda t : \alpha \to \beta \to \gamma$ 는 사상

모든 데카르트 닫힌 범주에서 잘 정의된 사상(형식화된 항)은 다음 타입 규칙에 따라 구성할 수 있다. 일반적인 범주론적 사상 표기법

f : \alpha \to \beta

는 타입 컨텍스트 표기법

\alpha \vdash f : \beta

로 대체된다.

항등 사상:

:

\frac{}{\alpha \vdash \text{id} : \alpha}

합성:

:

\frac{\alpha \vdash t : \beta \qquad \beta \vdash u : \gamma}{\alpha \vdash u \circ t : \gamma}

단위 타입(종결 객체):

:

\frac{}{\alpha \vdash \star : \top}

데카르트 곱:

:

\frac{\alpha \vdash t : \beta \qquad \alpha \vdash u : \gamma}{\alpha \vdash (t,u) : \beta \times \gamma}

왼쪽 및 오른쪽 투영:

:

\frac{}{\alpha \times \beta ~\vdash~ \pi_1 : \alpha}\qquad\frac{}{\alpha \times \beta ~\vdash~ \pi_2 : \beta}

커링:

:

\frac{\alpha \times \beta ~\vdash~ t : \gamma}{\alpha \vdash \lambda t : \beta \to \gamma}

적용:

:

\frac{}{(\alpha \rightarrow \beta) \times \alpha \vdash \text{eval} : \beta}

마지막으로 범주의 등식은 다음과 같다.

$\text{id} \circ t = t$
$t \circ \text{id} = t$
$(v \circ u) \circ t = v \circ (u \circ t)$
$\star = \text{id}$ (잘 형식화된 경우)
$\star \circ u = \star$
$\pi_1 \circ (t, u) = t$
$\pi_2 \circ (t,u) = u$
$(\pi_1, \pi_2) = id$
$(t_1, t_2) \circ u = (t_1 \circ u, t_2 \circ u)$
$\text{eval} \circ (\lambda t \circ \pi_1, \pi_2) = t$
$\lambda \text{eval} = \text{id}$
$\lambda t \circ u = \lambda (t \circ (u \circ \pi_1, \pi_2))$

이러한 등식은 다음

\eta

-법칙을 의미한다.

$(\pi_1 \circ t, \pi_2 \circ t) = t$
$\lambda (\text{eval} \circ (t \circ \pi_1, \pi_2)) = t$

\alpha_1 \times \ldots \times \alpha_n \vdash t : \beta

인

t

가 존재한다면,

\alpha_1, \ldots, \alpha_n \vdash \beta

는 함축적 직관주의 논리에서 증명 가능하다.

6. 한국의 관점 및 영향

커리-하워드 대응은 한국의 컴퓨터 과학 및 논리학 연구에 큰 영향을 미쳤다. 이 개념은 프로그래밍 언어 설계, 소프트웨어 검증, 인공지능 등 다양한 분야에서 활용되고 있다.

6. 1. 주요 인물

커리-하워드 대응에 기여한 주요 인물은 다음과 같다.

'''커리''': 1934년에 조합자의 타입이 직관적 함축 논리에 대한 공리 체계로 간주될 수 있다는 것을 관찰했다.^[6] 1958년에는 힐베르트식 연역 시스템이 조합 논리의 타입이 지정된 조각과 일부 일치한다는 것을 발견했다.^[6]
'''하워드''': 1969년에 자연 연역이라는 증명 계산 시스템이 람다 계산의 타입 지정된 변형으로 해석될 수 있음을 보였다.^[6]

이들의 연구를 통해 증명 시스템과 계산 모델 사이에 동형성이 존재한다는 커리-하워드 대응(Curry–Howard correspondence)이 확립되었다.^[6]

6. 2. 주요 사건

1934년 커리는 조합자의 타입이 직관적 함축 논리에 대한 공리 체계로 간주될 수 있다는 것을 관찰했다.^[1]
1958년 커리는 힐베르트식 연역 시스템으로 알려진 특정 종류의 증명 계산이 조합 논리로 알려진 표준 계산 모델의 타입이 지정된 조각과 일부 일치한다는 것을 관찰했다.^[2]
1969년 하워드는 자연 연역이라고 불리는 또 다른 "상위 수준"의 증명 계산이 직관주의 버전의 람다 계산으로 알려진 계산 모델의 타입 지정된 변형으로 직접 해석될 수 있음을 관찰했다.^[3]

7. 추가 연구 및 응용 분야

커리-하워드 대응은 발견 이후 증명 계산과 타입이 지정된 함수형 프로그래밍 언어 모두로 작동하도록 설계된 새로운 종류의 형식 시스템 연구로 이어졌다. 여기에는 마틴-뢰프의 직관주의적 타입 이론과 코캉의 구성의 계산이 포함되는데, 이 두 계산에서 증명은 일반적인 객체이며, 프로그램처럼 증명의 속성을 진술할 수 있다. 이러한 연구 분야는 현대 타입 이론이라고 불린다.

Coq와 같은 소프트웨어는 커리-하워드 패러다임에서 파생된 타입이 지정된 람다 계산을 기반으로 하며, 증명을 프로그램으로 간주하여 형식화, 검사 및 실행할 수 있도록 한다.

프로그램의 프로그램 정확성이 주어지면, ''프로그램을 사용하여 증명을 추출''하는 연구도 진행되고 있다. 이는 증명 휴대 코드와 밀접하게 관련되어 있으며, 커리-하워드 대응을 실질적으로 활용하려는 노력의 일환으로 타입 시스템 개발에 영향을 주었다.

커리-하워드 대응은 고전 논리가 프로그램의 지속을 조작하는 능력, 시퀀트 계산의 대칭성, 호출 방식과 값에 의한 호출의 평가 전략 간 이중성과 관련된다는 점 등, 증명 개념의 계산적 내용에 대한 새로운 질문을 제기했다.

튜링 완전 계산 모델은 무한 루프를 허용하기 때문에, 단순하게 대응을 적용하면 논리적 모순이 발생할 수 있다. 따라서 모나드를 사용하여 종료가 보장되는 코드와 그렇지 않은 코드를 분리하는 방식 등이 연구되고 있다. 전체 함수형 프로그래밍에서는 무제한 재귀를 제거하고, 종료되지 않는 동작이 필요한 경우 코재귀를 사용하는 접근 방식을 취한다.

명제 논리에 순환적 명제 ( $\mu p.\alpha$ ) 구성 규칙을 추가하면, 이는 논리식의 재귀 방정식( $X = [X/p]\alpha$ )의 해(고정점)를 의미하며, 거짓말쟁이의 역설과 같이 모순을 일으킬 수 있다.

이러한 논리식 구성에 대응하는 형 구성(type construction)은 재귀형이라고 한다. 예를 들어 가변 길이 리스트형은 재귀형( ${\rm List} T = \mu \tau.1+T\times\tau$ )으로 표현할 수 있다. 이 형 시스템에서는 Y 결합자나 $\Omega = (\lambda x.xx)(\lambda x.xx)$ 등의 항도 형을 가지며, 이는 커리의 역설과 대응된다.

논리와 프로그래밍의 대응 관계는 다음 표와 같이 정리할 수 있다.

논리	프로그래밍
순환적 명제	재귀형
$\frac{\Gamma \vdash \mu p.\alpha}{\Gamma \vdash [\mu p.\alpha/p]\alpha}$	$\frac{\Gamma \vdash X:\mu \tau.\alpha}{\Gamma \vdash X:[\mu \tau.\alpha/\tau]\alpha}$
$\frac{\Gamma \vdash [\mu p.\alpha/p]\alpha}{\Gamma \vdash \mu p.\alpha}$	$\frac{\Gamma \vdash X:[\mu \tau.\alpha/\tau]\alpha}{\Gamma \vdash X:\mu \tau.\alpha}$

7. 1. 고차 논리 및 시스템 F_ω

고차 논리는 제라르의 시스템 F_ω에 대응된다.^[6]

7. 2. 양상 논리

양상 논리의 필요성

\Box

은 단계별 계산에 대응된다. 양상 논리의 가능성

\Diamond

은 효과에 대한 모나드 타입에 대응된다.

7. 3. 유전자 프로그래밍

최근, 커리-하워드 동형사상이 유전자 프로그래밍에서 탐색 공간 분할을 정의하는 방법으로 제안되었다.^[11] 이 방법은 커리-하워드 동형 증명(종으로 지칭)에 의해 유전자형 집합(GP 시스템에 의해 진화된 프로그램 트리)에 색인을 부여한다.^[21]

7. 4. 소프트웨어 특허성

INRIA 연구 이사 베르나르 랑^[12]에 따르면, 커리-하워드 대응은 소프트웨어 특허성에 대한 논거를 구성한다. 알고리즘이 수학적 증명이므로 전자의 특허성은 후자의 특허성을 의미한다. 정리는 사유 재산이 될 수 있으며, 수학자는 이를 사용하기 위해 비용을 지불해야 하고, 증명을 비밀로 유지하고 오류에 대한 책임을 거부하는 회사를 신뢰해야 한다.

참조

_[1] 논문 Lecture Notes in Semantics http://www.ps.uni-sa[...] 2007-08
_[2] 서적 Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies https://books.google[...]
_[3] 서적 Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics https://books.google[...] Springer
_[4] 서적 Picturing Quantum Processes https://books.google[...] Cambridge University Press
_[5] 웹사이트 Computational trilogy https://ncatlab.org/[...] 2023-10-29
_[6] 간행물 Notions of Computation and Monads http://www.disi.unig[...]
_[7] 간행물 A Modal Analysis of Staged Computation https://www.cs.cmu.e[...]
_[8] 간행물 Lectures on the Curry-Howard Isomorphism
_[9] 간행물 Mathematical Modal Logic: A Model of its Evolution
_[10] 서적 Introduction to higher order categorical logic Cambridge university press 1989
_[11] 논문 Genetic programming with polymorphic types and higher-order functions http://www.site.uott[...] 2008
_[12] 웹사이트 Article http://bat8.inria.fr[...] 2020-01-31
_[13] 논문 Physics, Topology, Logic and Computation: A Rosetta Stone https://arxiv.org/ab[...] 2009
_[14] 서적 Homotopy Type Theory: Univalent Foundations of Mathematics http://homotopytypet[...] Institute for Advanced Study 2013
_[15] 간행물 A Judgmental Reconstruction of Modal Logic https://www.cs.cmu.e[...]
_[16] 간행물 A Modal Analysis of Staged Computation https://www.cs.cmu.e[...]
_[17] 간행물 λρ-calculus http://komoriyuichi.[...]
_[18] 간행물 Lectures on the Curry-Howard Isomorphism http://citeseerx.ist[...]
_[19] 간행물 Mathematical Modal Logic: A Model of its Evolution http://homepages.mcs[...]
_[20] 간행물 Computational types from a logical perspective
_[21] 논문 Genetic programming with polymorphic types and higher-order functions http://www.site.uott[...] 2008
_[22] 간행물 A Judgmental Reconstruction of Modal Logic https://www.cs.cmu.e[...]

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com