View file src/j/abstraction.out - Download

   NB. Abstraction 
   NB. ^y.expr ; x^y.expr ; u^.expr ; u^v.expr
   
   NB. ^y.y = ]
   ] 123
123
   
   NB. ^y.a = ] @ a = ] & a
   (] @ 123) 456
123
   (] & 123) 456
123
   
   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
_6
   - +: 3
_6
   
   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
24
   (>: 3) * (+: 3)
24
   
   NB. x^y.x = [
   NB. x [ y = x
   123 [ 456
123
   
   NB. x^y.y = ]
   NB. x ] y = y
   123 ]456
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  
123
   
   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
6
   +: (8 - 5)
6
   
   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
27
   (6+3) * (6-3)
27
   
   3 (+ [. *) 5  NB. LEV : left verb
8
   3 (+ ]. *) 5  NB. DEX : right verb  
15
   8 (- [.) 3    
_3
   (5 (]. -)) 3
_3
   
   NB. u^v.w = ]. (]. w)
   8 (9 (]. (]. -)) 1) 3
5
   8 (+ (]. (]. -)) *) 3
5
   8 (+ (]. (]. -)) 1) 3
5
   8 (9 (]. (]. -)) *) 3
5
   
   NB. Verb identity
   vid =: 1 : 'u'
   (- vid) 3
_3
   8 (- vid) 3
5
   
   (5 (]. +)) / 1 2 3
6
   (5 ((]. +) /)) 1 2 3
6
   (- ((]. +) /)) 1 2 3
6
   
   (8 (]. -)) 3
_3
   (]@9)5
9
   ((]@9) (].(]. -)) (]@1)) 3
_3
   ((]@9)(].(]. -))(]@1)) 3
_3
   1 (]. (]. 123)) 9
123
   
   (* ((]. 5) (]. -))) 3
_3
   (* ((]. +) (]. -))) 3
_3
   (* ((]. (]. 5)) (]. -)) +) 3
_3
   (9 ((]. (]. 5)) (]. -)) +) 3
_3
   (9 ((]. (]. 5)) (]. -)) 1) 3
_3
   (9 ((]. (]. +)) (]. -)) 1) 3
_3
   (9 ((]. (]. +)) (]. -)) +) 3
_3
   (* ((]. (]. +)) (]. -)) +) 3
_3
   (* ((]. (]. +)) (]. -)) 1) 3
_3
   
   NB. Select monad
   sm =: 1 : 'if. u=1 do. >: elseif. u=2 do. +: else. - end.'
   1 sm
>:
   (1 sm) 6
7
   (2 sm) 6
12
   (3 sm) 6
_6
   
   ah =: 1 : '-: u'
   6 ah
3
   
   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
7
   (4 (ah sm)) 6
12
   (6 (ah sm)) 6
_6
   ((2 ah) sm) 6
7
   ((4 ah) sm) 6
12
   ((6 ah) sm) 6
_6
   
   as =: 1 : '>: u'
   5 as
6
   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
as b
   
   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)
7
   2 (sm applyto6)
12
   3 (sm applyto6)
_6
   (1 sm) applyto6
7
   (2 sm) applyto6
12
   (3 sm) applyto6
_6
   
   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
12
   (+: (applyto1 sm)) 6
12
   (- (applyto1 sm)) 6
_6
   ((>: applyto1) sm) 6
12
   ((+: applyto1) sm) 6
12
   ((- applyto1) sm) 6
_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)
8
   +: ((^:2) applyto6)
24
   - ((^:2) applyto6)
6
   (>: (^:2)) applyto6
8
   (+: (^:2)) applyto6
24
   (- (^:2)) applyto6
6
   
   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
5
   (10 (minus sm) 9) 6
7
   (10 (minus sm) 8) 6
12
   (10 (minus sm) 7) 6
_6
   ((10 minus 9) sm) 6
7
   ((10 minus 8) sm) 6
12
   ((10 minus 7) sm) 6
_6