SKIコンビネータ計算
SII は引数をそれ自身に適用させる項である:
SIIα = Iα(Iα) = αα
この項を用いて SII(SII) と表される項は正規形を持たない。すなわち簡約が終了しないという性質を持つ。
S(K(SII))(S(S(KS)K)(K(SII))) は第一引数の不動点を与える項であり、Yで表す。Yコンビネータは次を満たす:
Yx = x(Yx)
このような性質を持つ閉項を不動点コンビネータといい、不動点コンビネータを用いることで再帰的呼び出しを含む項を定義できる。詳細は不動点コンビネータを参照。
SKIコンビネータ論理の項は次の規則により帰納的に定義される:
定数記号(ここではS、K、I)及び変数記号は項である。この形の項を原子(atom)という。
M と N が項ならば, (MN)は項である。この形の項を適用(application)という。
以上より項とわかるもののみを項という。
変数記号を含まない項を閉項といい、SKIのみから構成される項を結合子(コンビネータ)という。適用は左結合であるものとし、括弧を省略するのが普通である。SKIコンビネータ計算は次の簡約規則
S M N R → M R ( N R ) {\displaystyle {\boldsymbol {S}}MNR\to MR\left(NR\right)}
K M N → M {\displaystyle {\boldsymbol {K}}MN\to M}
I M → M {\displaystyle {\boldsymbol {I}}M\to M}
からなる項書換え系である。矢印の左辺の形をリデックス、右辺の形をコントラクタムという。矢印によって移る項の変形をweak簡約という。簡約関係の同値閉包をweak同値性といい、普通、等号を用いて表す。