I'm in a mood. So... I dunno, ... pray for me?
If he that breaks a thing to find out what it is has left the path of wisdom, what shall we say of him who breaks a thing because he has forgotten what it was?
JRRT fan
Saturday, June 29, 2013
Wednesday, June 26, 2013
There is no joy in Mudville
My dear neighbours,
As much as I am annoyed by the erroneous majorities delivered today, I am even more saddened to think of whatever ways the Superior Court of my own native Crown Realm, and its Prime Ministers and parliamentarians, have served poor example and made the day's transpirations at all easier.
frater tuus in fide
As much as I am annoyed by the erroneous majorities delivered today, I am even more saddened to think of whatever ways the Superior Court of my own native Crown Realm, and its Prime Ministers and parliamentarians, have served poor example and made the day's transpirations at all easier.
frater tuus in fide
Tuesday, June 25, 2013
Homotopy Type Theory
Out in the strange world beyond the pseudonyms (or, actually, the realm of different pseudonyms, used by other people) there is noise surrounding a new book, a collaborative work, titled Homotopy Type Theory, to which I can (quite unreliably and unverifiably) claim to have made at least a moral contribution (and one blog post contribution --- no, I'm not telling you here!). And I don't at all mind that my name appears nowhere in the text, because really this sort of thing is more about the fun than the credit (also, two or four dozen other people made much-more substantial-and-original contributions anyway).
The text is subtitled “Univalent Foundations of Mathematics”, which is really a much more interesting notion than “homotopy type theory” as such, and it is about this Univalence that I'd like to sing for just a little while.
Now, for a long time, mathematicians of a certain kind have been competing with eachother to compose a sort of abstract semantics which might conceivably give an underlying meaning to all the abstract nonsense ordinary mathematicians do for a living. This might sound like a funny thing to worry about, but it's had immensely practical results in the realm of computer science and such, whether the dear fellows and dames intended it or not. It also might sound like chasing one's tail (indeed this is a danger that competitors of the sport learn early on to avoid), which is probably why Foundations is so emphasized in the name of the specialization.
Anyways, lots of people have composed such schemes of abstract semantics, and so modern mathematicians have lots of variety to choose from whenever they worry about if they're spouting absolute nonsense or merely incomprensible sense; and these do have some interesting distinctions among them — the best foundations are perfectly able to talk about all of the other foundations, and find some interesting things the other foundations say, and explain why they are all wrong. This is part of the sport, you see. Great fun! What settles a mathematician on one foundation or another (some never do settle!) involves a combination of aesthetics, pragmatics, and intuition.
Homotopy Type Theory is, roughly, a language for discussing (and perhaps describing) objects made of stuffs that are put together, somehow. This sounds vague, I know; but it isn't that the words “objects”, “stuffs” or “put together” are intrinsically vague, it's that the rules for using them haven't been made explicit here. They aren't the usual words (except “objects” might be!) but that's immaterial. But there are words, and rules, and the rules let you do enough that one can call the result a language, and even think it versatile; and that's half of what one has come to expect of a foundation these days. The other third and the final quarter are, respectively, some assumptions about what you can assert without comment, and how you decide what follows from which assumptions. (If you're worried that ½ + ⅓ + ¼ is ¹³⁄₁₂, you're paying too much attention).
The Univalence Hypothesis belongs to the third part, assumptions to be quoted without comment, and specifically makes assumptions about some particular objects one can mention, and specific details about how they are put together. In just a little more specificity, it supposes there to be a family of particular objects, called $\mathrm{Type}_j$, that the stuffs each $\mathrm{Type}_j$ are made of are themselves objects, and that every object is party to most of them, and (most importantly) each $\mathrm{Type}_j$ is put together in such a way that equivalence of objects-as-stuffs-put-together is equivalent to objects as parts of $\mathrm{Type}_j$.
That's still vague, because I still haven't written here what the things mean, nor do I intend to, but an illustration might help.
Suppose a pair of twins shared a pair of identical bicycles. Now, the twins know eachother apart from themselves, and the bicycles certainly aren't in the same place, but in our imagination “identical bicycles” really does mean the twins can't distinguish the bicycles by sight, and because they're good detached Catholics they also have no inclination to fight over who is on which bike, and so There Are Two Ways for twins to mount and ride their bikes. The left-hand supposition of Univalence (and our experience in the world of the senses!) is that there is a path, or choreography between these two configurations: twin first-to-breathe and twin first-to-say-“ma!” (if this lists them all two) can dismount and walk around and effectively trade places. The right-hand supposition of Univalence is that there is, effectively, exactly one way to do this and one way to not; and this is where Univalence and the world of sense part ways, because there is no way to exhibit such a simple figure in our paltry three-space-less-one-time dimensions. But the key idea — having exactly one way to switch and one way to not-switch — generalizes in a beautiful and poetic way, and leads to all sorts of other beautiful and poetic equivalences, to say nothing of many subtler rhymes it gives rise to. For instance (one of my favourites!), there is a circle of ways to be the order of the integers. This notion of equivalence, identified with “identifiability”, is the key novelty proposed in Univalent Foundations, is the organizing principle of the book, and makes for some fun thought exercises too.
There's lots lots more (of course! we'll never be finished) and this wasn't ever meant to be a math 'blog, however fun maths is; so I'll leave off there, and if you want to go read more about it elsewhere, perhaps we'll meet again by other names and in other guise.
à bien-tôt!
The text is subtitled “Univalent Foundations of Mathematics”, which is really a much more interesting notion than “homotopy type theory” as such, and it is about this Univalence that I'd like to sing for just a little while.
Now, for a long time, mathematicians of a certain kind have been competing with eachother to compose a sort of abstract semantics which might conceivably give an underlying meaning to all the abstract nonsense ordinary mathematicians do for a living. This might sound like a funny thing to worry about, but it's had immensely practical results in the realm of computer science and such, whether the dear fellows and dames intended it or not. It also might sound like chasing one's tail (indeed this is a danger that competitors of the sport learn early on to avoid), which is probably why Foundations is so emphasized in the name of the specialization.
Anyways, lots of people have composed such schemes of abstract semantics, and so modern mathematicians have lots of variety to choose from whenever they worry about if they're spouting absolute nonsense or merely incomprensible sense; and these do have some interesting distinctions among them — the best foundations are perfectly able to talk about all of the other foundations, and find some interesting things the other foundations say, and explain why they are all wrong. This is part of the sport, you see. Great fun! What settles a mathematician on one foundation or another (some never do settle!) involves a combination of aesthetics, pragmatics, and intuition.
Homotopy Type Theory is, roughly, a language for discussing (and perhaps describing) objects made of stuffs that are put together, somehow. This sounds vague, I know; but it isn't that the words “objects”, “stuffs” or “put together” are intrinsically vague, it's that the rules for using them haven't been made explicit here. They aren't the usual words (except “objects” might be!) but that's immaterial. But there are words, and rules, and the rules let you do enough that one can call the result a language, and even think it versatile; and that's half of what one has come to expect of a foundation these days. The other third and the final quarter are, respectively, some assumptions about what you can assert without comment, and how you decide what follows from which assumptions. (If you're worried that ½ + ⅓ + ¼ is ¹³⁄₁₂, you're paying too much attention).
The Univalence Hypothesis belongs to the third part, assumptions to be quoted without comment, and specifically makes assumptions about some particular objects one can mention, and specific details about how they are put together. In just a little more specificity, it supposes there to be a family of particular objects, called $\mathrm{Type}_j$, that the stuffs each $\mathrm{Type}_j$ are made of are themselves objects, and that every object is party to most of them, and (most importantly) each $\mathrm{Type}_j$ is put together in such a way that equivalence of objects-as-stuffs-put-together is equivalent to objects as parts of $\mathrm{Type}_j$.
That's still vague, because I still haven't written here what the things mean, nor do I intend to, but an illustration might help.
Suppose a pair of twins shared a pair of identical bicycles. Now, the twins know eachother apart from themselves, and the bicycles certainly aren't in the same place, but in our imagination “identical bicycles” really does mean the twins can't distinguish the bicycles by sight, and because they're good detached Catholics they also have no inclination to fight over who is on which bike, and so There Are Two Ways for twins to mount and ride their bikes. The left-hand supposition of Univalence (and our experience in the world of the senses!) is that there is a path, or choreography between these two configurations: twin first-to-breathe and twin first-to-say-“ma!” (if this lists them all two) can dismount and walk around and effectively trade places. The right-hand supposition of Univalence is that there is, effectively, exactly one way to do this and one way to not; and this is where Univalence and the world of sense part ways, because there is no way to exhibit such a simple figure in our paltry three-space-less-one-time dimensions. But the key idea — having exactly one way to switch and one way to not-switch — generalizes in a beautiful and poetic way, and leads to all sorts of other beautiful and poetic equivalences, to say nothing of many subtler rhymes it gives rise to. For instance (one of my favourites!), there is a circle of ways to be the order of the integers. This notion of equivalence, identified with “identifiability”, is the key novelty proposed in Univalent Foundations, is the organizing principle of the book, and makes for some fun thought exercises too.
There's lots lots more (of course! we'll never be finished) and this wasn't ever meant to be a math 'blog, however fun maths is; so I'll leave off there, and if you want to go read more about it elsewhere, perhaps we'll meet again by other names and in other guise.
à bien-tôt!
Tuesday, June 11, 2013
To The Editor, or Worth doing? Then, even badly...
Dear Sir,
Oh, how the spheres do buzz some time; this cannot have been what Pythagoras had in mind...
Disclosures perhaps relevant to your weighing of what follows: I, a gent in hope if not indeed, have sometimes been described as "dapper", yet I own but two pairs of trousers and just enough of the other things to get through a week between launderings.
On the subject of appropriate garb: it is my considered opinion that civilized folk should wear clothes. That is, they should be clad. Beyond that, being dressed is all well and good in moderation and if suited to the job in hand. Being merely ornamented or sculpted are not at all the thing, should you be not actually made of maple or marble. Let's just leave the subject of swimming well alone.
a poor maths student
Oh, how the spheres do buzz some time; this cannot have been what Pythagoras had in mind...
Disclosures perhaps relevant to your weighing of what follows: I, a gent in hope if not indeed, have sometimes been described as "dapper", yet I own but two pairs of trousers and just enough of the other things to get through a week between launderings.
On the subject of appropriate garb: it is my considered opinion that civilized folk should wear clothes. That is, they should be clad. Beyond that, being dressed is all well and good in moderation and if suited to the job in hand. Being merely ornamented or sculpted are not at all the thing, should you be not actually made of maple or marble. Let's just leave the subject of swimming well alone.
a poor maths student
Subscribe to:
Posts (Atom)
