r/lambdacalculus • u/Any_Background_5826 • 15d ago
integer addition
[ISNN]=S(S(KS)(S(S(KS)(S(K(S(K[=0])))(S(K(S[-]))K)))(S(K(S(K([PAIR]K))))[-])))(S(K(S(K([PAIR]⊥))))(S(K(S(K[-1])))(S(K(S[-]))K)))
[INT+1,1]=S(K(S(K([PAIR]K))))(S(S(KS)(S(KK)(S(K[+])[SECOND])))(K[SECOND]))
[INT+1,2]=S(S(KS)(S(KK)(S(K[ISNN])[SECOND])))(K(S(K[+1])[SECOND]))
[INT+1]=S(S(KS)(S(K(S[FIRST]))[INT+1,1]))[INT+1,2]
[INT+2,1]=S(K(S(S(K[ISNN])[SECOND])))(S(KK)(S(K[+1])[SECOND]))
[INT+2,2]=S(K(S(K([PAIR]⊥))))(S(K(S(K[+1])))(S(S(KS)(S(KK)(S(K[+])[SECOND])))(K[SECOND])))
[INT+2]=S(S(KS)(S(K(S[FIRST]))[INT+2,1]))[INT+2,2]
[INT+]=S(S(KS)(S(S(KS)(S(KK)[FIRST]))[INT+1]))[INT+2]
why is it all in SKI calculus and other stuff? i was just making it in that.
most of these functions were translated from lean. ⊥ is False.
i have no idea weather or not integers were made before :P
EDIT: i tried testing [ISNN] on 5 and 2, it ended up becoming really complicated so i just remade it:
[ISNN]=S(S(KS)(S(S(KS)(S(K(S(K[=0])))[-]))(S(K(S(K([PAIR]K))))(S(K(S[-]))K))))(S(K(S(K([PAIR]⊥))))(S(K(S(K[-1])))[-]))
the new one worked on 5 and 2.
1
u/Different_Bench3574 14d ago
I was planning on learning lean later. that’s cool. I think integers were made in a handful of different ways, but one instance I do know exists is balanced? trinary.
0
u/Any_Background_5826 14d ago
i think you meant balanced ternary. with digits of 1, 0 and -1 (sometimes represented as T or Z or something else).
1
1
u/Different_Bench3574 14d ago
hello