SKIコンビネータ計算
SKIコンビネータ計算は型無しラムダ計算を単純化した、ひとつの計算モデルである。このモデルは、ある種のプログラミング言語と考えることができるが、人間によるソースコードの記述には適さない（難解プログラミング言語には時折採用される）。その代わり、このモデルは非常に単純なチューリング完全な言語であるため、アルゴリズムの数学理論においては重要である。また関数型言語を実行する抽象機械のモデルとして使っている例もある。
ラムダ計算におけるあらゆる演算は、SKIにおいて3つの定数記号S, KおよびI（これらをコンビネータと呼ぶ）および変数記号によって表現できる。2引数の関数適用演算のみを持つ形式言語の構文木と考えれば、定数記号と変数記号を葉とする二分木と捉えることもできる。 実際には、 I はモデルを簡単にするために導入されたものであり、SKIシステムを展開するにはSとKの2つで十分である。
直観主義論理との関係
コンビネータ K および S は、よく知られた次の命題論理の公理図式と対応する：
AK: A  (B  A),
AS: (A  (B  C))  ((A  B)  (A  C)).
関数適用は推論規則モーダスポネンスと対応する：
MP: 
公理 AK, AS 及び推論規則 MP は、直観主義命題論理の含意断片に対して健全かつ完全である。この体系に爆発原理 F → A と排中律に類する規則（例：パースの法則）を追加したものは古典命題論理と対応する。