Wednesday, February 3, 2016

216: Bowie Meets Escher

Audio Link

Apologies that this podcast is a little late.   A bunch of my time has been taken up by a fun new project:  putting together a Math Mutation book.   Yes, I’ve actually found a publisher crazy enough to want one!  I’ll announce more details here as we get closer to the book’s release.    One slight downside though:  due to the realities of publishing contracts, any episodes that end up in the book will have to be taken down from the web.   Sorry about that; I pushed back a little, but they were firm on this aspect of the contract.   So, if you were planning to catch up on old episodes, be sure to download them ASAP, before they start disappearing.   Now, on to today’s topic.

With the sad passing of the musical pioneer David Bowie, it seems appropriate to try to create one more Math Mutation episode that focuses on him somehow.   You may recall that he has come up before, in our discussion on random song selection back in podcast 193.   But this time I thought it would be fun to talk about something a little different:  the climactic scene in the movie Labyrinth.   As you may recall, Labyrinth was a 1980s movie that starred Bowie, Jennifer Connelly, and lots of muppets.   Bowie played the Goblin King in this move, where the only other speaking human was Connelly, as a scared teenage girl trying to rescue her baby brother, who Bowie had kidnapped.   To catch up with him, she had to traverse a bizarre maze filled with strange traps and spooky muppet monsters.   When the girl finally catches up with the Goblin King, he is in a huge maze with staircases in every direction, clearly inspired by M.C.Escher’s classic 1953 lithograph Relativity.

Before we get into the movie, let’s talk about the original lithograph.   Relativity is one of Escher’s less absurd works, in that the 3-D structure he depicts is actually self-consistent, and can theoretically be built in three dimensions.   It centers around a triangular group of staircases, with various doorways, windows, and secondary staircases nearby, and faceless figures walking up and down in various locations.   Where the Escher mind-bending comes in is that there are multiple distinct sources of gravity in the picture, with each of the walking figures independently subscribing to one or the other, even if on the same staircase.   For example, in the staircase at the top, two figures seem to have their feet near the same stair, but the “tops” of the stairs to one of them are the “fronts” of the stairs to the other, so they are standing perpendicular to each other.   Similarly, the doors and windows each seem perfectly reasonable on their own, but all together don’t make much sense, creating multiple different impressions of which way is “up”.

As with many Escher prints, generations of college math majors have put this poster up on their walls, and enjoyed the absurd questioning of basic artistic and mathematical rules.   But is there a deeper meaning to the lithograph?   One blogger suggests that it is questioning the nature of who actually controls reality:  “Who controls the world, and reality, in this painting? It seems that the human-like figures do. By going about their everyday business they show no desire to change it. Perhaps Escher is trying to say something about human nature.  It seems as though as long as these beings can eat, walk, read, and go about their normal lives they are content to go along with the distorted world they live in, however ridiculous it is…  If we care enough to wake up and see what's going on, we will have the power to change it.”    This seems to be the most interesting analysis I can easily find on the web, and ties in nicely with some of the fan interpretations of Labyrinth.

Getting back to the movie:   as I mentioned, the climactic scene involves a chase through a Relativity-like maze, complete with inconsistent gravity from various angles.   This was before the days of cheap CGI effects, so the filmmakers actually built a large Relativity-like set, and used camera tricks to make it look like Bowie, Connelly, and the baby were subject to varying gravity in multiple directions.   Like most of the movie, this scene seemed to come out of nowhere, with nothing earlier specifically alluding to it.  Many critics panned the movie for basically that reason, just being an accelerating series of oddities with no underlying rules— initially it wasn’t much of a box office success, though it is now considered a cult classic.  In the years since it came out, legions of fans have tried to discover a deeper underlying meaning.   

The easiest interpretation is that this is just another in a long line of absurd children’s tales, with crazy magic and monsters that don’t really have much deeper meaning.   A slightly more convincing interpretation is that it’s a coming-of-age tale, where the girl learns to take on the maturity and responsibility to make her own decisions.   This would put it squarely in the typical space of many popular fantasy stories.   However, there are darker possibilities.   One website, “Vigilant Citizen”, claims that the entire movie is an allegory for mind control, with each of the obstacles in the labyrinth being somehow related to the internal world of a brainwashing victim.    This also ties in well with the resolution of the scene, where Connelly tells Bowie “You have no power over me”, and as a result finds herself safely teleported home with her baby brother.   But is an interpretation this dark really appropriate for what is largely regarded as a children’s movie?

