커리-하워드 통신

기능적 프로그램으로 작성된 증명서
plus_comm = 재미있다 n m : 냇 => nat_ind (재미있다 n0 : 냇 => n0 + m = m + n0) (plus_n_0 m) (재미있다 (y : 냇) (H : y + m = m + y) => eq_ind (S (m + y)) (재미있다 n0 : 냇 => S (y + m) = n0) (f_message S H) (m + S y) (plus_n_Sm m y)) n : 전부 n m : 냇, n + m = m + n
증명 보조자 Coq에 있는 자연수 덧셈의 공통성 증명. nat_ind수학 유도를 나타낸다.eq_ind동등의 대체에 대하여f_equal평등의 양쪽에서 같은 기능을 취하는 것.$m{\displaystyle }$= ${\displaystyle \mathrm{m}}$+ 0 ${\displaystyle m=m+0}$ 및$$ S${\displaystyle (m}$+ ${\displaystyle y}$)${\displaystyle }$= ${\displaystyle m}$+ ${\displaystyle S}$ ${\displaystyle y}$ ${\displaystyle S(m+y)=m$을 보여주는 이전의 이론들을 참조한다.$+Sy}$.

프로그래밍 언어 이론과 증명 이론에서, Curry-Howard 대응(Curry-Howard 이형성 또는 동등성, 또는 Programs-as-programs and propositions- 또는 형식-as-type 해석이라고도 한다)은 컴퓨터 프로그램과 수학 증명 사이의 직접적인 관계다.

미국의 수학자 하스켈 커리와 논리학자 윌리엄 앨빈 하워드가 처음 발견한 형식논리와 계산계산학 시스템 사이의 통사적 유추를 일반화한 것이다.^[1]L. E. J. 브루워, 아렌드 헤이팅 및 안드레이 콜모고로프(Brouwer– 참조)가 여러 공식에서 제시한 직관적 논리의 운용 해석과 관련이 있지만, 일반적으로 커리와 하워드에게 귀속되는 것은 논리학과 연산 사이의 연결고리다.헤이팅-콜모고로프 해석)^[2]과 스테판 클레네(실현 가능성 참조).그 관계는 커리-하워드-람베크 3자 통신에 카테고리 이론을 포함하도록 확장되었다.

출처, 범위 및 결과

Curry-Howard 통신의 시작은 몇 가지 관찰에 있다.

1. 1934년 Curry는 조합자의 유형이 직감적 관계 논리의 공리로 보일 수 있다고 관찰한다.^[3]
2. 1958년에 그는 힐버트식 공제 시스템이라고 불리는 어떤 종류의 증명 시스템이 결합 논리학이라고 알려진 표준 계산 모델의 타이핑된 조각과 어떤 조각에 일치한다고 관찰한다.^[4]
3. 1969년에 Howard는 자연 추론이라고 불리는 또 다른 "고차원" 증명 시스템이 직관적 버전에서 람다 미적분학이라고 알려진 연산 모델의 유형 변형으로 직접 해석될 수 있다고 관찰했다.^[5]

즉, Curry-Howard의 대응은 겉보기에 무관해 보이는 형식주의, 즉 한 손에는 증명 시스템, 다른 한 손에는 연산 모델 등 두 집단이 사실상 같은 종류의 수학 물체라는 관측이다.

만약 어떤 사람이 어느 하나의 형식주의의 특수성을 추상화한다면, 다음과 같은 일반화가 발생한다: 증거는 프로그램이고, 그것이 증명하는 공식은 프로그램의 유형이다.보다 비공식적으로, 이것은 함수의 반환 유형(즉 함수에 의해 반환되는 값의 유형)이 논리 정리와 유사하며, 함수에 전달된 인수 값의 유형에 해당하는 가설을 따르며, 그 함수를 계산하는 프로그램이 의 증명과 유사하다고 말하는 비유로 볼 수 있다.그 정리.이것은 엄격한 기초 위에 논리 프로그래밍의 형태를 설정한다: 증명들은 프로그램으로 대표될 수 있고, 특히 람다 용어 또는 증명들이 실행될 수 있다.

서신은 발견 이후 새로운 연구의 큰 스펙트럼의 출발점이 되어 왔으며, 특히 증명 시스템으로서나 타이핑된 기능 프로그래밍 언어로서 모두 작용하도록 설계된 새로운 종류의 공식 시스템으로 이어졌다.여기에는 마틴 뢰프의 직관적 유형 이론과 코콴드의 구성 미적분학 등이 포함된다. 이 두 가지 미적분학에서는 증명들이 담론의 규칙적인 대상이며 어떤 프로그램과도 동일한 방식으로 증명들의 속성을 진술할 수 있다.이 연구 분야는 보통 현대형 이론이라고 한다.

Curry-Howard 패러다임에서 파생된 이러한 타입의 람다 캘커리는 프로그램으로 보이는 증거를 공식화하고, 확인하고, 실행할 수 있는 Coq와 같은 소프트웨어로 이어졌다.

역방향은 프로그램을 사용하여 정확성을 고려하여 증거를 추출하는 것이다. 즉, 증거를 운반하는 코드와 밀접하게 관련된 연구 영역이다.이는 프로그램이 작성되는 프로그래밍 언어가 매우 풍부한 유형일 경우에만 가능하다. 이러한 유형의 시스템의 개발은 부분적으로 Curry-Howard 서신을 실질적으로 관련성 있게 만들고자 하는 바람에서 비롯되었다.

커리-하워드의 서신은 또한 커리와 하워드의 원작에서 다루지 않았던 증명 개념의 계산적 내용에 관한 새로운 의문을 제기했다.특히 고전적 논리는 프로그램의 연속성을 조작할 수 있는 능력과 이름별과 가치별이라고 알려진 두 평가 전략 사이의 이중성을 표현하기 위한 시퀀스 미적분학의 대칭성에 해당한다는 것이 밝혀졌다.

추측적으로, Curry-Howard의 서신은 수학 논리와 기초 컴퓨터 과학 사이의 실질적인 통일로 이어질 것으로 예상된다.

힐버트식 논리와 자연 추리는 많은 형식주의자들 사이에서 두 종류의 증명제도에 불과하다.대체 구문에는 시퀀스 미적분학, 교정망, 구조 미적분 등이 있다.어떤 증명 시스템이든 계산 모델을 숨기고 있다는 일반적인 원리로 Curry-Howard 서신을 인정한다면, 이러한 종류의 증명 시스템의 근본적인 비형식 계산 구조에 대한 이론이 가능해야 한다.그렇다면, 자연스러운 질문은 이러한 근본적인 계산 계산에 대해 수학적으로 흥미로운 것이 말해질 수 있는가 하는 것이다.

반대로 결합논리와 간단히 타이핑된 람다 미적분학만이 연산의 유일한 모델은 아니다.지라드의 선형 논리는 람다 미적분학의 일부 모델에서 자원의 사용에 대한 정밀 분석으로부터 개발되었다. 증명 시스템으로 동작할 튜링의 기계에 타이핑된 버전이 있는가?유형화된 어셈블리 언어는 유형을 전달하는 "낮은 수준" 연산 모델의 한 예다.

중단되지 않는 프로그램을 작성할 수 있기 때문에, 통신의 순진한 적용이 일관되지 않는 논리로 이어지기 때문에 튜링-완전한 연산 모델(임의의 재귀적 기능이 있는 언어 등)은 주의 깊게 해석해야 한다.논리적인 관점에서 임의 계산을 다루는 최선의 방법은 여전히 활발하게 논의되고 있는 연구 질문이지만, 하나의 일반적인 접근법은 잠재적으로 종료되지 않는 코드(컴퓨팅의 훨씬 더 풍부한 모델에 일반화하는 접근법,^[6] 그 자체와 관련이 있는 접근법)를 분리하기 위해 모노드를 사용하는 것에 기초하고 있다.Curry-Howard 이소모르피즘의^{[ext 1]} 자연적 확장에 의한 모달 논리학).총기능 프로그래밍에 의해 주창되는 보다 급진적인 접근방식은 비단종적 행동이 실제로 원하는 곳이라면 어디서든 더 통제된 코어커서를 사용하여 무제한 재귀(그리고 높은 계산 복잡성은 유지하지만 튜링 완전성은 포기)를 제거하는 것이다.

일반 제형

보다 일반적인 공식에서, Curry-Howard 대응은 계산 모델을 위한 형식 증명 캘커리와 형식 시스템 사이의 대응이다.특히 두 개의 대응으로 나뉜다.하나는 특정한 증명 시스템이나 계산 모델을 고려하는 것과 독립적인 공식과 유형의 수준이고, 하나는, 이번에 검토된 증명 시스템과 계산 모델의 특정한 선택에 특정한 증명 시스템과 프로그램의 수준에 있다.

공식과 형식의 수준에서 함수는 함수형, 즉 "제품"형(이것은 언어에 따라 튜플, 구조체, 목록 또는 다른 용어)과 결합하여 작용한다(이 유형은 합체라고 할 수 있다), 합체형(이 유형은 합체라고 할 수 있다), 허구형, 참형 등과 같은 함수의 작용을 한다고 서신에서는 밝히고 있다.식을 싱글톤 유형으로 한다(단일 멤버는 null 객체임).정량자는 종속 기능 공간 또는 제품(해당되는 경우)에 해당한다.이는 다음 표에 요약되어 있다.

논리측	프로그래밍 측
보편적 정량화	일반 제품 유형(GRB 유형)
실존적 수량화	일반합계형(GNP형)
함축	함수형
접속사	상품형
분리	합계형
참된 공식	단위형
그릇된 공식	밑단 활자

증명 시스템과 계산 모델 수준에서, 대응은 주로 구조의 정체성을 보여주는데, 첫째, 힐버트식 공제 시스템이라고 알려진 시스템의 특정한 구성과 결합 논리 사이, 둘째, 자연 추론과 람다 미적분학이라고 알려진 시스템의 특정한 구성 사이의 것이다.

논리측	프로그래밍 측
힐버트식 공제 제도	전투 논리용 타이프 시스템
자연 공제	람다 미적분 타이프 시스템

자연적 공제 체계와 람다 미적분 사이에는 다음과 같은 서신들이 있다.

논리측	프로그래밍 측
가설.	자유 변수
시사 제거(모더스 폰)	신청
암시적 소개	추상화

해당 시스템

힐버트식 공제 체계와 결합 논리

그것은 1958년 Curry와 Feys의 결합논리에 관한 책인 1958년 펴낸 결합논리에 관한 책인 결합논리의 기본 결합자 K와 S에 대한 가장 단순한 형태는 힐버트식 추리시스템에서 사용된 각각의 공리계획 α → (β → α) → (β → β) → (α → β) → (α → α → α) → (α)에 놀랄 만큼 대응되었다.이 때문에 이러한 계략을 이제는 공리 K와 S라고 하는 경우가 많다.힐버트식 논리에서 증거로 보이는 프로그램의 예는 다음과 같다.

관계적 직관적 단편에만 국한한다면 힐베르트의 문체로 논리를 공식화하는 간단한 방법은 다음과 같다.Ⅰ을 가설로 간주되는 공식의 유한 집합이 되게 하라.그 다음 Δ는 Δ Δ로 표시된 Δ에서 도출할 수 있으며, 다음과 같은 경우 Δ Δ로 표시된다.

• Δ는 가설이다. 즉 Δ의 공식이다.
• Δ는 공리 계통의 한 예로서, 즉 가장 일반적인 공리 계통에서는 다음과 같다.
  • Δ는 α → (β → α), 또는
  • Δ는 형태(α → (β → γ) → (α → β) → (α → γ) → (α → γ)),
• Δ는 추론에 따른다. 즉, 일부 α에 대해서는 α → Δ와 α 모두 이미 γ에서 도출할 수 있다(이것이 모더스 폰의 규칙이다).

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

타이핑된 결합 논리는 유사한 구문을 사용하여 공식화될 수 있다: Ⅱ를 변수의 유형에 주석을 달고 변수의 유한 집합이 되게 한다.다음과 같은 경우, 용어 T(유형에 주석을 달기도 함)는 이러한 변수 [γ ⊢ T:Δ]에 따라 달라진다.

