(4 comments | Leave a comment)

Wow, my theorem proving environment is almost like a real research tool now. Last night it aquired its very own file format (as opposed to collections of SML functors that mutate the environment).

Roughly speaking, I am now able to prove things about sequences of instructions that are organized into functions. So I suppose one could say that there is progress. Although something the size of the Boehm collector still seems worlds away.

More than anything, I'm amazed how far I've been able to come without having to implement higher order pattern matching.

Current Mood: pleased

(Leave a comment)

Since the summer, there has been some (what one could generously call) lateral movement, but lately we've been moving steadily forward:

(This is, IMO, much more impressive when you consider that we only have one axiom on which to build induction – the analog of the Axiom of Infinity in ZFC.) Also, as you can see, all the real work happens inside two lemmas. So lemma management is working reasonably well (although I would really love to have a proper module system in Twelf).

Current Mood: accomplished

(5 comments | Leave a comment)

Today I have proved a most remarkable theorem:

Theorem:

pi nat ([x] (pi nat ([y] (eqlty nat (app succ x +n y) (app succ (x +n y))))))

Proof:

lam ([x] (lam ([y] (prnat ([#] (eqlty nat (app succ # +n y) (app succ (# +n y)))) (tlam ([phi] (llam ([u] u)))) ([z][i] (app (ann (lam ([i'] (tlam ([phi] (llam ([u] (lapp (tapp (lapp (tapp (lapp (tapp i' (clam nat ([z$1] (eqlty nat z$1 (app succ z +n y))))) (tlam ([phi] (llam ([u] u))))) (clam nat ([#] (eqlty nat (app succ (app succ (z +n y))) (app succ #))))) (tlam ([phi] (llam ([u] u))))) phi) u))))))) (pi (eqlty nat (app succ z +n y) (app succ (z +n y))) ([i'] (eqlty nat (app succ (app succ z) +n y) (app succ (app succ z +n y)))))) i)) x))))

Now to work on normalizing these things...

Can commutativity of addition be far behind?

Current Mood: accomplished

(Leave a comment)

Tempted to spend evenings hacking on the gnome2 port of gnucash. On the bright side I'd be scratching a personal itch, on the downside it'd be C hacking and library dependency hell and I don't really have the time for it.

Maybe i should learn French and hack on grisbi.

Or worse, I could learn C# and hack on kurush.

I wonder if there are any accountants who know Haskell...

Current Mood: working

(2 comments | Leave a comment)

There's a review of Okasaki's Purely Functional Datastructures on slashdot.

I always get very agitated when slashdot "discussions" drift towards PL. The sheer staggering absolute wrongness of how hackers approach PL is amazingly gut-wrenchingly painful.

I guess maybe tonight I'll have a beer or three and give in to my morbid curiousity. The alcohol should help buffer the pain from when I inevitably start bashing my head against walls, desks and other heavy blunt objects.

Current Mood: cynical

(3 comments | Leave a comment)

Old lesson: when implementing a type inference algorithm, test it. (well... really "prove it correct," but who has time to be that meta?)

New lesson: test it on type-correct examples and not ones without valid derivations.

Penalty: about 3 hours.

One-character fix: replace f by g in the definition of compose.

Current Mood: frustrated

(Leave a comment)

Note to self: do every case of an induction proof. You have no intuition for when stuff in linear logic "just works out".

Grr

Current Mood: annoyed

(1 comment | Leave a comment)

Thinking about random Haskell wankery. Attempting to install an RPM of GHC 6.2, of course, fails on my RH7.1 machine in the office. Will have to make do with 5.04.2. Not that I do any Haskell at school.

Although now that 6.2 supports arrows syntax I suppose I'll have to finally sit down and grok it. Maybe I just haven't attempted to do anything really complicated with monads yet, but I find Arrows to be sort of under-motivated for my needs as a simple functional programmer. (Although as an armchair category wanker I find them sort of cute).

I predict that none of this will be relevant to any of my daytime research in the next two years.

(3 comments | Leave a comment)

Plato.stanford.EDU is nifty. The section on substructural logics is of particular interest to me.

(Leave a comment)

Lesson of the day: Do not become married to your typesystem before you've proved it safe. Feel free to add weird new judgments if they give you what you want. Variable names suck, but sequent calculus left rules are teh r0x0r.

(Leave a comment)

Todo list for the near future:

• Prepare a lecture for 814 about existential types based on Chapters 24,25 from Pierce
• Work out how far normalization gets us in showing safety for ProofGC.Push through on the safety proof for ProofGC using resource contexts
• Grade some homeworks
• Prepare slides about HM(X)
• Journal stuff

The former three are all by Wednesday. Slides are Friday morning, journal stuff is by the end of next week.

(Leave a comment)

Was reading Andrew's senior thesis about Moby Dick. There's a quote in there, due to Melville, that I will have to steal at some point:

I hereupon offer my own poor endeavors. I promise nothing complete; because any human thing supposed to be complete, must for that very reason infallibly be faulty.

From p. 935 of the 1967 Norton Critical Edition of Moby Dick.

(Leave a comment)

Welp, I suppose the purpose of this journal is to collect my various thoughts related to my research or to programming in general. If any broad patterns evolve, they ought to be exported into full-fledged essays on my page. Although I imagine that most things I say here will be incorrect and/or complete non-starters.

Hrmf... no real thoughts yet. Although over the weekend I was thinking a bit about non-interference and how it (maybe) related to deontic logic. Insecure programs are morally wrong, aren't they?

In general it seems like a fruitful path through type theory is to pick an obscure logic that someone someplace thought up in the 1930's, develop an intuitionistic fragment of it, and then come up with an operational interpretation of it via propositions-as-types. (Well, I suppose in reality you start with an operational intuition and try to bang logics onto it until you get something sane).

(Leave a comment)