Ultimately, I’m not sure which view is correct.  Was the final Relativity stairway chase in Labyrinth a metaphor for pulling free of mind control, or a gentler coming-of-age ritual?   Or was it just another case of the legendary Bowie choosing to be weird for weirdness’s sake?    We’ll never be able to answer those questions completely, but I have no doubt that future generations will continue to enjoy both Escher’s Relativity and David Bowie’s Labyrinth.

And this has been your math mutation for today.



References:




Wednesday, December 23, 2015

215: It's Not A Conspiracy

Audio Link


Often when we are watching science fiction shows or movies, they imagine fantastic devices that are just at the edge of possibility according to modern physics.    Ideas like death stars, faster-than-light travel, or teleportation are all things we are unlikely to see for many years, but can’t totally dismiss as potential inventions of the far future.   But every once in a while, science fiction posits something so totally absurd that I can’t help but laugh.     The other day, while watching an episode of Star Trek: Deep Space Nine, I saw an idea in this category:   a small device that would alter the laws of probability.

The plot of this episode, titled “Rivals”, involved a series of strange events on a space station.    Gamblers would win against impossible odds, the infirmary suddenly filled with victims of freak accidents, a computer search of an unsorted file list would instantly discover just the right data, and a crew member who stunk at racquetball suddenly started making impossible trick shots.    As expected for a Star Trek episode, this all boiled down to an alien technological device, in this case one that could alter the laws of probability.    Once the captain found and destroyed the device, everything could go back to normal.

Now at first you might just label this as another piece of random technobabble used to advance a sci-fi plot.    But I think this hits at a popular misconception about probability.   Many people think then when the odds of some event are low, it’s some kind of conspiracy of the universe against them.    So if you have a one-in-a-million chance of making a trick racquetball shot, why shouldn’t some gizmo be able to alter that probability and help your game?    But actually, the low probability just reflects the fact that there are a million different ways you can hit the ball, all of which are equally valid executions of the laws of physics.   The universe doesn’t really care about the one shot that we abstractly label the great trick shot:  it’s just another in a huge sea of possibilities.    Tiny variations in the angle of your aim and the force of your swing can make a major difference in where the ball goes.   You can imagine a million parallel universes in which you hit the ball, and only one of them involves you making the shot successfully.     Which one is it?   You might care, but it’s none of the universe’s business.  All are roughly equally likely, depending on your exact position and momentum when you hit the ball.

So what would it mean for an alien device to change the laws of probability?    It is theoretically possible for some specific technical gizmo attached to your arm to bias it towards the successful racquetball shot.    But a generalized probability gizmo that could enhance your shot, improve computer data searches, enable victories at roulette, and cause freak accidents?   How would this device know how to bias the universe precisely in ways that we label as “unlikely” results, in all these diverse domains?    In the racquetball shot example, we’re estimating that there are a million possibilities, so *every* shot you take will be a one-in-a-million result:  no matter what ends up happening, there was only that same tiny chance of that specific shot occurring.    So a machine that caused an “unlikely” result for events would be useless at choosing the victory shot for you— every non-victory shot is equally as likely, and there are 999,999 of them.    On the outer fringe of possibility, perhaps if the machine had full artificial intelligence capability, there might be possibilities here.  But then it would be a techno-gremlin notable mainly for its intentional meddling in other’s lives, and nobody would describe this strange robot’s actions as a change in the laws of probability.   

We can see similar laws at work in many parts of our daily lives.   Is my daughter engaged in a specific effort to make her room messy?       If I don’t enter my daughter’s room for a few weeks, books, toys, and clothes are strewn about everywhere, with barely a path available to the bed.     But is she deliberately trying to make the room messy?   Though there is some doubt about her intentions here, I think it’s really a result of the fact that there are many more configurations of the room that are messy than non-messy.   You can put a sock in 1000 locations that are not the sock drawer, but need to spend some energy to intentionally put it in the sock drawer if that’s what you want.    Combine all the objects in the room, and it seems there are uncountably more ways for the room to be messy than clean.    Thus, without intentional action to drive it towards one of these clean configurations, small continuous changes will probabilistically lead to complete messiness.   So she doesn’t need to be trying, the messy room is just something that will happen with high probability unless someone invests energy to prevent it.   This is similar to the basic principles that the thermodynamic laws of entropy are built upon, though I won’t say much more about that right now, due to the large number of websites that seem to admonish us against the messy-room metaphor for this concept.   

