User loginNavigation |
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:
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 | 5193 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 5 days ago
16 weeks 6 days ago
16 weeks 6 days ago
39 weeks 7 hours ago
43 weeks 2 days ago
44 weeks 6 days ago
44 weeks 6 days ago
47 weeks 4 days ago
1 year 15 hours ago
1 year 17 hours ago