Kripke: Names, necessity, and identity

Kripke: Names, necessity, and identity
This sounds like an interesting book. I'll have to see if I can get a hold of it some how, as I don't really want to spend $130 on a book without at least looking at it first. On the other hand, if I spend $130 on a book, perhaps I'll bother to read it which will be an improvement.

Normally I buy books, and put them on my bookshelf, occasionally after having read a chapter or two.

A little bit on logic and trans-world identity

I've just posted a little bit about modal logic (more specifically the idea of trans-world identity) to a message board I read. My post was in response to a post in a thread about a story in which a character uses a portal to visit herself in other worlds. The originating post, my reply and a follow-up by personal message follow.

If anyone spots any glaring mistakes or omissions in the below, I would very much appreciate having them pointed out in the comments (as though anyone will read this).

et alia wrote:

Believe it or not, there's a work of contemporary philosophy devoted to this topic: Saul Kripke's Naming and Necessity. Anyone else here know it? If I remember correctly and follow his arguments from that work (two big ifs), it'd be girl with the same name that Daria should talk to.

Argh!--just realized this: since the hypothesis of the story is that Daria analogue opens the open, then n world Daria should open the door, i.e., the girl who looks like Quinn, etc, but is named Daria. There's potential for "who's on first" dialogue:

<snip>

My reply:

The issue of trans-world identity is quite interesting philosophically and is one in which there are a lot of points of view.

I, personally, like the counterpart theory (due to Lewis), in which there are no objects that are the same from world to world. What we mean when we speak of Daria from world n is the thing that is most similar to the actual Daria (i.e. the one we thing is "real"). All the "Daria"s are equally real, and completely unrelated, except through the counterpart relation.

