カリー＝ハワード同型対応
↑ Sørenson, Morten; Urzyczyn, Paweł, Lectures on the Curry-Howard Isomorphism, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385
↑ Goldblatt, “7.6 Grothendieck Topology as Intuitionistic Modality”, Mathematical Modal Logic: A Model of its Evolution, pp. 76–81, http://homepages.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf
↑ Benton; Bierman; de Paiva (1998), “Computational types from a logical perspective”, Journal of Functional Programming 8: 177–193
↑ F. Binard and A. Felty, "Genetic programming with polymorphic types and higher-order functions." In Proceedings of the 10th annual conference on Genetic and evolutionary computation, pages 1187 1194, 2008.
コンビネータからなる集合の完全性の結果もまた翻訳できる。例えば、 one-point basis X {\displaystyle X} は任意のCL項を表現できることが知られている。このコンビネータから公理図式
( ( ( α → ( β → γ ) ) → ( ( α → β ) → ( α → γ ) ) ) → ( ( δ → ( ε → δ ) ) → ξ ) ) → ξ {\displaystyle (((\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma )))\to ((\delta \to (\varepsilon \to \delta ))\to \xi ))\to \xi }
が得られる。これは X {\displaystyle X} の主要型( X {\displaystyle X} の可能な型で代入に関して極小なもの)である。 X {\displaystyle X} コンビネータの完全性から、上に挙げた唯一の公理図式から次の公理図式が証明可能であることが従う:
( α → ( β → α ) ) {\displaystyle (\alpha \to (\beta \to \alpha ))}
( α → ( β → γ ) ) → ( ( α → β ) → ( α → γ ) ) {\displaystyle (\alpha \to (\beta \to \gamma ))\to ((\alpha \to \beta )\to (\alpha \to \gamma ))}
t {\displaystyle t} がモルフィズムならば λ t {\displaystyle \lambda t} はモルフィズムである、
t {\displaystyle t} と u {\displaystyle u} がモルフィズムならば ⟨ t , u ⟩ {\displaystyle \langle t,u\rangle } と u ∘ t {\displaystyle u\circ t} はモルフィズムである。
Well-definedなモルフィズム(型付きの項)は以下の型付け規則にしたがって構成される:
恒等射:
i d : α ⟶ α {\displaystyle {\frac {}{id:\alpha \longrightarrow \alpha }}}
合成:
t : α ⟶ β u : β ⟶ γ u ∘ t : α ⟶ γ {\displaystyle {\frac {t:\alpha \longrightarrow \beta \qquad u:\beta \longrightarrow \gamma }{u\circ t:\alpha \longrightarrow \gamma }}}
終対象:
⋆ : α ⟶ ⊤ {\displaystyle {\frac {}{\star :\alpha \longrightarrow \top }}}
直積: