Lambda the Ultimate

By "frame problem" I (and I hope others, although there is always a risk of believing one's terminology is shared beyond a small community) mean the general question of specifying and proving what does not change in an operation. Contracts typically specify what changes and how it changes: in a bank withdrawal operation, the account's balance gets decreased by the specific amount. They seldom exhaustively state what does not change: the withdrawal operation should not replace the name of the account holder, the account number, the name of the bank. Full-fledged proofs must work with complete specifications that handle both kinds of properties.

This is indeed related to the AI notion of frames as defined by Minsky in the seventies, but with a specific software engineering meaning.

This is indeed related to the AI notion of frames as defined by Minsky in the seventies, but with a specific software engineering meaning.

Frame problem was described by McCarthy, and has had some famous attempts at solving it, most notably using circumscription that failed on the Yale shooting problem counter-example [1]. Frame problem is not really related to frame languages, as described by Minsky. In Society of Mind, Minsky opines that his sheer dumb luck in writing that paper was that he was vague just enough so that others would be inspired to flesh it out in tangential ways. He then notes that sometimes being too formal with new ideas can make them harder for others to embrace, and that it turned out his vague specification was a blessing in disguise. Paul G. Bassett also describes a different frame language in his book, Framing Software Reuse, which can best be thought of in today's terminology as an invasive software composition system (using Frame-Oriented Programming 'adapt' composers); it is also mostly unrelated to the frame problem.

Many ideas related to the frame problem have their roots in AI, but also in term rewriting. Rewriting logic solves the frame problem by phrasing the problem in terms of concurrent action and change. See this paper by two Maude weenies.

[1] For what it's worth, the solution to this problem in circumscription-based logic is known as the commonsense law of inertia: things are guaranteed to stay the same unless they are affected by an event.

Thanks for correcting me regarding the anteriority of McCarthy's paper (http://www-formal.stanford.edu/jmc/mcchay69/node17.html#SECTION00043000000000000000). Minsky's 1974 paper (http://web.media.mit.edu/~minsky/papers/Frames/frames.html) was the one through which I first learned about the topic.

Sorry, Bertrand.

After re-reading Minsky's essay carefully (it's been awhile), he does cover the frame problem, but does not refer to it as such. Instead, he refers to the frame problem as a problem of defining "a 'minimal' common-sense system".

FORMALIZING THE REQUIRED KNOWLEDGE: Just constructing a knowledge base is a major intellectual research problem. Whether one's goal is logistic or not, we still know far too little about the contents and structure of common-sense knowledge. A "minimal" common-sense system must "know" something about cause-and-effect, time, purpose, locality, process, and types of knowledge. It also needs ways to acquire, represent, and use such knowledge. We need a serious epistemological research effort in this area. The essays of McCarthy {} and Sandewall {} are steps in that direction. I have no easy plan for this large enterprise; but the magnitude of the task will certainly depend strongly on the representations chosen, and I think that Logistic is already making trouble.

It's clear, upon re-reading it with the frame problem in mind, that Minsky is referring to the frame problem. The last time I read this essay, the McCarthy citation was {} as it is now, so I made no connection to it.

Thanks a lot! Sorry for the typo (copy-paste error), now corrected.

The paper looks fascinating, though I have only looked at some of it.

Please read all... I think the most important parts come towards the end, but the buildup is necessary.

It would be interesting to look at applications to buffer overlap. As it is, however, the alias calculus assumes a typed framework, so I don't know how it transposes to a word of addresses and untyped pointers. But it's worth looking into.

Thanks for the references, I have started reading them. Applications to concurrency are indeed next on my agenda, although I was thinking more of issues like deadlock in SCOOP than of security, so I appreciate the hint.

I share this concern. My first questions were how this 'aliasing calculus' could possibly be relevant in the presence of implementation hiding (and its cousins, such as distributed programming). Given that implementation hiding is at the core of OOP, I don't see how it will be relevant for anything but local optimizations of certain patterns (e.g. the capability revocation and other 'interference' patterns mentioned by MarkM).

Linear typing is somewhat more promising, allowing aliasing concerns and exclusive rights transfers to be enforced to some degree. Locally, it is subject to type-checking or language-layer enforcement. The sort of exclusive transfer of rights supported by various 'smart contracts' protocols might even allow linear typing to work with a distributed protocol, though I can only imagine there would be a rather hefty performance and communications cost associated with achieving that (i.e. essentially requiring the right be renamed to finalize each transfer crossing trust or security domain boundaries).

In any case, I share your difficulty in seeing how this alias calculus would be useful to me. If it cannot be applied at the interface level, then it certainly isn't useful for analysis of 'large' software. It isn't even clear what sort of features (optimizations, data-flow analysis, etc.) might be achieved via its local application.

Perhaps someone with the big-picture view can explain where Aliasing Calculus might be useful?

Since Mr. Brandl posted the same comment next to the original referred entry, I responded there. Let me mention, though, that his post provides excellent (informal) evidence of the difficulty of the issue. Looking at the original blog, we could deduce that he did not make any comment related to a comment by Jules Jacobs. Now if I add there (as I now did for the sake of the argument) that “comments #1 and #13 on the first external blog referring to this topic are related”, I introduce an aliasing of sorts between the two authors, which is only visible when we consider the two blogs together.

See the full response at the given URL.

what if the problem is essentially non-compositional?

Software is composition. Even software that doesn't involve components will ultimately serve as one. For the software that doesn't involve components, I would suggest you should find a better paradigm for said problem than OOP - which is ultimately all about composition of software components.

if you are in charge of a mission-critical development and have to sign as statement that the software is correct, you will want to verify the full thing anyway, not rely blindly on someone else's guarantee that some routine or class is correct

Software composition doesn't require we "rely blindly on someone else's guarantee that some routine or class is correct". Static analyses, auditing, and automated tests of various sorts may, of course, apply. But, for 'large' software, we must ultimately collaborate, communicate, and compose. Communicating to other developers how features interact is just 'interface' or 'protocol' by another name.

For clarity: by 'large' software, I refer to software whose implementation is detailed beyond the comprehension of any single human or group. Issues of incomplete specification, distribution, and upgrade are inherent in such systems. Similarly are issues of interface: describing how components or features interact with one another and their environment.

It is not "wishful thinking" to assert that 'large' software involves composition; that's simply the nature of the beast. If a problem precludes a compositional software solution, you hope it either need not be solved or that it can be solved with a small and complete software specification (such that it may be composed into other systems).

You are right to insist that software construction should be modular and software compositional . The problem is that if we consider existing programming languages (in this case modern object-oriented languages), we are studying an objective reality, much as a natural scientist would do, and have to consider the properties it has rather than the properties we would like it to have.

A property p is compositional if p (o), applied to an object o with components o1 and o2, can be deduced from p (o1) and p (o2), each determined independently of o. Unfortunately aliasing is not compositional in this sense. This is highly regrettable, but once we recover from the pain we can try to harness aliasing anyway, which is what my calculus attempts to do.

Since we are dealing with human artifacts rather than objects of nature, we can (unlike natural scientists) change the reality; this means using programming languages with no aliasing. But if we deal with languages that have aliasing we must accept the facts.