• T는 γ의 변수 중 하나이다.
• T는 기본 콤비네이터로, 즉 가장 일반적인 콤비네이터 기준으로 다음과 같다.
  • T는 K:α → (β → α) [여기서 α와 β는 그 인수의 유형을 나타낸다] 또는
  • T는 S:(α → (β → γ) → (α → β) → (α → γ),
• T는 γ의 변수에 따라 달라지는 두 개의 하위 단어의 구성이다.

여기서 정의한 세대 규칙은 아래의 오른쪽 열에 제시되어 있다.커리의 말은 두 칼럼이 일 대 일 통신에 있다고 간단히 말한다.직감적 논리에 대한 대응의 제한은 페어스의 법칙(α → β) → α) → α와 같은 일부 고전적 토폴로지를 대응에서 제외하는 것을 의미한다.

힐버트식 직감론적 관계 논리	단순 입력 결합 논리
${\displaystyle {\frac {\alpha \in \Gamma }{\Gamma \vdash \vdash \alpha }}}}\qquad \qquad {\text{Assum}}}}}$	${\displaystyle {\frac {x:\alpha \in \Gamma }{\Gamma \vdash x:\alpha }}}$
${\displaystyle {\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}\qquad {\text{도끼}_{K}}$	${\displaystyle {\frac {}{\Gamma \vdash K:\alpha \rightarrow \alpha )}}$
${\displaystyle {\frac {}{\Gamma \vdash(\alpha \!\오른쪽 화살표 \!(\beta \\오른쪽 화살표 \!\\gamma )\!\rightarrow \!(\i1\\rightarrow \!\i1\i1\)\!\rightarrow \!(\reightarrow \\\\reightarrow \!\reghtarrow )}}\;{\text{도끼}_{S}}$	${\displaystyle {\frac {}{\\Gamma \vdash S:(\알파 \!\오른쪽 화살표 \!)\!\rightarrow \!(\i1\\rightarrow \!\i1\i1\)\!\rightarrow \!(\ready \\rightarrow \\\ready )}}}}$
${\displaystyle {\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\\damma \vdash \beta }}}}\quad{\text{\modus Ponens}}}}}}}}}}$	${\displaystyle {\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\Alpha }{\Gamma \vdash E_{1}\;E_{2}:\베타 }}$

좀 더 추상적인 수준에서 보면, 다음 표와 같이 서신을 재작성할 수 있다.특히 힐버트식 논리에 특화된 공제 정리는 결합논리의 추상화 제거 과정과 일치한다.

논리측	프로그래밍 측
가정하다	가변적
공리	전투원
양식장.	신청
공제 정리	추상화 제거

통신 덕분에 전투적 논리의 결과는 힐버트식 논리로 옮겨질 수 있고 그 반대도 가능하다.예를 들어, 결합 논리에서의 용어 축소의 개념은 힐버트식 논리로 옮겨질 수 있으며, 그것은 증명서를 같은 진술의 다른 증명들로 합법적으로 변형시키는 방법을 제공한다.또한 정상 용어의 개념을 정상 증거의 개념으로 옮길 수 있으며, 공리의 가설은 (그렇지 않으면 단순화가 일어날 수 있기 때문에) 모두 분리할 필요가 없다는 것을 표현한다.

반대로, Peirce의 법칙의 직감적 논리의 비증명은 다시 결합적 논리로 옮겨질 수 있다: 유형으로 타이핑할 수 있는 결합적 논리의 타이핑된 용어는 없다.

((α → β) → α) → α.

결합기 또는 공리의 일부 집합의 완전성에 대한 결과도 전송될 수 있다.예를 들어 콤비네이터 X가 (확장) 결합논리의 1점 기준을 구성한다는 사실은 단일 공리 체계임을 암시한다.

(((α → (β → γ)) → ((α → β) → (α → γ))) → ((δ → (ε → δ)) → ζ)) → ζ,

X의 주요 유형으로 공리 계획의 조합을 적절히 대체한다.

α → (β → α) 및

(α → (β → γ)) → ((α → β) → (α → γ)).

자연공제 및 람다 미적분

커리가 힐버트식 추론과 결합논리의 통사적 일치성을 강조한 후, 하워드는 1969년 단순히 타이핑한 람다 미적분학 프로그램과 자연적 추론의 증명 사이의 통사적 유사성을 분명히 했다.아래 왼쪽은 직감적 관계적 자연공제를 서열의 미적분으로서 공식화하고(서열을 사용하는 것은 추론규칙을 더욱 깨끗하게 진술할 수 있게 해 주기 때문에 Curry-Howard 이소모르피즘의 논의에서 표준으로 한다), 오른쪽은 람다 미적분의 타이핑 규칙을 보여준다.왼쪽에서 γ, γ₁, γ은₂ 순서가 정해진 공식의 순서를 나타내며 오른쪽에서 모든 이름이 다른 명명된(즉, 타이핑된) 공식의 순서를 나타낸다.

직관적 관계적 자연적 추론	람다 미적분 유형 할당 규칙
${\displaystyle {\frac {}{\Gamma _{1},\alpha,\Gamma _{2}\vdash \alpha }}{\text{악스}}$	${\displaystyle {\frac {}{\Gamma _{1},x:\alpha,\Gamma _{2}\vdash x:\alpha }}}$
${\displaystyle {\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \vdash \alpha \rightarrow }}}}$	${\displaystyle {\bambda x\\gamma ,x:\alpha \vdash t:\beta }{\gamma \vdash (\lambda x\!:\\!\cHB .t):\cHB \rightarrow \}}$
${\displaystyle {\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rigarrow E}$	${\displaystyle {\bdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha }{\Damma \vdash t\;u:\beta }}}}}}}$

통신 내용을 비유하자면, γ α를 증명하는 것은 γ에 열거된 유형과 함께 주어진 값을 가지고 α 타입의 물체를 제조하는 프로그램을 갖는 것을 의미한다.공리는 새로운 유형의 제약이 없는 새로운 변수의 도입에 대응하고, → I 규칙은 함수 추상화에 대응하고 → E 규칙은 함수 적용에 대응한다.예를 들어, α → α → α 타입의 type-terms xx.yy.x 및 xx.yy.y 타입이 통신에서 구별되지 않는 경우, context-terms xx.yy.y 공식의 집합으로 간주되는 경우, 대응은 정확하지 않음을 관찰한다.예는 다음과 같다.