So, in short, when some event we want has a low probability of occurring,  it is usually just a measure of the fact that there are many possibilities of what can occur, and only a small number have property that is significant to our human interpretations.    The universe doesn’t know which one we want, so it has no particular reason to deliver the desired outcome.   Imagining a technical device that can alter the laws of probability is like imagining a device that can make 2+2=5, or can cause triangles in a Euclidean plane to have angles totaling 190 degrees:   it simply violates the fundamental mathematics of the situation.     Over the next few millennia, humanity may see miraculous inventions such as laser pistols, teleportation, starships, or halfway decent William Shatner albums, but I think we can safely bet that no machine will ever alter the laws of probability.    If you’re frustrated sometimes by things not going your way, you should take comfort in the fact that there are many ways things can go, and figure out what you can do to reduce the number of possible bad outcomes.   The universe is not engaged in some kind of conspiracy against you that needs to be fixed with a magical gadget.

And this has been your math mutation for today.


References:




Sunday, November 29, 2015

214: In Search Of The Ultimate Math Game

Audio Link


With the holiday season upon us, many of you out there are probably giving or getting new tech gadgets as gifts.    Once you unwrap your fancy new iPad, iPhone, or Android tablet, you’re probably asking yourself, “Now what do I do with this?”    While you will probably be downloading lots of fun games and apps, you will somehow need to justify all the hours you spend in front of the screen to your family.    One of the best ways to do this is to install a few math-related games, and provide some educational value for your children.   But there is a bewildering array of supposedly educational games available for these systems.   How do you know which ones to get?     Today I will share some suggestions based on my experiences.

The first thing I should point out is that there are hundreds of games out there that are basically glamorized flashcards, presenting math problems directly and giving some kind of in-game reward for correct solutions.    For example, they will put up a math problem, like “What is 5 x 5?”, and if the answer is correct, the player gets a few points.   These points can then be traded in for virtual stickers, virtual ammunition against alien robots, or similar rewards.   While there is nothing wrong with this type of game, and they have the advantage of being able to easily draw on large libraries of problems for different skill levels, I don’t find them very exciting.    My daughter will play them if I tell her she needs to practice her math, but doesn’t usually come to me asking to play them.   What I really want are original games that both teach math and can stand on their own as fun games.   Fortunately, I have found two games that fit these requirements.

The first game I want to highlight is called “DragonBox Elements”.    This game is designed to teach the basics of geometric proofs, a seemingly advanced topic, but they present it in a very accessible and intuitive way.    Each basic shape, triangles and quadrilaterals, can summon a basic type of monster related to that shape.    So if you can identify a quadrilateral among the shapes on the screen, you trace it out and summon a quadrilateral-monster.   Line segments and angles are also marked with colors, such that any two objects with the same color have equal length, and you can upgrade the monsters to “special” ones using these.   So, for example, if you notice a triangle-monster has two equal sides, you can click on them to upgrade to the slightly more powerful isoceles-monster.   The monsters also have powers, which essentially invert this process:  so if you have been given an isosceles-monster and its two equal sides are not yet colored, you can click on the monster and the two sides to mark them as equal.   They also introduce other powers related to ideas like opposite angles, radii of circles, and parallel lines.   So the basic Euclidean concepts of definitions, axioms, and theorems have been transformed into monsters and powers.    I’m not totally sure how this will translate to actual proof skills when my daughter reaches that level of math class, but laying the foundations at such a young age can’t hurt.   And more importantly, she loves this game, even asking to replay all the levels at “hard” difficulty after beating it once.

