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 ncomputation as infinite data (in pseudosyntax): 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 0computation, and you might get back a 1computation. 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 0computation. There are uncountably many 0computations, though, so it's not anything like a correspondence (and thus, despite the name I've chosen, most 0computations 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 20100517 03:44  LtU Forum  previous forum topic  next forum topic  other blogs  4059 reads

Browse archives
Active forum topicsNew forum topics 
Recent comments
1 week 3 days ago
1 week 5 days ago
1 week 5 days ago
1 week 6 days ago
1 week 6 days ago
1 week 6 days ago
2 weeks 1 hour ago
2 weeks 8 hours ago
2 weeks 17 hours ago
3 weeks 1 day ago