하워드는 그 서신이 단순히 타이핑된 람다 미적분의 다른 구조와 논리의 다른 연결체까지 확장된다는 것을 보여주었다.추상적인 수준에서 보면, 다음 표와 같이 서신을 요약할 수 있다.특히 람다 미적분학의 정상형식의 개념은 프라위츠의 자연적 추론에서의 정상적 추론 개념과 일치한다는 것을 보여주는데, 그 결과 유형별 거주 문제에 대한 알고리즘이 직관적 검증 가능성을 결정하는 알고리즘으로 바뀔 수 있다는 것을 알게 된다.

논리측	프로그래밍 측
공리	가변적
도입규정	건설업자
탈락 규칙	파괴자
정상 공제	정상형
공제 정상화	약한 정상화
증명 가능성	유형별 거주 문제
직감적 태토론	사람이 사는 활자형.

하워드의 서신은 자연 공제의 다른 연장선상에 자연스럽게 확장되고 간단히 타이핑된 람다 미적분학으로 확장된다.다음은 비배출 목록:

• 2차 명제 논리 및 다형 람다 미적분학의 공통 언어로서 Girard-Reynolds System F,
• 고차 논리학 및 Girard의 시스템_ω F
• 대수 데이터 유형으로서의 유도 유형
• 모달 로직 및 단계별 계산의$$^{[ext 2]} 필요성${\displaystyle \Box }$
• 모달 로직 및 효과에^{[ext 1]} 대한 모나디 유형의 가능성$$${\displaystyle \Diamond }$
• calc_I 미적분은 관련 논리에 해당한다.^[7]
• 그로텐디크 위상에서의 국부적 진리(진리) 모달리티 또는 벤튼, 비에르만, 데 파바(1998)의 등가 "락스" 모달리티(진리)는 "컴퓨팅 유형"^[8]을 기술하는 CL 로직과 일치한다.

고전적 논리 및 제어 연산자

커리 당시, 그리고 하워드 당시에도, 프로그램으로서의 증명 서신은 직감적 논리, 즉 특히 피어스의 법칙을 추론할 수 없는 논리만을 다루었다.Peirce의 법칙과 그에 따른 고전적 논리에 대한 서신의 확장은 그리핀의 작업으로부터 명확해졌고, 이 평가 컨텍스트를 나중에 재설치할 수 있도록 주어진 프로그램 실행의 평가 컨텍스트를 포착하는 타이핑 운영자에 관한 것이었다.고전적 논리에 대한 기본적인 커리-하워드 방식의 대응은 다음과 같다.고전적 증거를 직관적 논리에 매핑하는 데 사용되는 이중 부정 번역과 통제를 포함하는 람다 용어를 순수한 람다 용어에 매핑하는 데 사용되는 연속 패스 방식의 번역 사이의 관련성을 주목한다.특히, 콜모고로프의 이중부정번역, 콜별 연속부정번역 방식의 번역은 쿠로다에 의한 일종의 이중부정번역과도 관련이 있다.

논리측	프로그래밍 측
페어스의 법칙 : (α → β) → α) → α	콜-와이-와이-와이-와이-와이-와이-
이중 부정 번역	연속 번역.

고전적 논리를 정의하는 것이 Peirce의 법칙과 같은 공리를 첨가하는 것이 아니라 속편에서 여러 가지 결론을 허용함으로써 고전적 논리를 정의한다면 더 미세한 Curry-Howard 서신은 고전적 논리에 대해 존재한다.고전적 자연 공제의 경우, 패리고트의 μ-미적분의 타이핑 프로그램과의 프로그램별 교신 증명서가 존재한다.

시퀀스 미적분학

프로그램으로서의 증명 서신은 겐첸의 속편 미적분학이라고 알려진 형식주의에 대해 정리가 될 수 있지만, 힐버트식 및 자연적 추론처럼 잘 정의된 기존 연산 모델과의 서신은 아니다.

시퀀스 미적분은 왼쪽 도입 규칙, 오른쪽 도입 규칙, 제거할 수 있는 컷 규칙이 있는 것이 특징이다.연속 미적분의 구조는 어떤 추상적인 기계의 구조에 가까운 미적분과 관련이 있다.비공식적인 서신은 다음과 같다.

논리측	프로그래밍 측
탈락시키다	추상적인 기계의 형태에서의 축소
올바른 도입 규칙	코드 생성자
좌익 소개 규칙	평가 스택의 생성자
컷오프에서 우측에 우선하는 것	호별 인하
컷오프에서 왼쪽의 우선 순위	가치별 통화료 인하

프로그램으로서의 관련 증명서 대응

드 브뤼옌 역

N. G. de Bruijn은 정리 검사기 Automath의 증거를 나타내기 위해 람다 표기법을 사용했으며, 명제를 그 증거에 대한 "범주"로 표현했다.하워드가 원고를 쓴 시기는 1960년대 후반이었다. 드 브루이진은 하워드의 작품을 몰랐을 가능성이 높았고, 독자적으로 서신을 진술했다(Sörensen & Urzyzyn [1998] 2006, 페이지 98–99).일부 연구자들은 커리-하워드-데 브루윈 통신이라는 용어를 커리-하워드 통신 대신에 사용하는 경향이 있다.

BHK 해석

BHK 해석은 직관적 증거를 함수로 해석하지만 해석과 관련된 함수의 종류는 명시하지 않는다.만약 어떤 사람이 람다 미적분을 이 등급의 기능에 사용한다면, BHK 해석은 하워드의 자연적 추론과 람다 미적분 사이의 대응과 같은 것을 말해준다.

실현 가능성

클렌의 재귀적 실현성은 직관적 산술의 증거를 재귀함수의 쌍과 재귀함수가 "실현"한다는 것을 표현하는 공식의 증명으로 나누며, 즉, 공식이 참이 되도록 초기 공식의 분리 및 실존적 정량자를 정확하게 인스턴스화한다.

Kreisel의 변형된 현실성은 직관적인 고차수 술어 논리에 적용되며, 교정에서 유도적으로 추출한 단순 타이핑된 람다 용어가 초기 공식을 실현한다는 것을 보여준다.명제 논리의 경우 추출된 람다 용어는 증거 그 자체(유형화되지 않은 람다 용어로 표시됨)이며 실현 가능성 문장은 추출된 람다 용어가 공식(유형으로 표시됨)이 의미하는 유형을 가졌다는 사실을 비유한 것이다.

