Combinatorics problem: you're arranging 10 people (A .. J) in a row. A and B must sit next to each other. How many arrangements? How could writing this problem as a program help scaffold the problem-solving process?
-
Show this thread
-
It seems like there are two styles of programming, which I call "subtractive" and "additive" (like 3D printing). permutations('A' .. 'J').filter(λ p: 'AB' in p or 'BA' in p) ^ subtractive means enumerate all possibilities, then remove constraint violations.
1 reply 0 retweets 4 likesShow this thread -
But subtractive is hard to reason about analytically -- how to compute len(..)? Then we rewrite additively: permutations(['AB'] + 'C' .. 'J') + permutations(['BA'] + 'C' .. 'J') Now we can easily derive the formula permutations(9) * 2.
2 replies 0 retweets 2 likesShow this thread -
Maybe this is actually a compiler problem: how can you rewrite the subtractive program (which naturally falls out of the problem statement) into an additive one (which is easily countable)? i.e. how do you remove all conditional expressions?
3 replies 0 retweets 6 likesShow this thread -
Replying to @wcrichton
hmm... makes me think of the examples ive seen about squiggol (https://en.wikipedia.org/wiki/Bird%E2%80%93Meertens_formalism …), which i know less about than i ought to
1 reply 0 retweets 2 likes -
Replying to @sarah_zrf @wcrichton
this kind of dichotomy is also definitely very present when working in a proof assistant—i wonder whether it's been pinned down in the proof automation/engineering literature?
1 reply 0 retweets 2 likes -
Replying to @sarah_zrf
When I was learning Lean and writing proofs about lambda calculus, I first wrote axioms as functions. But I later realized I couldn't easily access exhaustiveness theorems (eg this proof must have been derived using rule A or B), so I rewrote functions as a single data type.
2 replies 0 retweets 1 like
Seems kind of similar -- you have to carefully pick your representation to ensure downstream analysis will work.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
cognitive psychology. PhD