Home
Fly, fly, balloon man. Savor the Void! [entries|archive|friends|userinfo]
Jason

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

(no subject) [Jul. 10th, 2009|09:34 pm]
[Tags|]

What do you get if you combine super lo-fi 32kbps mp3 encoding, SWFTOOLS, and crumbly sleep-deprived left-over bits of sanity?

Flash dancing blob!

Perhaps my greatest accomplishment in the field of pointless animated musical proof-of-concept demos since my 6502 threading library MUSTARD.NES.

The concept this is proving is not very special in this case, just that command-line swf tools (called "SWFTOOLS") actually work as advertised. In some cases, even better than advertised since the docs imply that png and mp3 support has not yet been implemented, but the implementation says otherwise.
Link4 comments|Leave a comment

(no subject) [Jul. 10th, 2009|07:47 pm]
[Tags|, , ]

If you think my thesis has too many maths and not enough pretty pictures, you should read Raph Levien's PhD thesis. It is about the Spiro font tool/library he made, which I'm kind of suprised I haven't heard about before. This YouTube video explains better than words can. It was about 1:40 in where I started going "ooohhhhh I see why this is useful".
Link2 comments|Leave a comment

(no subject) [Jul. 8th, 2009|11:59 pm]
[Tags|]

Term of art: Dragon Marriage Condition
Link6 comments|Leave a comment

(no subject) [Jul. 3rd, 2009|07:16 pm]
[Tags|]

I had a bit of an epiphany right now that I actually don't dislike writing at all.

I dislike having to turn in bad writing, and this is sometimes the outcome when I write to deadlines.

Pieces of chapter 4 make me just wanna puke. If I was given a billion years to keep rehashing how to present the ideas in my thesis until they were actually well-presented, then that would be great. Instead, I am a day or two overdue, holding onto a morass of conflicting notations and lemmas that just aren't pretty enough. That is negative one frillionth of how much time I would like to have. This is regrettable.
Link5 comments|Leave a comment

(no subject) [Jul. 1st, 2009|07:57 pm]
[Tags|, , ]

Ending month of lj radio silence.

However, thesis not quite done yet. This is not so good. On the plus side, it is getting there --- I have perhaps 30 pages left to write/edit, I think, before it is sort of turnable-innable. On the even more plus side, I got a postdoc offer from Penn that looks rather appealing. Still gonna wait and see what CI Fellows says on the 10th.

Glum Buster is a very pretty game which I would like to play when I get more time.
Link3 comments|Leave a comment

(no subject) [Jun. 1st, 2009|10:31 am]
[Tags|]

Ok, everybody, I think it is seriously time for me to drop off the face of the earth and put a final push into this dissertation thing. See you in approximately July. Please do not be offended when I do not return your calls, literally or figuratively.
Link14 comments|Leave a comment

(no subject) [May. 30th, 2009|07:44 pm]
[Tags|]

Another day, another HLF example typed in and checked. This one did trigger a minor bug in coverage checking, (the monotonicity check was absurdly too-conservative in the case of a type family not declared with @type) which was easy to fix.
LinkLeave a comment

(no subject) [May. 30th, 2009|11:31 am]
[Tags|, , ]

When I awoke from troubled dreams this morning I found myself thinking about the discrete fourier transform. If you take a signal, and phase-shift each frequency component by some phase proportional to the square of its frequency, shouldn't that give you a kind of Laplace operator? The reasoning being that this is like saying that energy is proportional to the square of momentum, so the the time derivative of the result should look like the square of the momentum operator, hence a second spatial derivative. But if I do this with discrete time and space, it's not really a derivative, just some funny analogue of it.

In mathematica I can do
Delta[x_, y_] = If[x == y, 1, 0]; M = 100; K = 100;
H[s_] = s^2/(2 M K);
f[x_] = (1/(2 M)) Sum[
    Exp[2 I Pi (x s - H[s])/(2 M)], {s, -M, M - 1}];
rt = Table[{x, K*K*(Re[f[x]] - Delta[x, 0])}, {x, -20, 20}];
st = Table[{x, Re[f[x]] }, {x, -20, 20}];
it = Table[{x, K *Im[f[x]]}, {x, -20, 20}]; ListPlot[{st , it, rt }, 
 Joined -> True, Filling -> Axis, PlotRange -> (1 {-0.6, 1})]

and it yields this graph

