Jason (jcreed) wrote,
Jason
jcreed

Up to ep 12 of French in Action. It's still intensely surreal. There haven't been any classroom scenes in it for a little while. And I was just starting to warm up to the token irritating-smarmy-guy-who-already-has-some-level-of-fluency-and-likes-to-show-off. I really liked that as a nod to the realities of foreign language teaching in a classroom setting.

Still chugging away on "Modern Mind" as well. At this rate (a chapter a day) it'll still be another week and a half before I finish it. This is a considerably longer burden of attention span than I usually give to a single book, but this one's paying off pretty well.

Worked some in the morning, and last night, on a side project not really relevant to my current research project, but rather to the one I was working when I was a first-year. I hacked up a little theorem prover for propositional "proof-irrelevance" logic and discovered that the irrelevant negation (ie, A →i ⊥ for →i being irrelevant implication) is really wacky. No implication generally holds between A and (A →i ⊥) →i ⊥, unlike with ordinary negation, where intuitionistically at least you get one direction, and classically both. And much like in ordinary intuitionistic logic where the iterated negations of A lead to only three distinct propositions: A, ¬A, and ¬¬A, iterating the choice of ordinary and irrelevant negations leads to only a finite number of possibilites: but there are seven. The six new ones are somehow "strong", "standard", and "weak" versions of odd-parity and even-parity negations. Anyway, I tried working out a focussing calculus for it and ran into major difficulties. Maybe I should get back to finishing my actual project for the summer...

In other news, I ran into Jason Corwin at Veracruz, (who was also CMU class of '02) who is leaving for Austin in a matter of weeks to start a company making digital guitar effects. That sounds pretty awesome. I'm kind of jealous.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments