Home » forums » LtU Forum

What's the name for this model of computation?

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?

By Matt M at 2010-05-17 03:44 | LtU Forum | previous forum topic | next forum topic | other blogs | 5118 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Two questions

  1. How do you define the S combinator as an 0-computation?
  2. How do you get uncountably many 0-computations? It looks like you've defined them using a simple context-sensitive grammar.
By Charles Stewart at Mon, 2010-05-17 08:31 | login or register to post comments

Thank you

You're right - I'm missing a case. Checking that I can express SK before posting probably would have been a good idea. I think fix is to make Apply take a (potentially infinite) list of computations to apply. I notice now that there's also a (small, I think) problem with the way I overload "computation" to be both a lambda or a redex.

Despite the flaws, I'm still hoping someone will recognize what I want. The main feature I want is that computations are defined by a sort of trace of what they do to their parameters, with internal sub-computations not exposed, so that two computations are equivalent only if they are equal as (infinite) data.

Regarding countability, consider this grammar:

data SubsetOfNats = In SubsetOfNats | Out SubsetOfNats

There are only countably many inhabitants if you restrict to the computable sequences.

By Matt M at Mon, 2010-05-17 13:23 | login or register to post comments

Countability of sets of computations

I'm still not really clear where your formalism is headed. But when you say two computations are equivalent only if they are equal as (infinite) data, this reminds me of Bohm trees for the untyped lambda calculus.


Regarding countability, consider this grammar:
data SubsetOfNats = In SubsetOfNats | Out SubsetOfNats

Is the idea that you can construct programs out of these sets? You can do a similar thing, with the same cardinality, using oracle Turing machines.

By Charles Stewart at Mon, 2010-05-17 18:11 | login or register to post comments

Bohm-like trees

Bingo. Thank you, Charles. It sounds like the objects I'm interested in are actually "Bohm-like trees". From Barendregt notes, here:

A Bohm-like tree A is an actual Bohm tree (of a lambda-K term) iff FV(A) is finite and A is r.e. One direction of this is easy to see, since every BT(M) has finitely many free variables and is r.e. The other direction is quite involved.

So, a Bohm tree is a Bohm-like tree that corresponds to a lambda (finite free variables and computable). That's exactly what I want. I'd guess (without overconfidence) that this would be equivalent to Turing machines with infinite programs. These things seem interesting to me because they capture the local properties of computations without imposing a global restriction on what's computable.

Thanks again

By Matt M at Mon, 2010-05-17 18:55 | login or register to post comments

It's called de Bruijn notation

Here's a nice paper about how to do this in Haskell:
www.comlab.ox.ac.uk/richard.bird/online/BirdPaterson99DeBruijn.pdf

By Sjoerd Visscher at Mon, 2010-05-17 10:00 | login or register to post comments

I'm familiar with de Bruijn

I'm familiar with de Bruijn notation, but don't think that's what I'm after. Maybe see my clarifying post to Charles for my goals.

By Matt M at Mon, 2010-05-17 13:25 | login or register to post comments