The second truly engaging iPad math game I have discovered is called “Calculords”.   This is a card game, where each turn you have a bunch of cards in hand that you can use to summon creatures for battle.   There are two types of cards, number cards and creature cards.   It’s not a simple energy system like in most popular collectible card games though:   in order to summon a creature for battle, you need to add, subtract, and multiply number cards to reach the creature’s number.   The creatures are then placed on a lane-based battlefield, where they fight the evil monsters summoned by an alien enemy.    For example, suppose you have a Hungry Blob card, a monster with a summoning cost of 15, and your number cards are 3, 3, 4, and 1.   You can form a 15 using 3 x 4 + 3, so you can play those cards to summon your blob.   But an additional wrinkle, adding to the mathematical challenge, is that you also gain extra bonuses if you precisely use up all your number or creature cards.   So a better move would be to play 3 x 4 x 1 + 3, which still reaches your 15, but uses up your numbers.    Since you have 9 creature cards and 9 number cards on each turn, the number of potential choices and calculations is quite large, and the strategy to summon the best set of monsters while trying to use up cards to get the bonus can get very involved.    But the game offers many enemies at a variety of difficulty levels;  my daughter has been playing at the easier levels since she was in 2nd grade.   This is another game that she and I have found quite addictive, and an amazing way to get her to eagerly practice her basic arithmetic.   And at the top difficulty levels, even I find it challenging, when I sneak in a chance to play on my own.

So, in short, these are the two truly original smartphone/tablet math games I currently recommend for elementary-age students:   DragonBox Elements and Calculords.   Naturally, these are heavily influenced by my 4th-grade daughter’s tastes, and their effectiveness probably varies a lot at older and younger ages.   DragonBox elements provides the amusing and engaging transformation of Euclidean definitions, axioms, and theorems into monsters and powers.   And Calculords provides a strategic challenge involving arithmetic calculations that is accessible to young children at lower levels, and fun even for adult math geeks at the hardest settings.   If you have kids at the upper elementary level who could use some extra math practice, be sure to take a look at these excellent games.   Also be sure to post reviews on iTunes or similar sites if you like them, as this will increase the chance of further games appearing from these talented authors..   And as always, I’ll be interested to hear from you on this topic:  with such an overwhelming number of smartphone and tablet games out there, I’m sure there are a few great ones that I haven’t discovered yet.   

And this has been your math mutation for today.



References:  





Sunday, October 25, 2015

213: Proof of the Fourth Dimension

Audio Link

Rudolf Steiner was a prolific Austrian author and philosopher of the late 19th and early 20th centuries.    He felt a strong connection to mysticism and spiritualism, ever since he supposedly communicated with the ghost of a recently deceased aunt at the age of 9.   Steiner is well-known for having led a group that split off from the popular circle of European mystics known as the Theosophical Society, which seemed heavily inclined to regard the religions of East Asia as somehow providing the keys to understanding spirituality.   Steiner called his new group the Anthroposophical Society, and this competing group believed that Western science and culture were just as strongly connected to the spiritual-- it was just a matter of intepreting them properly.    One particular Western idea that Steiner was fond of was the concept of a fourth physical dimension, another mathematically-defined direction that we cannot percieve but is just as real as length, width, and height.     Steiner believed that our consciousness extended into this fourth dimension, and that phenomena like ghosts and ESP resulted from activity in this hidden dimension.      And most interestingly, he believed he had a simple philosophical proof that this fourth dimension really does exist, and our human minds really do extend into this additional dimension.

Here's how Steiner's proof goes.   We all know that a creature of a particular dimension, if it looks out at its world, really only sees a view that is one dimension smaller.   For example, a one-dimensional creature living in Lineland, a universe that exists entirely on a single straight line, can only perceive a single point on either side of himself:   a zero-dimensional view.    Similarly, a two-dimensional Flatlander, living on a plane, really only sees a line;  it is only us three-dimensional creatures, looking down on the plane from above, who can truly comprehend its full two-dimensional world.    And in real life, when we look out with our eyes, we are only seeing a plane.   Yet somehow we do believe we fully understand and perceive the three dimensions of our world.   Steiner draws what he believes is a natural conclusion from this:   "The fact that we can delineate external beings in three dimensions and manipulate three-dimensional spaces means that we ourselves must be four-dimensional...  We float in a sea of the fourth dimension just like ice cubes on water."   In other words, our ability to fully perceive our three-dimensional space shows that our minds must extend beyond those three dimensions.  

It's a fun thought, but you can see something fishy there right away, if you think about the world of modern computing.    I can think of all sorts of situations in which an object in three dimensions is represented by a model in fewer dimensions.     For example, most computer memories and circuits that power modern three-dimensional computer games are essentially stored in flat two-dimensional circuit boards.   While these are technically 3-D like all physical objects, the memory storage can be thought of as truly two-dimensional in some sense, as each (x,y) coordinate on the circuit board only stores one encoded value at any given time.    More basically, you may recall the concept of a Turing Machine discussed in some earlier podcasts:  this is a theoretical model of computing, based on writing and reading values from a long, essentially one-dimensional, tape.   It has been shown that any modern computer can be modelled by a very slow, but 100% accurate, Turing machine equivalent.    So even the 3-D models in a modern computer game could, with enough work, be represented in one dimension.

I think the main flaw in Steiner's argument is his fundamental premise, that a creature of n dimensions can only perceive n-1 dimensions.   It is true that through the sense of sight, a creature can only see one dimension lower, but our senses are not limited to sight.   Think about a blind man, who perceives the world mainly by walking around and tapping items with his cane to understand their form:  he can walk forward, back, right, or left, and even climb ladders up and down.    He is truly perceiving the full three dimensions of his world, travelling within all three of those dimensions and building a mental model based on his real experiences.    This applies to the lower-dimensional examples as well:   the flatlander can move around and perceive his full plane, and even the poor Linelander can move back and forth on his line.    Thus, the idea that perceiving your full dimensionality requires capabilities from a greater dimensionality does not really seem to ring true.    You need to think of perception much more generally than simple line-of-sight.

Naturally, this does not fundamentally prove that Steiner was wrong about our minds extending into the fourth dimension; it just means that the proof of such an idea is not so simple.   So it's still entirely possible that the concept of our mystical four-dimensional minds is correct but unproven, and the rest of Steiner's Anthroposophical Society ideas might still be valid.    This philosophy of the fourth dimension was just a launching point for a variety of mystic concepts, related to traveling along this fourth dimension to the astral plane where you could encounter ghosts, life after death, etc.   Some of Steiner's lectures get amusingly specific on details of the astral plane-- apparently he believed that his meditation and similar activities had actually taken him to this place, so he could talk about how astral dimensions mirrored our own, and writing there would appear backwards.   Personally, I'm a bit of a skeptic on this topic, but these kinds of ideas do seem to have a lasting appeal, as shown by the New Age sections you can find in many modern bookstores.   If you're into that stuff, try meditating hard enough, and maybe you too can follow Steiner's path into the astral plane through the fourth dimension.   While you're there. see if you can track down Steiner's spirit, to discuss the flaws in his philosophical proofs.

And this has been your math mutation for today.



References:

Sunday, September 27, 2015

212: De-Abstracting Your Life

Audio Link

One of the core principles of mathematics is the idea of abstraction, generalizing from various experiences to describe simplified models that enable rigorous reasoning.   For example, if you look at a street map of your city, nothing there qualifies as a pure Euclidean triangle:  all roads have thickness, varying slopes, squished raccoons, etc.     But by reasoning about ideal triangles and lines, we can make powerful deductions about the distances between points that are very useful and accurate for practical purposes.   However, there is a dark side to abstraction-- when used too much in your daily life, it can cause you to over-generalize and lead to issues like stereotyping and prejudice.  

For example, 20 years ago I had a Scottish roommate named Lloyd.    Lloyd was a great guy, but I could not understand a word he said, due to his outrageous Scottish accent.   Eventually we started keeping a notepad in the room so he could write down anything important he needed to communicate.   After a few months with him, I was on the verge of insanity.    Now, whenever I'm being introduced to someone from Scotland, I inwardly cringe, bracing myself for a similar experience.  In effect, I have abstracted Lloyd as the general Scotsman in my mind, impacting my further relationships and experiences with his countrymen.   It hasn't been that much of an impact in my life, as most residents of Scotland have yet to discover the joys of Hillsboro, Oregon, but it's still a bad habit.    Is there something simple I can do to try to cure myself of this way of thinking?     One intriguing set of ideas comes from a 20th-century pop philosophy movement known as General Semantics.

