penteract 2 days 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)
Reply View 2 replies
  • marvinborner 2 days 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)
  ...
    Reply View 1 reply
    • 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!
      Reply View 0 replies