3 ms·
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
by 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 agoOkay, 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!