More on Modal Logic

Whilst I appreciate and, I hope, understand the pedagogical value of using "practical" examples to offer motivation for topics that can, like modal logic, seem purely theoretical, I am beginning to appreciating just how interesting, versatile and useful a field modal logic really is by looking at it from a more theoretical and general point of view. The first twenty-four pages of Modal Logic (Blackburn, de Rijke and Venema) have impressed upon me more readily and immediately than umpteen different modally interpreted implication operators or logics of time did, the flexibility of the modal semantics that I was taught in Philosophy and Logic.

That is not to say, however, that the more theoretical approach is better or more suitable than teaching "by example". In a course without prerequisites in mathematical reasoning, teaching modal logic by focusing on examples of its use is the most obvious, and quite probably the best, course. Without the opportunity to study modal logic in such a course, it would probably not have caught my attention and I would be in no position to be reading this book.

More on Composable Memory Transactions

Caveat: I am not an RTS expert, not a Haskell expert, nor a concurrency, languages, or OS guru. This little spiel is probably rife with errors, but I'll publish this post in the hope that someone will point them out.

Having read the rest of the paper, its strikes me [even more than it did] just how cool software transactional memory (STM) is. I wonder how effective it would be in an language with object oriented features. In a language like Haskell (what with its functional purity and laziness) it makes sense for the atomicity of transactions to be guaranteed by the runtime systems thread scheduler, but I couldn't help but see the potential the implementation in GHC has for helping map Haskell threads onto OS thread primitives.

The simple scheme described in the paper for validating and committing transactions might be extended, to allow concurrent validations and commits by adding per TVar locks and locking the TVars accessed by a transaction. If I recall correctly, deadlock and a number of other concurrency pitfalls could be avoided by using a lock-ordering protocol of some description (probably just ordering locks on the TVar pointer order). I'm not sure how much, if any, improvement in throughput might be observed, but allowing concurrent commits would probably increase the utility in adding more fine-grained multithreading to Haskell, by easing the development of safe concurrent programs.

As I said at the top of this post, I am not an expert in any of the fields touched on here, but I'd love to hear from those who are if anyone would like to point out my errors.

Composable Memory Transactions

Composable Memory Transactions. Tim Harris, Simon Marlow, Simon Peyton Jones, and Maurice Herlihy. Submitted to PPoPP 2005.

I found this paper through a link from Lambda the Ultimate, a weblog about programming languages.

Though I've not yet read the complete paper, it has really impressed me. This use of monads, for me at least, justifies them in a way and to an extent that none of the rather limited set of explanations I've seen to date has been able to. The simplicity with which the transactional framework described in the paper can be used is amazing. Though I've yet to understand everything it describes (especially the semantics and implementation which sections I haven't even read yet), I think I'm going to have to get the GHC head, and return to learning Haskell.

I think I'm going to have to go through the MS Research publications sight for more interesting things to read.

The Code Book (Simon Singh)

The Code Book (Simon Singh)

A week or two ago, I finished reading Simon Singh's second book: The Code Book and it is every bit as good as Fermat's Last Theorem was. Simon Singh is, in my opinion and experience, one of the best popular science writers around (though I still need to get a copy of A Brief History of Time). I'd write more on the book but anything I could say, has already been said.

The publisher's site for the book
The author's site

Logic, modal and otherwise.

Attending the Logic Summer School at the Australian National University has encouraged me to continue my studies of formal logic begun with the unit HPA292: Logic and Philosophy more informally on my own.

To this end, I purchased the Cambridge Tracts in Theoretical Computer Science book Modal Logic. My initial impressions are favourable, though I've not read much of the book.

I'll expound here in further detail on the merits of this book at a later time.

A new blog

I've decided that I'm going to start a new 'blog. Lately, I've been struck by the realisation that most of my reading is being wasted: I waste time reading random junk on the net and neglect the papers and occasional book to which I ought to be devoting my attentions.

In an attempt to spur myself into action, I will be writing this weblog my thoughts and impressions, perhaps even reviews in some sense, of the papers and books that I read.

Uploading a photo