SK言語で現実逃避

Kxy≡x
Sxyz≡xz(yz)

I x ≡ x = SKKx = Kx(Kx)=x
∴I = SKK

K2 x y ≡ y = Iy = K I x y
∴K2 = KI

Bxyz ≡ x(yz) = (Kxz)(yz) = S(Kx)yz = (KSx)(Kx)yz = S(KS)Kxyz
∴B = S(KS)K

Rxy ≡ yx = K2xy(Kxy) = S K2x Kx y = S(SK2)K xy
∴B = S(SK2)K


Y f ≡ f(Yf)
Y = λf.(λx.(fxx)λx.(fxx))
Yf = λx.(fxx) λx.(fxx)

λx.(fxx) x = fxx = BfIx
Yf = BfIx(BfIx) = S(BfI)(BfI)x = S(RI(Bf))(RI(Bf))
= S(RI(Bf))(RI(Bf)) = S(B(RI)Bf)(B(RI)Bf) = BS(B(RI)B)f(B(RI)Bf)
= S(BS(B(RI)B))(B(RI)B) f
∴Y = S(BS(B(RI)B))(B(RI)B)


<true>≡K
<false>≡K2

<not>x ≡ x<false><true>
= R<false>x<true>
= R<true>(R<false>x)
= B(R<true>)(R<false>)x

∴<not> ＝ B(R<true>)(R<false>)

<or>xy ≡ x<true>(y<true><false>)
= x<true>(R<true>y<false>)
= x<true>(R<false>(R<true>y))
= x<true>(B(R<false>)(R<true>)y)
= B(x<true>)(B(R<false>)(R<true>)) y
= R(B(R<false>)(R<true>)) (B(x<true>)) y
= R(B(R<false>)(R<true>)) (B(B<true>x)) y
= R(B(R<false>)(R<true>)) ( BB(B<true>) x ) y
= B (R(B(R<false>)(R<true>))) (BB(B<true>)) xy
∴<or>= B (R(B(R<false>)(R<true>))) (BB(B<true>))

<and>xy ≡ x (y <true> <false> )<false>
= B x (y<true>) <false><false>
= B(Bx)y<true><false><false>
= B B B x y <true><false><false>
= R<true>(B B B x y)<false><false>
= B(R<true>) (B B B x) y <false><false>
= B(B(R<true>)) (B B B) x y <false><false>
= R<false> ( B(B(R<true>)) (B B B) x y ) <false><false>
= B (R<false>) ( B(B(R<true>))(B B B) x ) y <false><false>
= B(B(R<false>))(B(B(R<true>))(B B B)) x y <false><false>
= R<false> (B(B(R<false>))(B(B(R<true>))(B B B)) x y) <false>
= B(R<false>) (B(B(R<false>))(B(B(R<true>))(B B B)) x) y <false>
= B(B(R<false>))B(B(R<false>))(B(B(R<true>))(B B B)) x y <false>
= R<false>(B(B(R<false>))B(B(R<false>))(B(B(R<true>))(B B B)) x y)
= B(R<false>)(B(B(R<false>))B(B(R<false>))(B(B(R<true>))(B B B)) x) y
= B(B(R<false>)(B(B(R<false>))B(B(R<false>))(B(B(R<true>))(B B B)))) x y

∴<and> = B(B(R<false>)(B(B(R<false>))B(B(R<false>))(B(B(R<true>))(B B B))))


<if>≡I

<while> p f e ≡ p e e (<while> (Bpf) (fe) )
= SpI e (S (K(<while>(Bpf))) f e)
= S(SpI)( S(K(<while>(Bpf)))f) e
= S(SpI)( S(K(B<while>(Bp)f))f) e
= S(SpI)( S(BK(B<while>(Bp)) f)f) e
= S(SpI)( BS(BK(B<while>(Bp))) f ( If ) ) e
= S(SpI)( S (BS(BK(B<while>(Bp))))I f ) e
= B (S(SpI)) (S(BS(BK(B<while>(Bp))))I) f e
= B (S(RI(Sp))) (RI ( BS(B(BS)(BK(BB(B<while>)B))) p)) f e
= B (S(B(RI)Sp)) (B(RI)(BS(B(BS)(BK(BB(B<while>)B)))) p) f e
= B (BS(B(RI)S)p) (B(RI)(BS(B(BS)(BK(BB(B<while>)B)))) p) f e
= BB(BS(B(RI)S))p (B(RI)(BS(B(BS)(BK(BB(B<while>)B)))) p) f e
= S(BB(BS(B(RI)S)))(B(RI)(BS(B(BS)(BK(BB(B<while>)B))))) p f e

<while>
= S(BB(BS(B(RI)S)))(B(RI)(BS(B(BS)(BK(BB(B<while>)B)))))
= S(BB(BS(B(RI)S)))(B(RI)(BS(B(BS)(BK( RB(B(BB)(B)<while>))))))
= S(BB(BS(B(RI)S)))(B(RI)(BS(B(BS)(BK( RB ( B(BB)(B) <while>))))))
= S(BB(BS(B(RI)S)))(B(RI)(BS( B(BS) ( B(BK)(B(RB)(B(BB)(B))) <while>))))
= S(BB(BS(B(RI)S)))(B(RI)(BS( B(B(BS))(B(BK)(B(RB)(B(BB)(B)))) <while>)))
= S(BB(BS(B(RI)S)))(B(RI)( B(BS)(B(B(BS))(B(BK)(B(RB)(B(BB)(B))))) <while>))
= S(BB(BS(B(RI)S)))( B(B(RI))(B(BS)(B(B(BS))(B(BK)(B(RB)(B(BB)(B)))))) <while>)
= B(S(BB(BS(B(RI)S))))(B(B(RI))(B(BS)(B(B(BS))(B(BK)(B(RB)(B(BB)(B))))))) <while>
= Y(B(S(BB(BS(B(RI)S))))(B(B(RI))(B(BS)(B(B(BS))(B(BK)(B(RB)(B(BB)(B))))))))

***********************************************************************

<0>sx≡x
<n+1>sx≡s(<n>sx)

<0> = K2
<n+1>sx = s(<n>sx) = Ksx(<n>sx)
= S(Ks)(<n>s)x = BSKs(<n>s)x
= S(BSK)<n>sx
∴<n+1> = S(BSK)<n>

<inc> ≡ S(BSK)

<isZero> <0> ≡ <true>
<isZero> <n+1> ≡ <false>

<isZero> <n> = <n> (K<false>) <true>
= R(K<false>)<n><true>
= R<true>(R(K<false>)<n>)
= B(R<true>)(R(K<false>)) <n>

∴<isZero> = B(R<true>)(R(K<false>))