괴델의 변증법 해석은 계산 가능한 함수로 직관적 산수를 실현(확장)한다.자연 공제의 경우에도 람다 미적분과의 연관성이 불분명하다.

커리-하워드-람베크 통신

요아힘 람벡은 1970년대 초 직관적 명제 논리의 증명과 형식적 결합 논리의 결합자들이 데카르트 폐쇄 범주의 하나인 공통의 등가 이론을 공유한다는 것을 보여주었다.커리-하워드-람베크 대응이라는 표현은 현재 일부 사람들이 직관 논리, 활자화된 람다 미적분학, 데카르트 닫힌 범주 사이의 이형성 3가지 방식을 지칭하기 위해 사용하고 있는데, 그 용어나 증명으로 사물을 유형이나 명제, 형태성으로 해석하고 있다.서신은 동등한 수준에서 작동하며, 커리와 하워드의 서신 각각에 해당하기 때문에 구조의 통사적 정체성의 표현은 아니다. 즉, 데카르트-폐쇄 범주에서 잘 정의된 형태론의 구조는 어느 힐베에서든 상응하는 판결의 증거의 구조와 비교될 수 없다.rt식 논리 또는 자연 추론.이러한 구별을 명확히 하기 위해, 데카르트 폐쇄 범주의 기초적인 통사적 구조를 아래에 재인쇄한다.

객체(유형)는 다음에 의해 정의된다.

• ${\displaystyle \mathrm{▼}}$ ${\displaystyle \top}$이(가) 개체임$$
• α와 β가 물체라면 $\alpha {\displaystyle }$ ${\displaystyle \times }$ ${\displaystyle \beta }$ ${\displaystyle \alpha$ \$times \beta$\$beta$ \$displaystyle \rightarrow \beta}$은 물체다${\displaystyle .}$

형태론(단어)은 다음에 의해 정의된다.

• ${\displaystyle i}$ ${\displaystyle d}$ ${\displaystyle id$ $\star {\displaystyle }$ ${\$$displaystyle \star$ ${\displaystyle \mathrm{평가}}$ {\$displaystyle \$$pi$ {$eval},$$\pi {\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\$$\pi _$${$1$$$},$$$ 2$${\$displaystystysty_{2$}}는$$ 형태론이다.
• t가 형태론이라면, λt는 형태론이다.
• t와 u가 형태론이라면$,{\displaystyle }$ ( ${\displaystyle t}$ ,${\displaystyle u}$) ${\displaystyle (t,u)}$ 및 $u{\displaystyle }$ ${\displaystyle \circ }$ ${\displaystyle t}$ ${\displaystyle u\message$ t$}$은 형태론이다$$.

잘 정의된 형태론(유형 $용어$)은 다음과 같은 타이핑 규칙에 의해 정의된다$($일반적인 범주형 형태론 $표기법{\displaystyle }$ f${\displaystyle }$:${\displaystyle \alpha }$${\displaystyle }$→ ${\displaystyle \beta }$ ${\displaystyle$ f$:\\alpha$ ${\displaystyle \text{}}$$to \$${\displaystyle \text{beta}}$ $}).$$\!-~\cHB~~\vdash ~\buff }.$

ID:

${\displaystyle {\frac {}{id:\!\!-\\cHB~~\vdash~~\\cHB }}$

구성:

$디스플레이 스타일 {\frac {t:\!\!-~\cHB ~\vdash ~\cHB \qquad u:\!\!-~\cHB~~\vdash ~\\cHB }{u\cHB t:\!\!-\cHB~~\vdash~~\cHB }}$

단위 유형(터미널 개체):

${\displaystyle {\frac {}{\star :\!\!-\\cHB~~\vdash~~\top }}$

데카르트 제품:

$디스플레이 스타일 {\frac {t:\!\!-~\cHB ~\vdash ~\cHB \qquad u:\!\!-~\bash ~\vdash ~\bdash }{(t,u):\!\!\!-\bauth ~\vdash ~\bauth \baut \bauth \bauth \bauth \bauth \}}}}}$

왼쪽 및 오른쪽 투영:

${\displaystyle {\frac {}{\pi _{1}:\!\!-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}}}}}}}\qquad {\frac {}{\pi _{2}:\!\!-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ }$

커리어링:

$디스플레이 스타일 {\frac {t:\!\!-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\!-~\cHB~~\vdash ~\cHB \rightarrow \}}$

응용 프로그램:

${\displaystyle {\frac {}{eval:\!\!-~(\cHB \rightarrow \cHB )\cHB \cHB \vdash ~\cHB }}$

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

• $id\displaystyle id\display t=t}$
• $(\displaystyle t\display id=t}$
• $[\displaystyle (v\displaystyle (v\display u)\disput t=v\disput (u\$
• ${\displaystyle \star }$= ${\displaystyle i}$ ${\displaystyle d}$ ${\displaystyle \star =id}($잘 조정된 경우)
• $\displaystyle \star \who=\star }$
• ${\displaystyle \pi _{1}\pi(t,u)=t}$
• ${\displaystyle \pi _{2}\pi(t,u)=u}$
• ${\displaystyle(\pi _{1},\pi _{2}=id})$
• ${\displaystyle(t_{1},t_{2})\message u=(t_{1}\message u,t_{2}\message u)}$
• ${\displaystyle eval\reason(\data t\pi _{1},\pi _{2}=t}$
• ${\displaystyle \lambda eval=id}$
• ${\displaystyle \data t\pi u=\data(t\pi _{1},\pi _{2})}$

이러한 방정식은 다음과 같은 $\eta {\displaystyle }$ ${\displaystyle \eta }$ -sule을$$ 의미한다.

• ${\displaystyle(\pi _{1}\pi t,\pi _{2}\pi t)=t}$
• ${\displaystyle \lambda(eval\pi _{1},\pi _{2})=t}$

$현재{\displaystyle }$ t${\displaystyle }$: -${\displaystyle \text{α}{}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ …${\displaystyle \times }$ ${\displaystyle {\alpha }_{}}$ n β${\displaystyle {}_{}\beta }$ ${\displaystyle$ t$:\!$$\!-\dash \ldots$\ldots $\n1$}\ldots \$ldots$ \ldash $\ldots$ \n$}f$ α1 ,${\displaystyle }$…, ${\displaystyle {\alpha n}_{}\beta }$ ${\displaysty \{1$}, $\n}\dash \ldash$ \ldes$}}}}}}}}}}$은(으$$$)$의 설득력 논리에서 증명할 수 있다.