General Semantics was first created by Polish count Alfred Korzybski in the 1930s, and  detailed in a book called "Science and Sanity".    This book describes a wide-ranging philosophy based on evaluating our total "semantic response" to reality, and learning to separate true reality, our observations of reality, and our language that describes the reality.    By becoming conscious of our tendency to over-abstract, we can improve our own level of sanity, hence the book title "Science and Sanity".    While serious philosophers and linguists generally don't consider Korzybski's ideas very deep, he attracted a devoted cult following, who believe that the General Semantics tools can significantly improve people's lives by reducing the errors that result from over-abstraction.   This movement also led to the proposal for "E Prime", the variant English language without the verb "to be", which I described back in podcast 196.    Amusingly, Korzybski was also a bit of a math geek:  when his Institute for General Semantics in Chicago was assigned the address 1232 East 56th Street, he had the address changed to 1234, in order to create a nice numerical progression.

Among the key tools that General Semantics provides for fixing over-abstractions are the "extensional devices", new ways to think about the world that help you to correct your natural tendencies.   Many of these involve attaching numbers to words.   The most basic is "indexing", mentally assigning numbers to help emphasize the differences between similar objects.    For example, I might think of my friend Lloyd as Scotsman-1.   Then, if introduced to another person from Scotland, I can think of him as Scotsman-2, emphasizing that he is a completely different person from Scotsman-1 despite their common origin.   If I go out with my new friend for a yummy Haggis dinner, I would think of the waiter as Scotsman-3, again recognizing his essential uniqueness and separating him from the other two.   Through this assignment of numbers, I can avoid grouping them all into the single abstraction of Scotsmen, and help force myself to treat them as individuals.

Another important extensional device is called "Dating", similar to indexing but based on time.    With this device, you attach dates to objects, indicating when you observed or experienced them.   The Lloyd I remember should really be thought of as Lloyd-1993, since that's when I knew him, and I'm really only familiar with his characteristics at that time.   If he emails me that he's coming to town, I should now think of him as Lloyd-2015, who may be a different person in many ways.   Perhaps he has been working on his accent a bit, or maybe due to my 20+ years of engineering experience, my ears have gotten better at discerning words in unusual accents.    I should not over-abstract and assume that his most notable characteristics at one time, and my perception of them, will be the same today as in the past.    Like everything in the universe, he and I are constantly changing, and I can use this extensional device to remind myself of that.

There are a number of additional extensional devices in General Semantics, such as the use of Et Cetera, quotes, and hyphens to further qualify your abstracted language.    These seem a bit more awkward to me, though some may prefer them.     Overall, I think the general concepts behind Korzybski's extensional devices probably can serve as a useful tool, especially if I go to Scotland sometime, though perhaps they are not quite as profound as General Semantics fanatics like to think.    Korzybski's movement still seems to be going strong, with active institutes in New York, Australia, and Europe that have a presence on the web and in social media, and a quarterly newsletter still in print since 1943.     Naturally, I've grossly oversimplified many of the core ideas for this short podcast, but if this has served to whet your appetite, you can find many other details at the links in the show notes. 

 And this has been your math mutation for today.









References:


Sunday, August 30, 2015

211: Saving A Few Million Years

Audio Link

Those of you who follow the Math Mutation facebook feed may have noticed that a book I co-authored was just released: "Formal Verification: An Essential Toolkit for Modern VLSI Design". Now, I need to caution you that this is not a Math Mutation book-- it's a technical book, aimed at electrical and computer engineers invovled in chip design. However, I do think Math Mutation listeners might have some interest in the core concepts on which the book is based. So, today I'll try to give you a brief summary of what Formal Verification is, and why it's worth writing a book about.

You're probably aware that modern computer chips are pretty complicated, by many measures the most complex devices ever created by man. For new ones coming out this year, the number of transistors is measured in the billions. So it makes sense to ask the question: how do we know these things will work? It would be prohibitively expensive to just build them first and then test them, so we need to discover and fix as many of the bugs as possible during the design stage. The process of finding these bugs is known as design validation. For many years, the most popular technology used in design validation has been simulation: testing how a software model of the design will behave for various sets of inputs.

Unfortunately, even a simple chip design has so many possible behaviors that there is no way to simulate them all. For example, suppose you are designing a simple integer adder: it will take 2 numbers as inputs, each expressed with 32 bits, or binary digits, which can each be 1 or 0. It will then output their sum. How many possible input sets are there for this design? Since each input has 32 bits, it has 2^32 possible values, thus resulting in 2^64 possible values for the pair. If we assume we have a fast simulator that can check 2^20 values per second, that means that we will need 2^44 seconds to check all possible values-- over half a million years. Most managers are not very happy when given a time estimate on this order to finish a project. And needless to say, most chips sold today are many orders of magnitude more complex than a simple adder.

