The language of choice(codewords.recurse.com)
codewords.recurse.com
The language of choice
https://codewords.recurse.com/issues/four/the-language-of-choice
4 comments
Been a while since I felt smarter after reading something. Read this, and make the effort to follow along :-)
That's such a great compliment. Thanks!
> We just checked whether two different 64-bit adder circuits produce the same outputs for all 2^129 of the possible values of A, B, and carry. It took only a moment in interpreted Python. Magic!
This kind of processing is what makes me wonder on how computer, nowadays, still have foundations on _simple_ and _basic_ logic, combined and processed at zillions of repetitions per second.
This kind of processing is what makes me wonder on how computer, nowadays, still have foundations on _simple_ and _basic_ logic, combined and processed at zillions of repetitions per second.
I'm not sure I understand your comment. It isn't like it actually ran all 2^129 inputs. It created a BDD for each and determined they were the same. (Right?)
No, I understand that running such range would be impossible. What amazes me is how you can (sometimes) simplify things, and the "power" that being able do to zillions of calculations can have when you have already simplified your problem to some general proof. :) Well, that's what I meant.
I think this needs a bit more motivation (why do I want to know about BDDs) and more pictures. The code is great for playing with things and remembering better but the fundamental concepts would be clearer with more pictures.
Yes, I agree -- I ran out of time trying to get the animations I wanted with d3.js. Thanks for the feedback.
Maybe circuit diagrams of both kinds of adders and "by the end of this article we will prove that these are equivalent for all 2^192 possible inputs"?
Fabian Giesen pointed out last night that the example "carry-lookahead adder" was misnamed and it's a kind of https://en.wikipedia.org/wiki/Carry-select_adder. Oops. Going to fix that soon. I'd read the carry-lookahead article and was like "this derivation seems right but I don't see how you might invent it." Trying to fix that ended up reinventing something different. I should've noted there in the article that I felt iffy about what I'd called the circuit, even though it was functionally equivalent. (Better still of course to code up Wikipedia's version and check structural equivalence, if there'd been time.)