Talk:Detrovert

any proof for TC? Yayimhere (talk) 18:37, 23 August 2024 (UTC)

SKI calculus can be implemented like this (untested):

(Expr() K ~ Expr() S ~ Expr() App ~ Expr(X Expr Y Expr)) (App w1(X w2 Y b) App w2(X w3 Y a) K w3() Expr a() -> *a()) (App w1(X w2 Y c) App w2(X w3 Y b) App w3(X w4 Y a) S w4() Expr a() Expr b() Expr c() -> App *x(X a Y c) App *y(X b Y c) *w1(X x Y y))

Note that I is redundant because it is equal to S K K --Hakerh400 (talk) 07:16, 24 August 2024 (UTC)

thx. yes ik the thing with I --(this comment by Yayimhere at 07:28, 24 August 2024 UTC; please sign your comments with ~~~~)