which seems to be convergent as I increase M, the number of points in the world, and K, a scaling factor that when bigger makes every momentum count as less energetic. Maybe it is effectively acting like hbar (or its reciprocal) or something? I dunno.

Doing some numerical fiddling, it seems the spikes in the imaginary part (the red graph) just one step away from the origin on either side have the value of exactly 1/π --- not sure what causes that.
LinkLeave a comment

(no subject) [May. 29th, 2009|11:59 pm]
[Tags|]

Got a bunch more hlf-examples hacking done today: identity theorem for linear logic and a liveness theorem for a simple petri net.
LinkLeave a comment

(no subject) [May. 28th, 2009|10:09 am]
[Tags|]

Hello, I am a frequent victim of Bipolar Research Disorder, where my emotional state is subject to the whims of the platonic universe of mathematical and software artefacts, and whether it decides to cooperate or not. Disbelieving in it --- a favorite strategy of mine --- has proven ineffective.

I was in a lousy mood after the CSL paper got rejected, but holy shit my implementation is actually kinda behaving now, so life is sunshine and unicorns and lollipops again. Except, of course, that I am not kidding about the lollipops.

Which is to say, I succeeded at adapting the LLF miniml-with-refs example with only a couple of hiccups. I found myself extremely perplexed at the very end of the process, with exactly one missing case reported:
tppres.elf:201.23-201.24 Error: 
Coverage error --- 1 missing case(s):
{K1:cont} {V1:val} {E1:exp} {W1:final} {T1:tp} {T2:tp} {T3:tp} {P1:w}
   {Ex1:exec (K1 ; ([x2:val] return (pair* V1 x2))) (ev E1) W1 P1}
   {Ok1:ofk K1 (T1 ** T2) T3} {E2:exp} {Oe1:ofe E2 T2} {Ov1:ofv V1 T1}
   {Of1:off W1 T3}
   |- tpex P1 (ex_pair1 P1 Ex1) Ok1 (ofi_pair1 Oe1 Ov1) Of1.

val it = ABORT : Twelf.Status


Because, I mean, how the heck is my code failing at something specific to the second stack-machine instruction of pair-formation? Then I went back and found the bug was a typo in the original code:
ofi_pair1 : ofi (pair1 V1 E2) (T1 ** T2)
	     <- ofv V1 T1
	     <- ofe V2 T2.

A misnamed free variable (should have been E2) meant that too many stack machine instructions were well-typed, so type preservation was false.

So even though it's not really my code (but rather the pre-existing coverage checking that is not really touching the world equational theory at all) finding that bug, it was a great feeling being able to run the tool over a signature that used linear features and find a error in the theorem being claimed rather than just having bugs and barfing unhandled Match exceptions all over my shoes.
Link4 comments|Leave a comment

(no subject) [May. 27th, 2009|07:17 pm]
[Tags|, ]

Trying to go through and adapt Frank and Iliano's LLF miniml type preservation proof to the HLF implementation. The modes of the higher-order thingies having to do with reference cells are slightly more subtle than I expected, but once I understand what they're supposed to do it's all quite lovely, actually.

For any of you that enjoyed Schild's Ladder, I might recommend taking a look at Spin Networks, the thing Egan's fictional "Quantum Graph Theory" was clearly based on. I found the original Penrose paper on the topic to be astonishingly readable up until about page 26 when he starts talking about 'twistors', which are to SU(2,2) and SO(2,4) what spinors are to SU(2) and SO(3). Also this is a more recent tutorial paper with another crop of pretty diagrams.
LinkLeave a comment

(no subject) [May. 27th, 2009|11:17 am]
[Tags|]

Hee hee last.fm allows music uploads and makes them look all legitimate,
see here for instance. (warning: autoplays music) Some piece of electronics I was using for this recording picked up a radio signal that can be faintly heard.

Hm, though I can't see any way of conveniently autoplaying or downloading the whole album. Is this a known fault of last.fm? Should I use imeem or something instead?
Link1 comment|Leave a comment

(no subject) [May. 26th, 2009|11:04 pm]
[Tags|, ]

Went to Peter O'Hearn's talk. I kind of enjoy talks that are clearly about not-quite-finished work, full of interesting speculation and conjecture. [info]simrob pointed out a nice encoding technique for the pi-calculus into focused bunched logic. I guess one ought to really sit down and bang out what focused bunched logic is - on some level it's simple what to say about the connectives, but what happens with the structural operations is a little more subtle, but I think we all (by which I mean at a minimum frank, rob, and I) basically know what to do with them, either from the getting-the-example-to-work-right angle, for from the general theoretical angle.
LinkLeave a comment

