Lambda the Ultimate

Courtesy of my shiny new commute, I have been listing to various podcasts, including Software Engineering Radio. A while back, they had an interview with Dan Grossman on his OOPSLA 2007 paper, which I have not seen discussed here.

The Transactional Memory / Garbage Collection Analogy is an essay comparing transactional memory with garbage collection based on the analogy:

Transactional memory (TM) is to shared-memory concurrency
as
garbage collection (GC) is to memory management.

Grossman presents the analogy as a word-for-word transliteration of a discussion of each of the technologies. (Hence the "fun" category.)

(As an aside, Grossman does not address message-passing, but says, "Assuming that shared memory is one model we will continue to use for the foreseeable future, it is worth improving," which is probably a correct assumption.)

One point that he does make is that

[This essay] will lead us to the balanced and obvious-once-you-say-it conclusion that transactions make it easy to define critical sections (which is a huge help in writing and maintaining shared-memory programs) but provide no help in identifying where a critical section should begin or end (which remains an enormous challenge).

The one serious weakness of the analogy, to me, is that GC does not require (much) programmer input to work, while TM does.

Although some parts of the analogy are strained, there are some interesting correspondences.

What portion of linear lambda calculus corresponds to using only the B and I combinators (composition and identity)? I have a hunch that it's all lambda terms that use their input variables exactly once and without permuting them, but I'm finding it hard to prove that.

The standard abstraction elimination algorithm doesn't work to give a combinator:

\abcd.a(b(cd))
=\abc.B a (B b c)
=\ab.B (B a) (B b)
=\a.B (B (B a)) B

and to eliminate the variable "a" here, I need to use the C combinator.

But there is a combinator that is extensionally equivalent that doesn't use C:

\abcd.a(b(cd))
=\abc.B (B a b) c
=\ab.B (B a b)
=\a.B B (B a)
=B (B B) B

It depends on using the associativity of composition.

How can I tell which linear terms are in the span of B and I?

I'm looking into defining a flow-sensitive effects system for Java (to check things like the definite assignment of local variables). Does anybody know of a good existing Java-like formalism I could use?

I don't think Featherweight Java is appropriate here because it mostly ignores Java's control-flow mechanisms. Much of what's interesting about a flow-sensitive effects system has to do with loops, conditionals, exceptions. On the other hand, I care less about things like classes and inheritance.

Maybe the simply typed lambda calculus (plus some Java-like exception mechanism) would work better?

Proving that particular methods within a code base are functionally pure - deterministic and side-effect free - would aid verification of security properties including function invertibility, reproducibility of computation, and safety of untrusted code execution. Until now it has not been possible to automatically prove a method is functionally pure within a high-level imperative language in wide use such as Java. We discuss a technique to prove that methods are functionally pure by writing programs in a subset of Java called Joe-E; a static verifier ensures that programs fall within the subset. In Joe-E, pure methods can be trivially recognized from their method signature.

The paper includes a nice discussion of security benefits that can stem from being able to identify pure functions (of course, it is not obvious that guarantees at the programming language level are maintained at the run time level). I am sure many here have opinions about whether it makes more sense to try to graft purity on an imperative language, exposing it as an added feature, or to move programmers to functional languages..