一点基底について調べた
発見者 | 一点基底 | S |
K |
他 |
---|---|---|---|---|
\x.xSK |
X(X(X(XX))) |
X(X(XX)) |
I = XX , iotaで使われている |
|
John Barkley Rosser | \x.xKSK |
X(XX) |
XXX |
|
Corrado Bohm | \x.x(fS(KI))K |
X(XX) |
XX |
|
Henk Barendregt | \x.x(fS(KK))K |
X(XXX) |
XXX |
|
Jeroen Fokker | \f.fS(\xyz.x) |
X(XX) |
XX |
|
Carew Meredith | \abcd.cd(a(Kd)) |
V(XXX(XX)(XXXX(XXXX(VV))(K(XXXX)))) |
XXXX(XXXX(XXX(XX))(XX))(XX) |
V = XXXX(K(XXXX)) とする |
let’s 簡約
iotaのものを簡約する
# XX = I
XX a
= (\x.xSK) (\y.ySK) a
= ((\y.ySK) SK) a
= ((S SK) K) a
= ((SK) (KK)) a
= SK (KK) a
= (Ka) (KKa)
= a
= I a
# X(X(XX)) = K
X(X(XX))
= X(XI)
= (\x.xSK) ((\y.ySK) I)
= (\x.xSK) (I SK)
= (\x.xSK) (SK)
= (SK SK)
= ((KK) (SK))
= K
# X(X(X(XX))) = S
X(X(X(XX)))
= XK
= (\x.xSK) K
= KSK
= S