4 ms·

I'm curious to see how parallel or is implemented on a TM. It's not a function from (nat -> nat) of course since we're talking about something other than extens

by tel 11y ago

I'm curious to see how parallel or is implemented on a TM. It's not a function from (nat -> nat) of course since we're talking about something other than extensional equality... but even then I tend to find these things not terrifically far out of whack.

pron 11y ago
You're right, it's not a function nat -> nat because it depends on program representation. And it's implemented in a universal TM by dovetailing: running one instruction from one input program and then one instruction from the other program and so on back and forth until one of them terminates. Parallel or is important because it uncovers something interesting: LC works with high-order functions but it can't do high-order programs, namely representing the computation process itself as a first-class entity. LC is not introspective in that sense, and most of its limitations flow from that (including the difficulty describing complexity, which is a feature of the computation process, not of the functions). Again, I'm not well versed in PL theory (or hardly at all), but I think that Lisp's macros therefore actually make it strictly more powerful than LC[1] (I think I may have seen this mentioned somewhere). Indeed, macros have allowed Clojure to implement stackless continuations, and bytecode manipulation has allowed us to implement full continuations on the JVM without any JVM hacking. Similarly, this kind of direct computation representation allows all sorts of instrumentations and various interesting transformations that are not representable in LC proper (without macros). This isn't at all catastrophic -- you can live without those transformations -- but they can be very powerful and very useful. [1]: And by "strictly" I mean with direct representation rather than by simulating a TM.
- tel 11y ago
  Ah, yes. Generally you're right: on 2nd order functions ((nat -> nat) -> nat) TMs and LC differ where TM's have strictly more functionality. But then it flips again at 3rd order (((nat -> nat) -> nat) -> nat) and so on and so forth. Additionally, you can always just Gödel encode a program, pass it in, get all of this functionality. That might be considered cheating (simulating a TM, although you could just as well simulate LC in both models). This is not actually any different from what the UTM is doing... it's just possible to ignore the difference between interpretation and normal operation because it's all just tape.

by tel 11y ago

pron 11y ago

You're right, it's not a function nat -> nat because it depends on program representation. And it's implemented in a universal TM by dovetailing: running one instruction from one input program and then one instruction from the other program and so on back and forth until one of them terminates. Parallel or is important because it uncovers something interesting: LC works with high-order functions but it can't do high-order programs, namely representing the computation process itself as a first-class entity. LC is not introspective in that sense, and most of its limitations flow from that (including the difficulty describing complexity, which is a feature of the computation process, not of the functions). Again, I'm not well versed in PL theory (or hardly at all), but I think that Lisp's macros therefore actually make it strictly more powerful than LC[1] (I think I may have seen this mentioned somewhere). Indeed, macros have allowed Clojure to implement stackless continuations, and bytecode manipulation has allowed us to implement full continuations on the JVM without any JVM hacking. Similarly, this kind of direct computation representation allows all sorts of instrumentations and various interesting transformations that are not representable in LC proper (without macros). This isn't at all catastrophic -- you can live without those transformations -- but they can be very powerful and very useful. [1]: And by "strictly" I mean with direct representation rather than by simulating a TM.

tel 11y ago
Ah, yes. Generally you're right: on 2nd order functions ((nat -> nat) -> nat) TMs and LC differ where TM's have strictly more functionality. But then it flips again at 3rd order (((nat -> nat) -> nat) -> nat) and so on and so forth. Additionally, you can always just Gödel encode a program, pass it in, get all of this functionality. That might be considered cheating (simulating a TM, although you could just as well simulate LC in both models). This is not actually any different from what the UTM is doing... it's just possible to ignore the difference between interpretation and normal operation because it's all just tape.