ABSTRACTION IN COMBINATORY LOGIC AND LAMBDA CALCULUS

^x x = I = S K K ; I x = x
^x a = K a (x not in a) ; K a x = a
^x (a b) = S (^x a) (^x b) or ^x (f x (g x)) = S f g ; S f g x = f x (g x)


ABSTRACTION IN J

^y y = ] 
^y a = ] @ a = ] & a  
^y (f y) = f
^y (f b) = f @ (^y b) = f & (^y b)
^y (a f b) = (^y a) f (^y b)

x^y x = [
x^y y = ]
x^y a = (] @ a) @ [ = (] & a) @ [
x^y (f x) = f @ [
x^y (f y) = f @ ]
x^y (f b) = f @ (x^y b) 
x^y (x f y) = f
x^y (a f b) = (x^y a) f (x^y b)


F@G y = F (G y) ; x F@G y = F (x G y)
F&G y = F (G y) ; x F&G y = (G x) F (G y)
(G H) y = G y (H y) ; x (G H) y = x G (H y)
(F G H) y = (F y) G (H y) ; x (F G H) y = (x F y) G (x H y)


Example :
 
trace =: 3 : 0
    (, =/ ~ i. # y) +/ . * ((((0 & {) * 1 & {) , 2 & }.) $ y) $ , y
)

trace = ^y ( (, =/ ~ i. # y) +/ . * ((((0 & {) * 1 & {) , 2 & }.) $ y) $ , y ) = ^y (a f b)
 = ^y(, =/ ~ i. # y) +/ . * ^y(((((0 & {) * 1 & {) , 2 & }.) $ y) $ , y)
 = (, & (=/~) & i. & #) +/ . * (^y ((((0 & {) * 1 & {) , 2 & }.) $ y)) $ (^y (, y))
 = (, & (=/~) & i. & #) +/ . * ((((0 & {) * 1 & {) , 2 & }.) & $) $ ,

trace =: (, & (=/~) & i. & #) +/ . * ((((0 & {) * 1 & {) , 2 & }.) & $) $ ,