There are alternative views in which the Darias are all part of one trans-world object, a kind of Uber-Daria. This is called mereology (IIRC) and the various Darias are just world indexed parts of the trans-world Daria. This view is somewhat related to the idea of temporal identity (i.e. am 'I' the same thing that sat here yesterday and browsed this forum?). The temporal variant is pretty much the same (just replace "world" with "time"), but also a lot stronger as a person has some form of spacial continuity between instants (i.e. I'm pretty close to where I was from one instant to the next), whereas there is no continuity between objects at different worlds.

Another view which might be taken into account is haecceity (literally, "this-ness") in which there is some ineffable thing (a je ne sais quoi if you'll forgive the pretension) that makes Daria-n identical to Daria-m, even if one is a person and the other a cement block. This is, needless to say, a little weird, but the whole concept of trans-world identity is a bit strange anyway.

If anyone cares to read more, I can post some references, or you can just look for books on modal logic (if you like formalisms) or the attendant philosophy of possibility (and lots of other stuff) in your local library.

My follow-up by PM:

First of all, I'm no expert, so you'll have to take what I've said, and will say with a grain of salt. Additionally, I'm more interested in the formalisms of modal logic than the attendant philosophical issues, so I don't pay as much attention to them than I might otherwise. I'm writing this the better part of three months after the end of my unit on modal logic. Needless to say, I'll probably make a few mistakes.

If you're familiar with formal logic, you might be familiar with the concept of an interpretation which assigns values to logical formulae. In propositional calculus, or PC, (ordinary two-valued logic with 'and', 'or', 'not', 'implies' and 'equals' and an alphabet of propositional parameters 'p', 'q', ... which stand for propositions). An interpretation of PC is simply a function v [the Greek letter nu, if you can type it :-)], which is a function from logical formulae to true or false.

PC is normal everyday logic. It is simple, obvious, and to most people fairly intuitive. It also doesn't really match the way we speak or think about a lot of things. Things like possibility and necessity ("Surely it is possible that I be Prime Minister."), temporality ("Tomorrow, we will try to take over the world!"), belief ("If Jill knows that John is drunk, she'll ...") and a whole bunch of other things that we talk about can't really be encoded into PC without causing problems.

Modal logic is one approach concerned with reasoning formally about these concepts. In general, modal logic is concerned with reasoning about relational structures, like possible worlds, or instants in time, or any set of things that can be represented as a graph (or network).

The most basic interpretation of modal logic is , as set of Worlds, a Relation between them, and an interpretation function that is a little more complex than that for PC.

I'll skip the whole great big raft of crap on modal operators and more than one modality here, as there are plenty of books on the subject and I wouldn't be able to write a passingly good blurb, never mind a book.

Another form of logic for reasoning about relational structures is quantification theory (QT). The main difference between modal logic and QT, is their perspective. In modal logic, one examines the structure from the inside (e.g. from the "world n", or "time t", etc) whereas with QT one has a gods eye perspective (e.g. you can see all the objects, not just the ones you can reach from here).

With plain modal logic, W (the set of worlds, times, whatevers) contains the "things" with which the logic is concerned and the most we can do regarding things IN the worlds (or times, etc) is say "the cat is green" is true or not. Combining QT with modal logic however we can say things like: it is possible that, for all objects x, if x is a cat, then it is green (which would be something like:

<>(Ax . isACat(x) -> isGreen(x))

where the <> is a diamond modal operator and the A should be upside down and stands for "forall", but I can't be bothered trying to type the correct symbols).

This then leads to a number of logics, one of which has the interpretation , a Domain of all objects (all the objects in all the worlds), a set of Worlds (times, etc), an accessibility relation between the members of W, and v (the truth function). Then all the mess comes in about objects being present in two worlds (if there is me in world n and me in world m, then are they two different objects in D? Are they the same object in D? If they're the same object, how can they be in two worlds at the same time?, etc). There is LOTs of stuff about this, Lewis is a good start (a search for Lewis and modal logic will probably get you heaps), Meinongianism is an interesting perspective where there are non-existent objects like the proverbial pigs-with-wings (Routley Exploring Meinong's Jungle and Beyond). On the other hand, modal logic is not a give and does have detractors. The only one that springs to mind is W. V. Quine.

Merging QT and K (the basic modal logic) as above leads us to questions about identity between objects in different worlds. Is the Daria in canon the same person as the Daria in John? There are four approaches to this that I'm familiar with. The first is to say that there is no identity between worlds, that canon-Daria and John-dating-Daria are completely different entities. This is called extreme essentialism and one proponent is Chisholm.

The second is the counterpart theory proposed by David Lewis and explained, however briefly, in my post on the message board.

The third is haecceitism, also covered above. It is also something of a cop-out to say that "canon-Daria and John-dating-Daria are identical because they are" (in my opinion at least).

The fourth is mereology. This holds that canon-Daria and John-dating-Daria are parts of Uber-Daria, a trans-world "whole" composed of all the Darias in all the worlds. This is similar to an approach to temporal identity, as I explained previously. An interpretation of a mereological modal logic might be where the Domain is a set of parts (the things in worlds) and the members of the set of Worlds (times, etc) are linked by a Relation. There is also a set of Functions which, given a world, return a part from D. The members of D then, are the things that exist in worlds, and the functions in F are "individuals". That is, f (a member of F) represents Daria. At the world canon, f returns canon-Daria, which is the thing that is "Daria" at the world canon. At the world John, it returns John-dating-Daria, which is the thing that is "Daria" at the world John. There are a few philosophical approaches that result in a semantically equivalent logics, but I can't really remember them.

If you're interested, I'd recommend seeing if your local University offers a course about modal logic, and see if you can go along. There are also a wealth of fairly good books on modal logic. If you like formalisms (i.e. mathematical proofs, etc) "Modal Logic" a volume in the Tracts in Theoretical Computer Science series from Cambridge University Press is good as well as detailing the true generality of modal logic (the modal operators and multiple modalities mentioned above). Finally, there are a large number of resources on the web. There are lots of 'blogs by students of logic, and you should be able to find a lot of paper, most of which won't make much sense.

Once again if anyone has any pointers to interesting material, comments or criticisms of my explanations above, please feel free (I'd like to say obliged, but you aren't) to post comments.

Additionally, this post wouldn't have been possible without the efforts of Dr. James Chase to endow a class of undergraduates with some little (in my case at least) understanding of modal logic during HPA292 - Logic and Philosophy.

Tools for reading

Since I got my iBook, I've been using Bibdesk to manage a BibTeX database of the papers I've downloaded (and bothered transferring to my laptop). It's quite cool. Well, once you get past a few bugs, it's quite cool. It ties in with Preview's recent documents or will move a file that you select to your "papers folder" (it won't do both as far as I can tell).

Whilst this is pretty cool, I've been thinking that BibTeX is a little annoying (what with it wanting to rewrite capital letters unless you use braces as the string delimiters, etc). Lately I've been thinking that perhaps an XML format might be just what the doctor ordered. DC probably supports as many fields as necessary. The only problem might be the bunch of publication types that bibliography styles typeset differently, though I'm sure that there is a DC element (and maybe a dictionary of terms) to describe document types.

In any case, I'm too lazy to switch from something that works (BibTeX, et al) to something that I'd have to write myself (because using someone else's would defeat the purpose :-).

---

Other things that might be useful are some software to convert PDF and PS documents to text and an automatic text condenser and an outline editor. The former would help process those pesky documents without abstracts, whilst the latter would help note-taking and the like. If anyone happens to read this and knows of any free software (for Mac OS X, or UNIX) which fits the descriptions here, post links in a comment.

On a Mac

I like this. I'm sitting here at my desk in my room at Burgmann College (paid for by the RSISE as part of my Summer Research Scholarship). I've just posted an entry on my other 'blog (Very Big Graphs) to the effect that I've just discovered that I needn't have done a lot of the work I have done and that, had I read the documentation for the library I'm using, I would've known that.

The part of this situation that I like is that I only realised this because I've been working in Xcode on my new iBook for the last two days. The iBook is seriously cool. If anyone on the OS X team ever reads this: you rock (and could you tell the hardware engineers to read this next bit). If anyone of the Apple engineering team ever reads this: you rock (and could you tell the OS X people to read that last bit). This is probably, of all the computers I've owned, my favourite.

The only problem is the I now have the urge to switch completely: the Mac mini is looking quite tempting. I'll be able to hold out for a while (primarily due to a lack of disposable income), but once I've got my enrolment, accommodation and various other fees out of the way, I think that some small part of my scholarship might become available for conversion to a more solid, white, Mac branded form.

Another benefit is the software. I'm starting to get used to everything "just working". Unfortunately there are a few bugs in some things I've been using (like Bibdesk, a bibTeX database editor), but on the whole, I like it.

Thoughts on a Programming Language

I've been thinking for quite a while now, that I'd like to have a go at writing my own programming language. I've been slowly working my way, little by little, through some of the ideas I'd like to experiment with in my language over the last couple of years. The Software Systems and Programming Paradigms units I took last year gave me a lot to think about, as have exposure to languages like Io, Haskell, Scheme, Python and Java 1.5.

Though I still have a lot to study in more depth (especially in the areas of semantics and type systems, neither of which I have actually studied), I've come up with a few features that I want in my language.

1. A lightweight, flexible type system.

I'd like my language to have a type system that includes a number of features usually only found in heavy weight languages like Java, Common Lisp and C#. First amongst these is some form of inheritance and polymorphism. This has fairly obvious benefits, and is something I missed during my brief foray into the world of Haskell (either because it isn't possible, or I didn't know how). Second is some form of parametrised types to implement generics (and whatever else one uses parametrised types for). Parametrised types and generics are a more subtle beast. I don't really know if they will be any harder [than inheritance and polymorphism] to implement, but they will make any language immeasurably more usable, especially for collections and various patterns involving proxying of one form or another.

Another aspect of the type system that will be essential is being light weight. If the language winds up supporting run-time loading of objects (like Java, C#, et al) it will need to support run-time type checking, which means that it'll have to have some form of type tagging, boxing, etc. I would like to keep this as minimal as possible, ideally, it would be [at most] a single word per object.

2. Support for object-oriented programming.

Hand in hand with the specialisation and polymorphism and parametrisation (in my opinion at least) is support for object-oriented programming techniques. Whilst I'm still of two minds about making everything an object, I do think that the <object>.<verb> form makes a lot of sense for certain operations. I also think that supporting a restricted multiple inheritance, be it mix-ins or just interfaces, paired with polymorphism, can provide similar amounts of power to operator overloading in C++, or type classes in Haskell.

3. Fine grained memory access, if you want it.

In addition to object orientation, I think that fine grained access to memory is essential. One of the main goals I have is to be able to do similar things with objects and collections in my language, as I can do with arrays of structs in C, with similar efficiency. This will probably mean that the user will need to have some way of controlling memory access, probably via the type system.

4. A functional flavour.

Whilst I do like functional programming, sometimes (especially when dealing with things like the "tables" described in point 3) a little bit of statefulness is essential. As cool as the monads in Haskell are, I'm going to try making functional-ness optional. Things like predicates should be functions. Things like operators should, arguably, be functions. Accessor methods probably shouldn't.

5. Real support for concurrency.

I love the idea of language level support for concurrency. Transactional Memory (see my earlier posts) is a brilliant idea. The paper on undo in C# is also fairly interesting. I intend to use native threading support in my run-time to implement things like co-routines and actors as well as more traditional concurrency primitives. This is one the aspects I find most interesting. Adding support for high level concurrency primitives will have, I hope, a similar degree of impact on the languages usability as generics.

On the whole, I'm not much closer to being able to write my own language than I was last year, but my ideas have coalesced into a much more coherent form. I hope to start working some time this year on it, which means I need to start reading up on many aspects, especially formal semantics, in between doing my Honours.

I'd better get started.

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