Comment by marvinborner
Comment by marvinborner 2 days 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!