(no subject) [May. 24th, 2009|08:46 pm]
[Tags|]

Balanced my checkbook. It's super tedious when you wait so long to update that your bank's "recent activity" with running balance fails to reach all the way across your period of slacking and you have to go back and type stuff in from your old statements.

I still find the beautiful conservation-law magic of double-entry accounting to be stunning.
LinkLeave a comment

(no subject) [May. 23rd, 2009|04:56 pm]
[Tags|, ]

Distraction from thesis number eleventy million:

I wanted to quickly submit (a cleaned-up version of) "judgmental deconstruction of modal logic" to IMLA, and I figured I should hack up a nice little summary figure with diagrams for all the encodings, so I took a look at TikZ, since spoons recommended it to me some time ago.

I would like to say it's not the be-all and end-all of LaTeX graphics packages, except that it is. Oh my god, it has everything. [info]_tove: you are free to make fun of me for drooling over the lovely faded-out primary-color color-scheme that is used throughout the examples.

---

Here is the revised version if you would like to see the diagrams. TikZ is super slow to run, but it does make nice graphics rather convenient.
Link1 comment|Leave a comment

(no subject) [May. 22nd, 2009|11:59 pm]
[Tags|, ]

Went to Derek's talk, (verdict: quite interesting) and talked to him for a while after about researchy things.
LinkLeave a comment

(no subject) [May. 21st, 2009|10:55 pm]
[Tags|]

The wungsten/Näthan & Dave Bernabo show was so great! I am glad I succeeded at getting to it, and also dragging Erika along, whom I ran into just before it.
LinkLeave a comment

(no subject) [May. 21st, 2009|03:33 pm]
[Tags|, ]

More manifest security meeting today. Didn't understand as much, I think. One of those things where you actually do acquire new facts, but the content of those facts is finding out that you didn't really understand things as well as you did previously.

Wungsten show tonight! This time I will not miss it! It will be much easier what with it being on campus.
LinkLeave a comment

(no subject) [May. 20th, 2009|11:59 pm]
[Tags|]

There was this Manifest Security meeting happening today that I sat in on. Neat stuff. I think I finally understand exactly how Henry and Frank's paper can be 'deconstructed', and it's quite simple. Make a poset with judgments knows_K, has_K, asserts_K, valid, true, lax. What the paper calls "hyp" on the left is the same as what it calls "true" on the right, and I'm calling them both just "true". Valid and knows_K are unrestricted, and the rest are linear. Axiomatize the stronger-than relation by taking for every K all of
knows_K ≥ has_K
knows_K ≥ valid
valid ≥ true
has_K ≥ true
true ≥ asserts_K
true ≥ lax
and taking the reflexive, transitive closure. Then all the connectives are defined "at true". The connectives [[ ]], [ ], < >, !, and { } are defined as round trips through knows, has, asserts, valid, and lax, departing from and returning to true.

Afterwards tagged along with rwh and ben pierce and one of pierce's students for dinner, much technical conversation ensued.
Link1 comment|Leave a comment

(no subject) [May. 19th, 2009|03:48 pm]
[Tags|, ]

Finished "Permutation City". I thought [info]gwillen was a fast reader for finishing it in two days, but so did I. I found it quite the page turner. Increasingly ridiculous as the story went on, but I still found it tremendously fun. Not unlike "Anathem" on both counts, and this one lacked some of Stephenson's slightly annoying conceits.

Got cut elimination working in the HLF implementation for additive conjunction, and multiplicative unit! That makes six "connectives" that work, now, 1, top, bottom, ampersand, trivial, and atoms. I am super stoked. I am slightly cheating, since I am making use of monotonicity without checking it, but it's a very heartening proof-of-concept. Also, I finally got around to checking it in as a real branch rather than in my own subversion repository. It is at https://cvs.concert.cs.cmu.edu/twelf/branches/twelf-hlf/

My INBOX contains two items, both pertinent to the immediate future. Doin' that inbox zero thing. We'll see if it Changes My Life.
Link11 comments|Leave a comment

navigation
[ viewing | most recent entries ]
[ go | earlier ]