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
Sunday, May 12, 2013
Something that has lately amused and puzzled me
Why is it that, after The Man is received into a cloud, "behold two men stood by them in white garments"? Continuing,
"11 Who also said: Ye men of Galilee, why stand you looking up to heaven? This Jesus who is taken up from you into heaven, shall so come, as you have seen him going into heaven." Not that it is unusual for "men" to appear and disappear, in the Inspired Record of Salvation History (it might have been unusual in an absolute sense, but the Bible isn't about business-as-usual), and yet... Is it, for instance, possible that the eleven were in danger of lingering by the mount untill they sequentially keeled over for hunger and exhaustion? Why, for this very practical nudge, is it so conveniens that it be delivered by angels and not Our Lord who, really, was just right there. And what about their non-question interjection: "[he] shall so come, as you have seen him going"; is this advice to them, and how is it not the answer to their own question, "why stand you looking up to heaven"? I presume they were angels, for Peter and James and John would recognize Moses and Elijah, and Luke would have said so if it were them again.
These are some things that lately have puzzled and amused me.
Any thoughts? (please limit your comments to less than 1 megabyte in size)
"11 Who also said: Ye men of Galilee, why stand you looking up to heaven? This Jesus who is taken up from you into heaven, shall so come, as you have seen him going into heaven." Not that it is unusual for "men" to appear and disappear, in the Inspired Record of Salvation History (it might have been unusual in an absolute sense, but the Bible isn't about business-as-usual), and yet... Is it, for instance, possible that the eleven were in danger of lingering by the mount untill they sequentially keeled over for hunger and exhaustion? Why, for this very practical nudge, is it so conveniens that it be delivered by angels and not Our Lord who, really, was just right there. And what about their non-question interjection: "[he] shall so come, as you have seen him going"; is this advice to them, and how is it not the answer to their own question, "why stand you looking up to heaven"? I presume they were angels, for Peter and James and John would recognize Moses and Elijah, and Luke would have said so if it were them again.
These are some things that lately have puzzled and amused me.
Any thoughts? (please limit your comments to less than 1 megabyte in size)
Wednesday, May 8, 2013
Troubles with Scientism and Antiscientism
Oh, for the good old days that never were...
Have I ranted here before about the silly slogan "gravity is just a theory"? To sum-up (too much to explain), it revolves around (hee!) a confusion of "theory", "hypothesis", and "observation".
Today in my book of faces arises a photo impression of a "science" "quiz" titled "Dinosaurs: Genesis and the Gospel"; the keeper of the books of faces have tried to make it difficult to circulate this thing, and the circulator (not circulants) is doing her darndest to get around (are we talking in circles, yet? It's not intentional) such frustrations.
The trouble with the Scientist is that, while fighting the antiscientist, she thinks she is fighting something to do with "religion". But religio ("I bind together", man to God, men to men) has very little to do with the D:G&G "science" "quiz"; it is rather a work of superstition (on which the OED says that its etymology is confused, but may have something to do with a soldier pointlessly standing over a defeated enemy).
The particular superstition of the Book-Literal antiscientist is that God's Creation ought to fit in a book; there is a similar kind of scientistic superstition as well that the Universe ought to fit within Creation, but... why, under Heaven, anyone would take the name of Christ and insist that God made Creation a small thing, a humanly brief and fleeting thing... as though He wouldn't be large enough anymore if the Past and Future didn't fit within human history... For instance, it is abundantly clear that the people we hear about who breathe the air and speak and sing to the Lord a new song do not flee, as it were a shadow, neither is alles Fleisch es ist wie Gras, und alle Herlichkeit des Menschen wie des Græses Blumen — das Gras ist verdorret, und die Blume abgefallen. We are (in a litteral sense) rather more long-enduring than grass and flowers, if not more permanent in body. But that's not the point of the Book!
How often have I lamented (in other words) that the difficulty in talking with the world is that the world has forgotten how to talk? And there's something about that in The Last Battle...
Anyways, this is, I suppose, one of those letters-to-nobody... I wonder who will open it?
a Christopher
Have I ranted here before about the silly slogan "gravity is just a theory"? To sum-up (too much to explain), it revolves around (hee!) a confusion of "theory", "hypothesis", and "observation".
Today in my book of faces arises a photo impression of a "science" "quiz" titled "Dinosaurs: Genesis and the Gospel"; the keeper of the books of faces have tried to make it difficult to circulate this thing, and the circulator (not circulants) is doing her darndest to get around (are we talking in circles, yet? It's not intentional) such frustrations.
The trouble with the Scientist is that, while fighting the antiscientist, she thinks she is fighting something to do with "religion". But religio ("I bind together", man to God, men to men) has very little to do with the D:G&G "science" "quiz"; it is rather a work of superstition (on which the OED says that its etymology is confused, but may have something to do with a soldier pointlessly standing over a defeated enemy).
The particular superstition of the Book-Literal antiscientist is that God's Creation ought to fit in a book; there is a similar kind of scientistic superstition as well that the Universe ought to fit within Creation, but... why, under Heaven, anyone would take the name of Christ and insist that God made Creation a small thing, a humanly brief and fleeting thing... as though He wouldn't be large enough anymore if the Past and Future didn't fit within human history... For instance, it is abundantly clear that the people we hear about who breathe the air and speak and sing to the Lord a new song do not flee, as it were a shadow, neither is alles Fleisch es ist wie Gras, und alle Herlichkeit des Menschen wie des Græses Blumen — das Gras ist verdorret, und die Blume abgefallen. We are (in a litteral sense) rather more long-enduring than grass and flowers, if not more permanent in body. But that's not the point of the Book!
How often have I lamented (in other words) that the difficulty in talking with the world is that the world has forgotten how to talk? And there's something about that in The Last Battle...
Anyways, this is, I suppose, one of those letters-to-nobody... I wonder who will open it?
a Christopher
Thursday, May 2, 2013
Brief and Minimally Considered
- I have this hour run across MyJetpack
- There are many ways to work stale bread into sweet pudding. At least two involve eggs.
- The american robin, it seems, is a relative of the thrush. I haven't seen them eating snails; but then it's been a while since I saw wild snails. Perhaps in later in the season.
- Have you before considered use of "the" to treat as gramatically definite a fictitious generic creature, as in "The american robin..."? These things amuse me!
- I'm starting actually to get tired of this friendly web-logging thing; the gimmick isn't holding up and very few people ever say hello; and that's OK. At the tmbl (which I'm using in a most-untmbly fashion, it seems) there is still the fresh focus of my academic speciality, which might keep me going there longer in spite of even fewer people saying hello, but this... One of my early inspirations-unto-blogging did recommend it as a way to make acquaintances, but I've made more from reading than from writing, and that one also doesn't 'blogg any more that I know of. And that's OK, too...
- TeX-setting diagrams is tricky, but you can do it incrementally. One day MathJax will pick up XYJax and then we'll all be that much more impressed with everything.
- Six is enough, I think. Don't you?
Subscribe to:
Posts (Atom)
