4 ms·

Fun fact: The nth composition combinator can be created by applying the b combinator to the nth Church numeral: (1 b) ~> λgfx.(g (f x)) (2 b) ~> λhgfx.(h (

Fun fact: The nth composition combinator can be created by applying the b combinator to the nth Church numeral: (1 b) ~> λgfx.(g (f x)) (2 b) ~> λhgfx.(h (g (f x))) (3 b) ~> λihgfx.(i (h (g (f x)))) ... Furthermore: (X (Y b)) = (X*Y b) I use these in my bruijn programming language in the form of infix/prefix operators. [1] [1] https://bruijn.marvinborner.de/std/Combinator.bruijn.html#b https://bruijn.marvinborner.de/std/Combinator.bruijn.html#b

penteract 2y ago
I think you've got the first claim wrong - for a church numeral N, (N b g f) appears to give the composition of g and f with f taking N arguments. 2 b = (λf x.f (f x)) b ~> λx.b(b x) = λx.(λgfy.(g (f y))) (λabc.(a (b c)) x) ~> λx.(λfy.(λabc.(a (b c)) x) (f y)) ~> λxfy.(λbc.(x (b c))) (f y) ~> λxfy.(λc.(x ((f y) c))) = λxfyc.(x (f y c)) (3 b) ~> λihgfx.i (h g f x)
- marvinborner 2y ago
  Ah yes, you're right. I messed up the associativity in the reductions. (2 b) ~> λhgfx.(h ((g f) x)) (3 b) ~> λihgfx.(i (((h g) f) x)) ... It still does what most interpretations would consider the "nth composition combinator": (1 b f g) x = f (g x) (2 b f g) x y = f (g x y) (3 b f g) x y z = f (g x y z) ...
  - marvinborner 2y ago
    Okay, you've definitely nerd-sniped me here. Actually producing my initial reductions is not as trivial as I thought. Still, I came up with a solution that works for n>2: d = λλλλ(3 2 (1 0)) # common d' = λλλλλ(4 3 2 (1 0)) # common weird = λλλλλ(4 (d (3 2)) 1 0) Here I use de Bruijn indices instead of named variables and write Church numerals as <n>. Then, (<n-3> weird d' b) ~> λ^{n+1}(n (n-1 (n-2 ... (1 0)..))) I could explain it in detail if anyone's interested. There should be some more elegant solutions though, so give it a try!

penteract 2y ago

I think you've got the first claim wrong - for a church numeral N, (N b g f) appears to give the composition of g and f with f taking N arguments. 2 b = (λf x.f (f x)) b ~> λx.b(b x) = λx.(λgfy.(g (f y))) (λabc.(a (b c)) x) ~> λx.(λfy.(λabc.(a (b c)) x) (f y)) ~> λxfy.(λbc.(x (b c))) (f y) ~> λxfy.(λc.(x ((f y) c))) = λxfyc.(x (f y c)) (3 b) ~> λihgfx.i (h g f x)

marvinborner 2y ago
Ah yes, you're right. I messed up the associativity in the reductions. (2 b) ~> λhgfx.(h ((g f) x)) (3 b) ~> λihgfx.(i (((h g) f) x)) ... It still does what most interpretations would consider the "nth composition combinator": (1 b f g) x = f (g x) (2 b f g) x y = f (g x y) (3 b f g) x y z = f (g x y z) ...
- marvinborner 2y ago
  Okay, you've definitely nerd-sniped me here. Actually producing my initial reductions is not as trivial as I thought. Still, I came up with a solution that works for n>2: d = λλλλ(3 2 (1 0)) # common d' = λλλλλ(4 3 2 (1 0)) # common weird = λλλλλ(4 (d (3 2)) 1 0) Here I use de Bruijn indices instead of named variables and write Church numerals as <n>. Then, (<n-3> weird d' b) ~> λ^{n+1}(n (n-1 (n-2 ... (1 0)..))) I could explain it in detail if anyone's interested. There should be some more elegant solutions though, so give it a try!