예

Curry-Howard 통신 덕분에, 논리 공식에 해당하는 타입의 표현은 그 공식의 증거와 유사하다.예를 들어보자.

힐버트식 논리에서는 α → α의 증거로 보이는 정체성 결합기

예를 들면 정리 α → α에 대한 증거를 생각해 보자.람다 미적분학에서 이것은 ID 함수 I = xx.x의 유형이며 결합 논리에서는 K = xyxy.x에 S = =fgx.fx(gx)를 두 번 적용하여 ID 함수를 얻는다.즉, I = (S K) K.증명에 대한 설명으로서 α → α를 증명하기 위해 다음과 같은 단계를 사용할 수 있다고 한다.

• 공식 α, β → α, α로 두 번째 공리 체계를 인스턴스화하여 (α → (β → α) → (α → α) → (α → α) → (α → α) → (α → α), (α → α),
• α와 β → α로 첫 번째 공리 계략을 한 번 인스턴스화하여 α → (β → α) → α)의 증거를 얻는다.
• α와 β로 두 번째 공리 계략을 인스턴스화하여 α → (β → α),
• 모듀스 폰(modus ponens)을 두 번 발라 α → α의 증거를 얻어내다.

일반적으로 프로그램은 양식(P Q)의 적용을 포함할 때마다 다음 단계를 따라야 한다.

1. 먼저 P와 Q의 종류에 해당하는 이론을 증명한다.
2. P를 Q에 적용하고 있기 때문에 P의 형식은 α → β 형태를 가져야 하며, Q의 형식은 일부 α와 β를 위해 α 형태를 가져야 한다.따라서 모더스 포넨스 규칙을 통해 결론인 β를 분리할 수 있다.

힐버트식 논리에서는 (β → α) → ( ( → β) → → → α의 증거로 보는 합성 결합기.

좀 더 복잡한 예로 B함수에 해당하는 정리를 살펴보자.B의 종류는 (β → α) → (γ → β) → γ → α. B는 (S (K S) K와 동일하다.이것은 정리(β → α) → ( ( → β) → → → α의 증명에 대한 우리의 로드맵이다.

첫 번째 단계는 (K S)를 건설하는 것이다.K 공리의 선행자를 S 공리처럼 보이게 하려면 α를 (α → β → β → β) → (α → β) → α → β를 Δ와 같게 설정하고 (변동 충돌을 피하기 위해) β를 Δ와 같게 설정한다.

K : α → β → α

K[α = (α → β → β → β) → α → β → Δ] : (α → β → β → Δ] → (α → β → β) → Δ → (α → β → β) → (α → β) → α → β → α → β → α → α → α → α → α → α → α → α → α → α → α → α → α → α → γ

여기서 선행자는 S에 불과하므로 그 결과물은 Modus Ponens를 사용하여 분리할 수 있다.

K : Δ → (α → β → β → β) → α → α → γ

이것이 (K S)의 종류에 해당하는 정리다.이제 이 표현에 S를 적용하십시오.다음과 같이 S를 복용한다.

S : (α → β → γ) → (α → β) → α → α,

α = Δ, β = α → β → γ, γ = (α → β) → α → γ, 항복.

S[α = Δ = β = α → β → β → β → α → α → β] : (α → β → β → α → α → β) → Δ → (α → β → β) → Δ → (α → β → β) → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α → α

다음 결과를 분리하십시오.

S (K S) : (Δ → α → β → β → Δ → (α → β) → α → α → γ

이것은 (S (K S)의 종류에 대한 공식이다.이 정리의 특별한 경우는 Δ = (β → γ):

S (K S)[ Δ = β → β] : (β → β → β → β → β → β) → (α → β) → α → α → α → α → →.

이 마지막 공식을 K에 적용해야 한다.이번에도 α를 (β → γ)로, β를 α로 대체하여 K를 전문화한다.

K : α → β → α

K[α = β → β, β = α] : (β → α) → α → (β → γ)

이는 이전 공식의 선행 조건과 동일하므로 그 결과를 분리한다.

S (K S) K : (β → γ) → (α → β) → α → γ

변수 α와 and의 이름을 바꾸면 우리에게 주어진다.

(β → α) → (γ → β) → γ → α

증명해야 할 것이 남아 있었다.

(β → α) → (γ → β) → α의 정상적인 증명은 λ-기간으로 보는 자연적 차감에서 → → α

아래 도표는 (β → α) → (γ → β) → (γ → β) → γ → α의 자연적 차감을 증명하며, λ-표현 λa.λb.λg.(a (b g)형식(β → α) → γ → γ → α로 해석할 수 있는 방법을 보여준다.

a:β → α, b:γ → β, g:γ ⊢ b : γ → β    a:β → α, b:γ → β, g:γ ⊢ g : γ ———————————————————————————————————  ———————————————————————————————————————————————————————————————————— a:β → α, b:γ → β, g:γ ⊢ a : β → α      a:β → α, b:γ → β, g:γ ⊢ b g : β ————————————————————————————————————————————————————————————————————————가 β → α, b:γ → β, g:γ ⊢(b감속):α ————————————————————————————————————가 β → α, b:γ →β ⊢ λ g.(b감속):→ α ———————————————————————————————————————— γ:β →α ⊢ λ. b이다. λ(b감속):(γ → β)-> g., γ →α ——————————————————————————————————.——⊢ a a. b. λ g. (b g) : (β → α) -> (γ → β) -> > → α

기타 응용 프로그램

최근 유전자 프로그래밍에서 검색 공간 칸막이를 정의하는 방법으로 이형성이 제안되고 있다.^[9]이 방법은 Curry-Howard 이형성 증명(종이라고 부름)에 의해 유전자형 집합(GP 시스템에 의해 진화된 프로그램 트리)을 지수화한다.

INRIA 연구 책임자인 Bernard Lang이 지적한 바와 같이,^[10] Curry-Howard 서신은 소프트웨어의 특허성에 반대하는 주장을 구성한다: 알고리즘은 수학적 증거이므로, 전자의 특허성은 후자의 특허성을 암시할 수 있다.정리는 사유재산이 될 수 있다; 수학자는 그것을 사용하는 것에 대한 대가를 지불해야 할 것이고, 그것을 팔지만 그것의 증거를 비밀로 하고 어떤 오류에 대한 책임을 거절하는 회사를 신뢰해야 할 것이다.

일반화

여기에 열거된 서신들은 훨씬 더 멀리, 더 깊이 들어간다.예를 들어, 데카르트 폐쇄 범주는 폐쇄된 단면체 범주에 의해 일반화된다.이러한 범주의 내부 언어는 선형형 체계(선형 논리에 대응함)로 단순형 람다 미적분을 데카르트 폐쇄형 범주의 내부 언어로 일반화한다.더욱이 이것들은 끈 이론에서 중요한 역할을 하는 ^[11]거미줄에 해당한다고 보여질 수 있다.

호모토피형 이론에서도 확장된 일련의 동등성 이론이 연구되고 있는데, 이 이론은 2013년 경에 매우 활발한 연구 영역이 되었고^[update] 2018년 현재도 여전히 존재한다.^[12]여기서 유형론은 단발성 공리("평등성은 평등과 동등하다")에 의해 확장되는데, 이는 호모토피형 이론이 모든 수학(세트 이론과 고전 논리를 포함, 선택의 공리와 많은 다른 것들을 논할 수 있는 새로운 방법을 제공한다)의 기초로서 사용될 수 있도록 허용한다.즉, 증명들이 거주형식의 요소라는 Curry-Howard의 대응은 증명들의 동음이의적 등가성 개념으로 일반화된다(공간의 경로로서, 유형 이론의 정체성 유형 또는 동일성 유형이 경로로 해석되고 있다).^[13]

참조

이 글은 일반적인 참고문헌 목록을 포함하고 있지만, 그에 상응하는 인라인 인용구가 충분하지 않다. 보다 정확한 인용문을 도입하여 이 기사를 개선할 수 있도록 도와주십시오. (2010년 4월) (이 템플릿 메시지를 제거하는 방법 및 시기 알아보기)

세미날 레퍼런스

• Curry, H B (1934-09-20). "Functionality in Combinatory Logic". Proceedings of the National Academy of Sciences of the United States of America. 20 (11): 584–90. Bibcode:1934PNAS...20..584C. doi:10.1073/pnas.20.11.584. ISSN 0027-8424. PMC 1076489. PMID 16577644.
• Curry, Haskell B; Feys, Robert (1958). Craig, William (ed.). Combinatory Logic. Studies in Logic and the Foundations of Mathematics. Vol. 1. North-Holland Publishing Company. LCCN a59001593; with two sections by Craig, William; see paragraph 9E{{cite book}}: CS1 maint : 포스트스크립트(링크)
• De Bruijn, Nicolaas (1968), 수학 언어인 Automath, 수학 학부, 아인트호벤 공과대학, TH-보고서 68-WSK-052페이지의 해설과 함께 수정된 형태로 다시 인쇄됨: 자동화 및 추론, 제2권, 계산 논리에 관한 고전 논문 1967–1970, 스프링거 베라크, 1983, 페이지 159–200.
• Howard, William A. (September 1980) [original paper manuscript from 1969], "The formulae-as-types notion of construction", in Seldin, Jonathan P.; Hindley, J. Roger (eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 479–490, ISBN 978-0-12-349050-6.

통신의 연장

• Griffin, Timothy G. (1990), "The Formulae-as-Types Notion of Control", Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17–19 Jan 1990, pp. 47–57, doi:10.1145/96709.96714, ISBN 978-0-89791-343-0, S2CID 3005134.
• Parigot, Michel (1992), "Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction", International Conference on Logic Programming and Automated Reasoning: LPAR '92 Proceedings, St. Petersburg, Russia, Lecture Notes in Computer Science, vol. 624, Springer-Verlag, pp. 190–201, ISBN 978-3-540-55727-2.
• Herbelin, 후고(1995년),"ALambda-Calculus 구조 Isomorphic Gentzen-Style Sequent 미적분학 유형에", Pacholski, 레제크;Tiuryn, 예지(eds.), 컴퓨터 과학 논리, 8일 국제 워크숍 CSL 94, 카지미에시, 폴란드, 9월 25–30, 1994년, 선택된 논문, 강의 노트 컴퓨터 과학으로, 933년 vol., Springer-Verlag,를 대신하여 서명함. 61–75, ISB.N978-3-540-60017-6.
• Gabbay, Dov; de Queiroz, Ruy (1992). "Extending the Curry–Howard interpretation to linear, relevant and other resource logics". Journal of Symbolic Logic. The Journal of Symbolic Logic. Vol. 57. pp. 1319–1365. doi:10.2307/2275370. JSTOR 2275370.. (90년, 헬싱키 로직 콜로키에서 제시된 논문의 풀버전.JSL 56(3):1139–1140, 1991).
• de Queiroz, Ruy; Gabbay, Dov (1994), "Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality", in Dekker, Paul; Stokhof, Martin (eds.), Proceedings of the Ninth Amsterdam Colloquium, ILLC/Department of Philosophy, University of Amsterdam, pp. 547–565, ISBN 978-90-74795-07-4.
• de Queiroz, Ruy; Gabbay, Dov (1995), "The Functional Interpretation of the Existential Quantifier", Bulletin of the Interest Group in Pure and Applied Logics, vol. 3, pp. 243–290. (로직 콜로키움 91, 웁살라에서 제시된 논문의 풀 버전.JSL 58(2:753–754, 1993)의 개요.
• de Queiroz, Ruy; Gabbay, Dov (1997), "The Functional Interpretation of Modal Necessity", in de Rijke, Maarten (ed.), Advances in Intensional Logic, Applied Logic Series, vol. 7, Springer-Verlag, pp. 61–91, ISBN 978-0-7923-4711-8.
• de Queiroz, Ruy; Gabbay, Dov (1999), "Labelled Natural Deduction", in Ohlbach, Hans-Juergen; Reyle, Uwe (eds.), Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, Trends in Logic, vol. 7, Kluwer, pp. 173–250, ISBN 978-0-7923-5687-5.
• de Oliveira, Anjolina; de Queiroz, Ruy (1999), "A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction", Logic Journal of the Interest Group in Pure and Applied Logics, vol. 7, Oxford University Press, pp. 173–215. (Recife, 2번째 WoLLIC'95에 제시된 논문의 전체 버전.순수 및 응용 로직에서 관심 그룹 저널의 개요 4(2):330–332, 1996).
• Poernomo, 이만. Crossley, 존은 Wirsing, 마틴(2005년), Adapting Proofs-as-Programs:.그 Curry–Howard 프로토콜, Monographs 컴퓨터 과학, 스프링거,에 국제 표준 도서 번호 978-0-387-23759-6은 작가들은Curry–Howard 프로토콜을 부르는 메서드를 통해proofs-as-programs 프로그램 합성 및 프로그램 개발 문제 시급하 coarse-grain에 적응에 관한 것이다.컴퓨터 과학의 관점에서 Curry-Howard 서신에 대한 논의를 포함한다.
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina (2011), "The Functional Interpretation of Direct Computations", Electronic Notes in Theoretical Computer Science, Elsevier, 269: 19–40, doi:10.1016/j.entcs.2011.03.003. (브라질, 나탈, LSFA 2010에서 제시된 논문의 전체 버전)

철학적 해석

• de Queiroz, Ruy J.G.B. (1994), "Normalisation and language-games", Dialectica, vol. 48, pp. 83–123. (Logic Colorquium 88, Padova에서 제시된 초기 버전.JSL 55:425, 1990.)
• de Queiroz, Ruy J.G.B. (2001), "Meaning, function, purpose, usefulness, consequences – interconnected concepts", Logic Journal of the Interest Group in Pure and Applied Logics, vol. 9, pp. 693–734(1989년 8월 13~20일 Kirchberg/Wechel에서 열린 제14회 국제 비트겐슈타인 심포지엄(백주년 기념식)에서 초판이 발표되었다.)
• de Queiroz, Ruy J.G.B. (2008), "On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics", Studia Logica, 90 (2): 211–247, doi:10.1007/s11225-008-9150-5, S2CID 11321602.

합성지

• 드 브뤼앵의 기고문De Bruijn, Nicolaas Govert (1995), "On the roles of types in mathematics" (PDF), in Groote, Philippe de (ed.), De Groote 1995, pp. 27–54.
• 는 Curry-Howard 통신에 대한 합성 서론을 포함하고 있다Geuvers, Herman (1995), "The Calculus of Constructions and Higher Order Logic", De Groote 1995, pp. 139–191.
• 는 Curry-Howard 통신에 대한 합성 서론을 포함하고 있다Gallier, Jean H. (1995), "On the Correspondence between Proofs and Lambda-Terms" (PDF), De Groote 1995, pp. 55–138.
• Wadler, Philip (2014), "Propositions as Types" (PDF), Communications of the ACM, 58 (12): 75–84, doi:10.1145/2699407, S2CID 11957500

책들

• 는De Groote, Philippe, ed. (1995), The Curry–Howard Isomorphism, Cahiers du Centre de Logique (Université catholique de Louvain), vol. 8, Academia-Bruylant, ISBN 978-2-87209-363-2 드 브뤼옌의 논문과 몇 개의 다른 논문인 커리-피이스와 하워드의 논문을 재현한다.
• 그 Curry–Howard 유질 동상에 쇠 렌센, 모르텐 하이네, Urzyczyn, Paweł(2006년)[1998년], 강의, 논리의 연구들과 수학의 기초, vol. 149, 엘제비어 과학, CiteSeerX 10.1.1.17.7385, 아이 에스비엔 978-0-444-52077-7, th등에 초점을 맞추는Curry–Howard 통신에 대해 발표를 포함한다 입증 이론 및 형식 이론, 위에 노트.e편지 formulae-as-types
• Girard, Jean-Yves (1987–1990), Proof and Types, Cambridge Tracts in Theoretical Computer Science, vol. 7, Translated by and with appendices by Lafont, Yves and Taylor, Paul, Cambridge University Press, ISBN 0-521-37181-3, archived from the original on 2008-04-18, Curry-Howard 서신 발표와 함께 증명 이론에 대한 노트.
• Thompson, Simon (1991), Type Theory and Functional Programming, Addison–Wesley, ISBN 0-201-41667-0.
• Poernomo, 이만. Crossley, 존은 Wirsing, 마틴(2005년), Adapting Proofs-as-Programs:.그 Curry–Howard 프로토콜, Monographs 컴퓨터 과학, 스프링거,에 국제 표준 도서 번호 978-0-387-23759-6은 작가들은Curry–Howard 프로토콜을 부르는 메서드를 통해proofs-as-programs 프로그램 합성 및 프로그램 개발 문제 시급하 coarse-grain에 적응에 관한 것이다.컴퓨터 과학의 관점에서 Curry-Howard 서신에 대한 논의를 포함한다.
• Binard, F.; Felty, A. (2008), "Genetic programming with polymorphic types and higher-order functions" (PDF), Proceedings of the 10th annual conference on Genetic and evolutionary computation, Association for Computing Machinery, pp. 1187–94, doi:10.1145/1389095.1389330, ISBN 9781605581309, S2CID 3669630
• de Queiroz, Ruy J.G.B.; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011), The Functional Interpretation of Logical Deduction, Advances in Logic, vol. 5, Imperial College Press/World Scientific, ISBN 978-981-4360-95-1.
• Mimram, Samuel (2020), Program = proof, Independently published, ISBN 979-8615591839

추가 읽기

• Johnstone, P.T. (2002), "D4.2 λ-Calculus and cartesian closed categories", Sketches of an Elephant, A Topos Theory Compendium, vol. 2, Clarendon Press, pp. 951–962, ISBN 978-0-19-851598-2 — Curry-Howard 서신에서 "어떻게 되는가"에 대한 범주적 견해를 제공한다.

외부 링크

위키북 하스켈에는 다음과 같은 주제의 페이지가 있다.커리-하워드 이소모르프

• 하워드 온 커리하워드
• 하스켈의 커리-하워드 통신
• 모나드 리더 6: 고전적인 나라의 모험: 커리-하워드 인 하스켈, 피어스의 법칙