[HN Gopher] A Curried Composition Puzzle
___________________________________________________________________
A Curried Composition Puzzle
Author : 082349872349872
Score : 81 points
Date : 2024-09-17 10:12 UTC (12 hours ago)
(HTM) web link (franklin.dyer.me)
(TXT) w3m dump (franklin.dyer.me)
| js8 wrote:
| 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.
| MatthiasPortzel wrote:
| 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.
| adregan wrote:
| 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
| User23 wrote:
| > 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.
|
| [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
| Icy0 wrote:
| 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 :
| b - g) (f : a - b) := 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
| cscscscscsc wrote:
| 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!
| dwlg00 wrote:
| 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)))
| marvinborner wrote:
| Fun fact: The nth composition combinator can be created by
| applying the b combinator to the nth Church numeral:
| (1 b) ~> lgfx.(g (f x)) (2 b) ~> lhgfx.(h (g (f x)))
| (3 b) ~> lihgfx.(i (h (g (f x)))) ...
|
| Furthermore: (X (Y b)) = (X*Y b)
|
| 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
| nimih wrote:
| 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.
| JulianChastain wrote:
| I got h = c(c)(c)(c)(c), just by playing around with it
___________________________________________________________________
(page generated 2024-09-17 23:01 UTC)