So, what can we do to make sure our chip designs really will work? A variety of technologies have been developed over the past few decades to try to find a good set of example values to simulate. And they do seem to be doing a decent job: most electronic devices you buy today seem to more-or-less do what you want them to. But it still seems like there should be a better way to validate them: no matter how good you make it, simulation and related methods can never cover more than a tiny portion of your design's possible behaviors.

That's where formal verification comes in. The idea of formal verification is to take a totally different approach: instead of trying specific values for your design, why not just mathematically prove that it will always be correct? That way you don't have to worry about trying every possible test case. If there is a single set of values that would generate an incorrect result, your proof will fail, and you will know your design has a bug. If you do succeed in mathematically proving your design correct, then you know that there is no bug, and do not need to waste time simulating lots of testcases. In effect, formally verifying a design is equivalent to simulating all possible values. Many would argue that philosophically, this is really the "right" way to validate chip designs. You may have heard the famous Guindon quote, "Writing is nature’s way of letting you know how sloppy your thinking is." Formal Verification pioneer Leslie Lamport expanded on this with "Math is nature's way of letting you know how sloppy your writing is.", and later added "Formal math is nature's way of letting you know how sloppy your math is."

You've probably guessed by now that there has to be a catch. Formal verification is easier defined than done: when billions of transistors are involved, how do we even get our heads around the problem of creating mathematical proofs? It's far beyond what anyone could manually do, so to make this method a possibility, humans need to be aided by intelligent software that helps to automate proofs. To further complicate matters, it's also been shown that any formal verification system needs to internally solve what are known as NP-complete problems. If you remember our discussion way back in episode 13, an NP-complete problem is "provably hard" in some sense, meaning that no piece of computer software can ever solve it efficiently in 100% of cases. However, researchers have worked for many years to try to develop practical software that could utilize clever tricks to enable real proofs on a wide variety of actual industrial product designs.

The good news is that, in the past decade, formal technology has advanced to the point where it really is practical for an average design engineer to use in many cases. While formal verification software can't handle full multi-billion-transistor chip designs, it can often enable an engineer to create solid proofs on major sub-blocks that go into a chip design, massively reducing overall risk of bugs. Using formal verification software remains a bit of an art though. Due to the NP-completeness issue, the software may get stuck or progress very slowly: the user must often give subtle hints and suggest shortcuts to enable the proofs to complete. In addition, formal verification is a problem that is impossible to fully automate: no matter how good your software gets at proving stuff, a human still has to somehow be able to tell it what stuff to prove-- what is the overall intent of the design in the first place? Ultimately, someone has to carefully transfer the design intent from their human brain into a machine-readable form, and understand the possible limitations and pitfalls in this process. Sadly, computer software that directly plugs into your brain is probably still many years away, and even then I have the feeling that many of us think too sloppily to enable this level of verification directly.

Thus, the need for a Formal Verification book. While there have been many books on Formal Verification published over the past few decades, most have focused on internal algorithms that would be needed to develop the software involved. Our book is one of the first real practical manuals designed to help deesign and validation engineers use formal verification software on real-life design targets.
Anyway, that quick summary should give you an idea of what our new book is about. If you're in a field where you do chip design or something related, please visit our book's website at http://formalverificationbook.com, order a copy, and tell all your friends about it!   If you're not in this field, the book probably won't make much sense to you, but hopefully you've still enjoyed this episode of the podcast.


And this has been your Math Mutation for today.


References:

Sunday, July 26, 2015

210: Two Plus Two Equals Five

Audio Link

Before we start, I'd like to thank listener D. Zemke, who posted another nice review on iTunes.  Thanks D!

Now, on to today's topic.   Recently I heard someone quote a clever metaphor in a casual conversation,  "Life is when nature takes 2 and 2 to make 5."   It's a nice statement of how living creatures are more than the sum of their parts.  If you took all the chemical compounds in my body and dumped them on the ground in the right proportions, all you would get is a mess.   Yet somehow I am here, and at least sentient enough to record math podcasts.    I went online to try to find the source of this quotation, and was surprised to see the number of references to this seemingly silly nonsense equation, 2+2=5.

