December 4th, 2003

beartato phd

(no subject)

From http://homepage.mac.com/jhjenkins/Deseret/Deseret.html:
The original design of Unicode allowed the inclusion of some 65,534 characters, with some six thousand of those "private use characters" which basically anybody can use any way they like. When it became clear that this simply wasn't enough to accomodate all the large, rare character sets such as Egyptian hieroglyphics, and uncommon Han ideographs, an extension mechanism (surrogates) was added to the standard which allow the addition of another million characters.

The problem was, a vicious circle quickly arose. Nobody started to implement surrogates because there were no characters encoded using them, and nobody wanted their characters to be encoded using surrogates because nobody was implementing them.

To break the vicious circle, we needed a writing system which was at once real and at the same time so incredibly rare and/or dead that nobody would object to its being encoded with surrogates. I volunteered the Deseret Alphabet as such as script, and it was quickly accepted. Since then, Shavian, the Cypriot syllabary, Linear B, Gothic, and Etruscan have all been formally approved for addition to Unicode using surrogates and dozens of other scripts have been earmarked for encoding that way. The Deseret Alphabet has also been approved by WG2, the ISO standards body which works with Unicode on the continued development of Unicode's ISO counterpart, ISO/IEC 10646.


The original proposal:
http://www.unicode.org/pending/deseret/Proposal.html
More samples:
http://www.utlm.org/onlineresources/deseretalphabet.htm
beartato phd

(no subject)

Blerg. Slept in until like 11:40 this morning. Feel like crap. Though Tom7 has a talk soon on the modal logic stuff he's been hacking on, so that should be cool.
beartato phd

(no subject)

Random thoughts on modal logic floating through my head while listening to tom's talk, condensed into near-incomprehensibility because I just need to write them down before I forget:

* So the endofunctoriality of modalities is totally standard (to put it another way, it's obvious that their kind is type -> type) but after seeing so many instances of Gamma |- M : A@w in tom's presentation, I start to wonder if all the "@w"s are just funny backwards notation for what is morally an endofunctor application. That is, are modal worlds themselves just a funny sort of type operator?

Wait, no, now that I think about it, you don't get <>A -> <>B from A -> B, so maybe they're not really functors, just type operators. Then again, (A -> B)@w is the same as A@w -> B@w, so maybe that works still.

* This is sort of suggested by ultrafinitism: what sort of axiomitzation would correspond to posssible-world models with an accessibility function (taking values in some ring, somehow compatible via a triangle-like inequality with transitivity of accessibility) in place of an accessibility relation? The analogy to ultrafinitism is "I believe in proofs at most k symbols long" compared to "My imagination is powerful enough to imagine a possible world k different than my current world", or, in tom's case, putting some sort of resource bound on how much time mobile code could take, i.e. "this host is distance/latency k from this other host on the network".

* Found a link crediting a guy named Lewis for inventing the concept of modal logic in 1918. I'm bothered that I've never heard of him before. Always thought Kripke was the one big name.