コンビネータ論理 応用

ウィキペディア

コンビネータ論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/10 14:50 UTC 版)

応用

関数型言語のコンパイル

関数型言語は、ラムダ計算がシンプルながら万能性があるため、ラムダ計算をベースとしているものが多いが、ラムダ式はコンビネータ式に変換可能であり、一種のコンパイルとも言える。David Turnerは、SASLの実装にコンビネータを利用した（SASLに限らず、一般に関数型言語の実装に応用可能である）。

Kenneth E. Iversonは、APLの後続に位置づけられるJ (プログラミング言語)で、カリーのコンビネータを基本としたプリミティブを採用し、Iversonがtacit programming（en:Tacit programming）と呼んだものを可能にした。それは、変数を含まない式で、そのようなプログラムで作業するための強力なツールに沿って行うプログラミングである。APLのような言語では、ユーザー定義の演算子を用いたclumsier mannerで暗黙のプログラミングが可能であることが判明した。(Pure Functions in APL and J)

論理学

カリー＝ハワード同型対応によれば、論理式と型が対応し、直観主義論理の含意断片のヒルベルト流の推論図と型付きコンビネータ項が対応する。 コンビネータK、Sは以下の公理型に対応する。

AK: A → (B → A),

AS: (A → (B → C)) → ((A → B) → (A → C)),

そして、関数適用はモーダスポネンスに対応する。

MP: A と A → B から B を推論できる。

コンビネータ項に直和や直積の為の定数を加え、さらに基本型としてbottom $\bot$、複合型として直積型と直和型を加えたものは、ヒルベルト流の直観主義命題論理と対応する。