Most of us are probably familiar with the equation from George Orwell's classic novel 1984.   As you probably recall, in the book, people are told that if the government says that 2+2=5, it is the duty of all citizens to believe it-- not just say it, but actually come to believe that it is true.   Surprisingly, Orwell did not come up with this out of thin air:  a real-life totalitarian government, the Soviet Union, actually did use 2+2=5 as part of its propaganda, in a poster with the title ""2+2=5: Arithmetic of a counter-plan plus the enthusiasm of the workers."    It wasn't quite as blatantly absurd as in 1984, but the Soviet propaganda poster used it as a metaphor:   supposedly a 5-year plan could be completed in 4 years, because the entuhsiasm of the workers provided an invisible additive factor.   Sadly, most of this "enthusiasm" was mainly due to fear of being sent to the Gulag prison camps, which resulted in many managers doctoring the statistics to match the results that the government wanted-- on paper only.   It's also reported that Nazi Herman Goering actually used this metaphor in real life, once saying "“If the F├╝hrer wants it, two and two makes five!”

The phrase 2+2=5 actually existed in the arts dating from the early 19th century.   According to Wikipedia, the phrase was first coined in a letter from Lord Byron, where he wrote ""I know that two and two make four—& should be glad to prove it too if I could—though I must say if by any sort of process I could convert 2 & 2 into five it would give me much greater pleasure."   He may have been making an indirect reference to Rene Descartes' Meditations, where the famous philosopher discussed whether equations such as 2+3=5 exist outside the human mind, and whether they can be doubted:  "And further, as I sometimes think that others are in error respecting matters of which they believe themselves to possess a perfect knowledge, how do I know that I am not also deceived each time I add together two and three, or number the sides of a square, or form some judgment still more simple, if more simple indeed can be imagined?"

Later Victor Hugo used this concept in a critique of tthe mob rule that had led to Napolean, foreshadowing Orwell's later political metaphor:  ""Now, get seven million five hundred thousand votes to declare that two and two make five, that the straight line is the longest road, that the whole is less than its part; get it declared by eight millions, by ten millions, by a hundred millions of votes, you will not have advanced a step."   Russian authors Ivan Turgenev, Leo Tolstoy, and Fyodor Dostoyevsky also made use of this metaphor.   Turgenev used it to symbolize divine intervention:  "Whatever a man prays for, he prays for a miracle. Every prayer reduces itself to this: Great God, grant that twice two be not four."    In the 20th century, there are many instances of authors following Orwell's lead and again using this metaphor for the struggle against totalitarianism, including Albert Camus and Ayn Rand.

An intriguing question is whether there are cases when it is actually valid to say that 2+2=5.   A well-known mathematicians' joke is that "2+2=5, for particularly large values of 2."   This may refer to issues with rounding:  if you start, for example, with the obviously correct equation "2.4 + 2.4 = 4.8", and ask someone to round all the numbers to the nearest integer, you do indeed derive "2+2=5" from this true equation.   It also might be a case of playing with the definitions of symbols:  perhaps you can define the symbol that we normally write as "2" to actually be an algebraic variable representing the value 2.5.   A trickier example is a "proof" that 2+2=5 that is circulating the web, where many lines of complex algebra are used.   These many lines are artificially complex in order to misdirect you from one invalid step, where a term t is replaced with the square root of t squared.   Remember that you can only do such a replacement if t is positive, a fact glossed over in the so-called proof.   I won't bore you by trying to cite all the lines of equations in an audio podcast, but you can find them linked online in the show notes if you're curious.

An amusing spoof article online points out some real-life situations where 2 and 2 might really make 5.   Ancient Incas used knotted ropes to track business transactions, and if you tie together two ropes that each have two knots, the resulting rope will have 5 knots, including the one used to tie them together.   Another example is if you put 2 male and 2 female rabbits in a cage-- pretty soon you will see numbers way larger than 5.   I'm pretty sure that most people who experience these situations in real life can make the distinction between the messiness of reality and the related arithmetic though.

But that last example brings us back around to the quote that started this whole thing.   Ironically, my web searching did not succeed in uncovering the source of the clever comparison between life and making two plus two equal five.   Most likely I didn't remember the phrasing exactly right, or else someone was just coining this on the fly and it didn't really come from a famous quote.   If you have heard it before and know its origin, please send me an email!

And this has been your math mutation for today,

References: