> 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 diagrammatic solution the author uses is related to something else I've been interested in, namely Peirce's Existential Graphs[2]. They are also based on diagrammatic representations of mathematical objects with a small set (somewhere between 3 and 6 depending on how you count inversion) of permissible rewrites. Existential Graphs are powerful enough to represent propositional or predicate logic with the exact same rules of inference! There is also an extension for something equivalent to Tarski's modal logic, but I haven't looked into it really. Peirce also designed existential graphs to be amenable to uninterpreted manipulation.
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.
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!
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 saw what each #reduce c c ... c did to explore the "palette" I had to work with, and then accidentally stumbled upon the answer that way. I also stumbled on the c (c c) c solution.
May as well include a formalized proof while we're at it:
def c (g : β → γ) (f : α → β) (x : α) : γ := g (f x)
example (h : γ → δ) (g : β → γ) (f : α → β) (x : α) :
h (g (f x)) = (c (c c) c) h g f x :=
rfl
-- Or
example :
(fun (h : γ → δ) (g : β → γ) (f : α → β) (x : α) => h (g (f x)))
= (c (c c) c) :=
rfl
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!
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.
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!
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
We need to start somewhere:
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
Okay, we knew this wouldn't work, does a solution exist if we apply `c` to a single argument?
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
Nope, it can't: `c` allows its 3rd argument to be an arbitrary type `y`, but we know the corresponding argument to `answer` should be constrained to a function type `x -> y`. So we need to fully apply `c`.
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
Okay, great, we'll be done if we can find values for our typed holes. Again, we need to start somewhere:
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
Again, the shape of [the 2nd] `c` is wrong here: we need a function whose 3rd argument is a function of some sort, not an arbitrary type (NB in retrospect we could've realized this by looking at the shape of `_1`'s type). Let's try the simplest possible option:
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
We seem to be on the right track here: the 2nd `c` now typechecks. Even better, `_3` has a familiar looking type: it looks suspiciously similar to the type of `c`. Let's see if that works.
answer = c (c c) _2
- Found hole: _2 :: (y -> z) -> (x -> y) -> x -> z
Where: ‘y’, ‘x’, ‘z’ are rigid type variables bound by
The final piece of the puzzle is now hopefully obvious:
answer = c (c c) c
Much like the article's author (which I read after finding my own solution), I don't feel like I gained any great insight through this process, other than how useful it is to have good compiler error messages alongside features like typed holes.
> 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.
The diagrammatic solution the author uses is related to something else I've been interested in, namely Peirce's Existential Graphs[2]. They are also based on diagrammatic representations of mathematical objects with a small set (somewhere between 3 and 6 depending on how you count inversion) of permissible rewrites. Existential Graphs are powerful enough to represent propositional or predicate logic with the exact same rules of inference! There is also an extension for something equivalent to Tarski's modal logic, but I haven't looked into it really. Peirce also designed existential graphs to be amenable to uninterpreted manipulation.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:
Furthermore: 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
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.
Ah yes, you're right. I messed up the associativity in the reductions.
It still does what most interpretations would consider the "nth composition combinator":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:
Here I use de Bruijn indices instead of named variables and write Church numerals as <n>.Then,
I could explain it in detail if anyone's interested. There should be some more elegant solutions though, so give it a try!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:
I used Lean too earlier today :-)
I saw what each #reduce c c ... c did to explore the "palette" I had to work with, and then accidentally stumbled upon the answer that way. I also stumbled on the c (c c) c solution.
May as well include a formalized proof while we're at it:
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 happened to notice the exact same thing when playing with this puzzle in Lean!
I got c(c(c))(c).
My steps:
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.
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
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:
We need to start somewhere: Okay, we knew this wouldn't work, does a solution exist if we apply `c` to a single argument? Nope, it can't: `c` allows its 3rd argument to be an arbitrary type `y`, but we know the corresponding argument to `answer` should be constrained to a function type `x -> y`. So we need to fully apply `c`. Okay, great, we'll be done if we can find values for our typed holes. Again, we need to start somewhere: Again, the shape of [the 2nd] `c` is wrong here: we need a function whose 3rd argument is a function of some sort, not an arbitrary type (NB in retrospect we could've realized this by looking at the shape of `_1`'s type). Let's try the simplest possible option: We seem to be on the right track here: the 2nd `c` now typechecks. Even better, `_3` has a familiar looking type: it looks suspiciously similar to the type of `c`. Let's see if that works. The final piece of the puzzle is now hopefully obvious: Much like the article's author (which I read after finding my own solution), I don't feel like I gained any great insight through this process, other than how useful it is to have good compiler error messages alongside features like typed holes.I got h = c(c)(c)(c)(c), just by playing around with it