View file src/j/abstraction.ijs - Download
NB. Abstraction
NB. ^y.expr ; x^y.expr ; u^.expr ; u^v.expr
NB. ^y.y = ]
] 123
NB. ^y.a = ] @ a = ] & a
(] @ 123) 456
(] & 123) 456
NB. ^y.(fy) = f
NB. ^y.(fz) = f @: ^y.z
NB. (f @: ^y.z) t = f ((^y.z)t)
NB. ex. ^y.(- +: y) = - @: +:
NB. (- @: +:) t = - +: t
(- @: +:) 3
- +: 3
NB. ^y.(sft) = (^y.s) f (^y.t)
NB. ((^y.s) f (^y.t)) z = ((^y.s)z) f ((^y.t)z)
NB. ex. ^y.(>: y) * (+: y)) = >: * +:
NB. (>: * +:) z = (>: z) * (+: z)
(>: * +:) 3
(>: 3) * (+: 3)
NB. x^y.x = [
NB. x [ y = x
123 [ 456
NB. x^y.y = ]
NB. x ] y = y
123 ]456
NB. x^y.z = (]@z) @ [
NB. x (F@G) y = F (xGy)
NB. x ((]@z) @ [) y = (]@z) (x[y) = (]@z) x = z
NB. ex. x^y.123 = (]@123) @ [
456 ((]@123) @ [) 789
NB. x^y.fx = f@[
NB. x^y.fy = f@[
NB. x^y.(xfy) = f
NB. x^y.(fz) = f @: (x^y.z)
NB. s (f @: (x^y.z)) t = f (x (x^y.z) t)
NB. ex. x^y.(+: x-y) = +: @: -
NB. s (+: @: -) t = +: (s - t)
8 (+: @: -) 5
+: (8 - 5)
NB. x^y.(qfr) = (x^y.q) f (x^y.r)
NB. s ((x^y.q) f (x^y.r)) t = (s (x^y.q) r) f (s (x^y.r) t)
NB. ex. x^y.((x+y)*(x-y)) = + * -
NB. s (+ * -) t = (s+t) * (s-t)
6 (+ * -) 3
(6+3) * (6-3)
3 (+ [. *) 5 NB. LEV : left verb
3 (+ ]. *) 5 NB. DEX : right verb
8 (- [.) 3
(5 (]. -)) 3
NB. u^v.w = ]. (]. w)
8 (9 (]. (]. -)) 1) 3
8 (+ (]. (]. -)) *) 3
8 (+ (]. (]. -)) 1) 3
8 (9 (]. (]. -)) *) 3
NB. Verb identity
vid =: 1 : 'u'
(- vid) 3
8 (- vid) 3
(5 (]. +)) / 1 2 3
(5 ((]. +) /)) 1 2 3
(- ((]. +) /)) 1 2 3
(8 (]. -)) 3
(]@9)5
((]@9) (].(]. -)) (]@1)) 3
((]@9)(].(]. -))(]@1)) 3
1 (]. (]. 123)) 9
(* ((]. 5) (]. -))) 3
(* ((]. +) (]. -))) 3
(* ((]. (]. 5)) (]. -)) +) 3
(9 ((]. (]. 5)) (]. -)) +) 3
(9 ((]. (]. 5)) (]. -)) 1) 3
(9 ((]. (]. +)) (]. -)) 1) 3
(9 ((]. (]. +)) (]. -)) +) 3
(* ((]. (]. +)) (]. -)) +) 3
(* ((]. (]. +)) (]. -)) 1) 3
NB. Select monad
sm =: 1 : 'if. u=1 do. >: elseif. u=2 do. +: else. - end.'
1 sm
(1 sm) 6
(2 sm) 6
(3 sm) 6
ah =: 1 : '-: u'
6 ah
NB. x^.(ya) = (x^.y) a
NB. z (x^.(ya)) = z ((x^.y) a) = (z (x^.y)) a because z (b a) = (z b) a
NB. cf. https://code.jsoftware.com/wiki/Vocabulary/fork#invisiblemodifiers :
NB. A0 A1 adv (u A0) A1
NB. ex. x^.y = ah : z (ah a) = (z ah) a
(2 (ah sm)) 6
(4 (ah sm)) 6
(6 (ah sm)) 6
((2 ah) sm) 6
((4 ah) sm) 6
((6 ah) sm) 6
as =: 1 : '>: u'
5 as
b =: 1 : '1 u'
as b NB. It does not work because u must be a verb or a noun and cannot be an adverb
applyto1 =: 1 : 'u 1'
applyto6 =: 1 : 'u 6'
NB. x^.(ua) = (x^.u) a
NB. z (x^.(ua)) = z ((x^.u) a) = (z (x^.u)) a because z (b a) = (z b) a
NB. ex. x^.u = sm, a = applyto6
NB. z (sm applyto6) = (z sm) applyto6
1 (sm applyto6)
2 (sm applyto6)
3 (sm applyto6)
(1 sm) applyto6
(2 sm) applyto6
(3 sm) applyto6
NB. u^.(xa) = (u^.x) a
NB. w (u^.(xa)) = w ((u^.x) a) = (w (u^.x)) a because w (b a) = (w b) a
NB. ex. u^.x = applyto1, a = sm
NB. w (applyto1 sm) = (w applyto1) sm
(>: (applyto1 sm)) 6
(+: (applyto1 sm)) 6
(- (applyto1 sm)) 6
((>: applyto1) sm) 6
((+: applyto1) sm) 6
((- applyto1) sm) 6
NB. u^.(va) = (u^.v) a
NB. w (u^.(va)) = w ((u^.v) a) = (w (u^.v)) a because w (b a) = (w b) a
NB. ex. u^.v = ^:2, a = applyto6
NB. w ((^:2) applyto6) = (w (^:2)) applyto6
>: ((^:2) applyto6)
+: ((^:2) applyto6)
- ((^:2) applyto6)
(>: (^:2)) applyto6
(+: (^:2)) applyto6
(- (^:2)) applyto6
NB. x^y.(za) = (x^y.z) a
NB. s (x^y.za) t = s ((x^y.z) a) t = (s (x^y.z) t) a because s (c a) t = = (s c t) a
NB. cf. https://code.jsoftware.com/wiki/Vocabulary/fork#invisiblemodifiers :
NB. C0 A1 conj (u C0 v) A1
minus =: 2 : 'u - v'
8 minus 3
(10 (minus sm) 9) 6
(10 (minus sm) 8) 6
(10 (minus sm) 7) 6
((10 minus 9) sm) 6
((10 minus 8) sm) 6
((10 minus 7) sm) 6