A Curried Composition Puzzle

> It's almost as if wanting a meaningful, intuitive solution prevented me from solving the problem.

This theme shows up repeatedly in Dijkstra's work[1]. The symbol manipulation is itself a calculation.

  As a final influence I must mention our desire to let the symbols do the work —more precisely: as much of the work as profitably possible—. The intuitive mathematician feels that he understands what he is talking about and uses formulae primarily to summarize situations and relations in to him familiar universes. When he seems to derive one formula from another, the transformations he allows are those that seem to be true in the universe he has in mind. The formalist, however, prefers to manipulate his formulae, temporarily ignoring all interpretations they might admit, the rules for the permissible symbol manipulations being formulated in terms of those symbols: the formalist calculates with uninterpreted formulae.

The tutorial I link has some nice examples of proving Frege's axioms using only a single assumed axiom and rules of inference he proved sound. Frege assumed all of his axioms. I mean no disrespect to Frege, but it illustrates just how powerful existential graphs are.

[1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130...

[2] https://www.jfsowa.com/pubs/egtut.pdf or https://www.jfsowa.com/peirce/ms514.htm

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))))
  ...

  (X (Y b)) = (X*Y b)

[1] https://bruijn.marvinborner.de/std/Combinator.bruijn.html#b

I appreciate the author including the four different syntaxes of the same problem. Some syntaxes are more natural for some people depending on your experience, and I don’t think it takes away from the problem. On my final in a functional programming class I took a problem involving a Y-combinator which was given in Lisp, converted it to JavaScript, solved it in JavaScript, and then converted the syntax back to Lisp.

You can solve this by working backwards from the outside in, replacing a (b x) with c a b x wherever you can (not inside out, or else you get into an infinite loop!)

A cute alternative expression to solve the curried composition puzzle is c c c c c, just 5 c's in a row :)

Finally, Lean is a great language to do these puzzles in. See the following code:

  /-- Compose! -/
  def c (g : β → γ) (f : α → β) := g ∘ f
  /-
  ?f (?g (?h ?x))
  -/
  #reduce c (c c) c ?f ?g ?h ?x
  /-
  ?f (?g (?h ?x))
  -/
  #reduce c c c c c ?f ?g ?h ?x

I ended up solving the problem as `c c c c c`, which reminded me of a fun fact I once derived about repeated applications of that composition operator. If we call this sort of expression of `n` chained composition operators `n`-fold composition, then for `n >= 6` (i.e. starting at `c c c c c c`), `n`-fold composition has the same type and semantics as `n+4`-fold composition. Not a particularly deep insight, but neat!

I got c(c(c))(c).

My steps:

  c(g):      (f) => (x) => g(f(x))
  c(c):      (f) => (x) => c(f(x)) = (g) => (y) => f(x)(g(y)), or
             (f) => (x) => (g) => (y) => f(x)(g(y))
  c(c)(c):   (x) => c(c(x)) = (f) => (y) => c(x)(f(y)) = (z) => x(f(y)(z)), or
             (x) => (f) => (y) => (z) => x(f(y)(z)) # close!
  c(c(c)):   (f) => (x) => c(c)(f(x)) = (y) => c(f(x)(y)) = (g) => (z) => f(x)(y)(g(z)), or
             (f) => (x) => (y) => (g) => (z) => f(x)(y)(g(z)) # We just need to substitute f with c
  c(c(c))(c): (h) => c(c)(c(h)) = (g) => c(c(h)(g)) = (f) => (x) => c(h)(g)(f(x)) = h(g(f(x)), or
              (h) => (g) => (f) => (x) => h(g(f(x)))

The first thing I did was head over to the Combinator Birds[0] site to see what this one is called. It’s the B3 combinator, also known as the Becard.

It’s really fun to puzzle out combinators made from smaller combinators, but it doesn’t take me long to find myself in the tall grass. SKI calculus goes from 0 to insane so quickly!

0: https://www.angelfire.com/tx4/cus/combinator/birds.html

The way they do it is actually to express it in terms of combinatory logic. If we have a combinator Bxyz = x(yz), how can we express combinator Axyzw = x(y(zw)) using only B?

The famous Smullyan's book To Mock a Mockingbird is full of little puzzles like this.

Somewhat surprisingly (to me at least), this puzzle is "solvable" pretty quickly by using the Haskell typechecker interactively. Here's what I did, along with the compiler's error messages.

Start with some definitions:

    c :: (b -> c) -> (a -> b) -> (a -> c)
    c = \g f x -> g (f x) -- alternatively, c = (.)

    answer :: (y -> z) -> (x -> y) -> (w -> x) -> (w -> z)
    answer = undefined

    answer = c

    - Couldn't match type ‘x’ with ‘w -> x’
      Expected: (y -> z) -> (x -> y) -> (w -> x) -> w -> z
        Actual: (y -> z) -> (x -> y) -> x -> z

    answer = c _1
    
    - Couldn't match type ‘y’ with ‘x -> y’
      Expected: (y -> z) -> (x -> y) -> (w -> x) -> w -> z
        Actual: (y -> z) -> y -> (w -> x) -> w -> z

    - Found hole: _1 :: z -> (w -> x) -> w -> z

    answer = c _1 _2

    - Found hole: _1 :: b0 -> (x -> y) -> (w -> x) -> w -> z
      Where: ‘b0’ is an ambiguous type variable

    - Found hole: _2 :: (y -> z) -> b0
      Where: ‘b0’ is an ambiguous type variable

    answer = c c _2

    - Couldn't match type ‘x’ with ‘w -> x’
      Expected: (y -> w -> z) -> (x -> y) -> (w -> x) -> w -> z
        Actual: (y -> w -> z) -> (x -> y) -> x -> w -> z

    - Found hole: _2 :: (y -> z) -> y -> w -> z

    answer = c (c _3) _2

    - Found hole: _3 :: b0 -> (w -> x) -> w -> z
      Where: ‘b0’ is an ambiguous type variable

    - Found hole: _2 :: (y -> z) -> (x -> y) -> b0
      Where: ‘b0’ is an ambiguous type variable

    answer = c (c c) _2

    - Found hole: _2 :: (y -> z) -> (x -> y) -> x -> z
      Where: ‘y’, ‘x’, ‘z’ are rigid type variables bound by

    answer = c (c c) c

I got h = c(c)(c)(c)(c), just by playing around with it