Lambda the Ultimate

I'm looking for a name for, and work that's been done with, a certain model of computation. I'm guessing it would come up in untyped denotational semantics. The basic idea is to take computations to be their behavior on symbolic parameters.

Define n-computation as infinite data (in pseudo-syntax):

data Comp n:Nat = Diverge | Parameter (0..n) | Computation (Comp (n+1)) | Apply (0..n) (Comp n)

Here 0..n is the type of an integer in that range. The four data constructors' meaning is, when supplied a parameter:

• Diverge - Diverge
• Parameter m - Return the mth formal parameter seen "thus far" (see below)
• Computation f - Return the computation f
• Apply m f - Apply the mth formal parameter to computation f

Basically you treat a computation as a little machine that accepts a formal parameter, and computes as much as it can until it either can return a result or needs to apply one of its formal parameters as a function. The natural numbers index the formal parameters in the order that they were applied. Computations have an "evaluation strategy" baked into them, so there is a natural order. You start with a 0-computation, and you might get back a 1-computation. This is conceptually a function closed over the first parameter, but all such bookkeeping is left to the environment. For example:

id x = x
idComp = Parameter 0

const x y = x
constComp = Computation (Parameter 0)

apply f x = f x
applyComp = Computation (Apply 0 (Parameter 1))

A closed term in the untyped lambda calculus would have an associated 0-computation. There are uncountably many 0-computations, though, so it's not anything like a correspondence (and thus, despite the name I've chosen, most 0-computations are uncomputable).

That's not as clear as I'd like, but hopefully it will do. Anyone have a name for these things?

In recent weeks the volume of new spammer accounts has grown considerably. These accounts are sometimes used to post spam messages to the discussion group, but more often are simply used to game google by including spam urls in the user profile.

Due to the high volume of new spammer accounts I have implemented a new policy regarding new accounts. Given how things play out, it may become permanent:

1. New accounts are bocked by default, until released by an administrator. The user receives an email explaining this. While blocked, the user profile is invisible to anyone but the site administrators. They are also, of course, unable to sign in.

2. Accounts that seem legitimate, are released, while accounts that are clearly spam (e.g., from know spammers, include spam urls) are either deleted or put in the spammer category.

3. Accounts that we can't be sure about may be put in the "on probation" category. Members of this class can post, but their posts will appear only after being reviewed by an administrator. If the user turns out to be legitimate, it will be moved to the regular category, allowing the member to post directly.

4. Note that the "on probation" category is also used for members who are not spammers, but are considered or tend to post messages that are off topic. The messages posted by users that are on probation are in general reviewed by me before being allowed to appear.

New users are advised that by putting a short sentence or two about their specific interests relating to PL in their user profile, they will help us allow them to post sooner.

Paul McJones has been curating ALGOL section of Software Preservation Group. He notes:

I recently created an ALGOL section at the Computer History Museum’s Software Preservation Group web site, covering the language standardization efforts — for ALGOL 58 (also known as the International Algebraic Language), ALGOL 60, and ALGOL 68 — and also covering many implementations, dialects, and offshoots, complete with source code, manuals, and papers for many of these. The history of ALGOL has attracted many writers, and the final section of the web site links to many of their papers.

Also see his follow up blog about Whetstone ALGOL.