Lambda the Ultimate

A Topos Foundation for Theories of Physics: I. Formal Languages for Physics. Andreas Döring and Chris Isham.

This paper is the first in a series whose goal is to develop a fundamentally new way of constructing theories of physics. The motivation comes from a desire to address certain deep issues that arise when contemplating quantum theories of space and time. Our basic contention is that constructing a theory of physics is equivalent to finding a representation in a topos of a certain formal language that is attached to the system. Classical physics arises when the topos is the category of sets. Other types of theory employ a different topos. In this paper we discuss two different types of language that can be attached to a system, S. The first is a propositional language, PL(S); the second is a higher-order, typed language L(S). Both languages provide deductive systems with an intuitionistic logic. The reason for introducing PL(S) is that, as shown in paper II of the series, it is the easiest way of understanding, and expanding on, the earlier work on topos theory and quantum physics. However, the main thrust of our programme utilises the more powerful language L(S) and its representation in an appropriate topos.

This is a little outside of our usual areas, but I think it will appeal to at least some readers. Personally, I find the approach aesthetically very, very appealing for several reasons, and I would be thrilled if an answer to quantum cosmology came from this direction, but I'm the first to admit that my grasp of the phsyics is barely enough to follow along. I was able to make it through this paper fairly easily, but things aren't too interesting in the classical case, and I sadly suspect that the application to quantum physics in parts II and III will leave me behind.

Via The n-Category Cafe, where there is also considerable discussion, much of it around the single word "peristalithic"...

I am a little late in passing on these news, but the new ISO standard for Ada is now officially published.

We discussed the new features in this revision of the language a couple of times before, so search the archives if you are interested. Among the new things are interface (as in Java), a container library, and the ability to use the "distinguished receiver" or prefix style in method calls.

For the record, the the recommended informal name for the latest Ada standard is Ada 2005, not Ada 2007.

We are pleased to announce the Twelf Wiki, a major new source of documentation about Twelf:

http://twelf.plparty.org

Twelf is a tool used to specify, implement, and prove properties of deductive systems. The Twelf Wiki includes:

• A new introduction to LF and Twelf.
• Tutorials on common Twelf tricks and techniques.
• Case studies of larger applications of Twelf, including encodings of and proofs about linear logic, mutable state, and CPS conversion.
• Pre-compiled CVS builds of Twelf for Linux and Windows.

We invite you to come share what you know, learn from what's there, and ask questions about what's not.

- The Twelf Wiki Team

(I know many of the people working on this, and they've put in a lot of effort to make a really useful resource.)