3 ms·

I'm interested what you mean by [1]. The rigorous part of Church's Thesis says exactly that the set of LC-computable, TM-computable, and general recursive funct

by tel 11y ago

I'm interested what you mean by [1]. The rigorous part of Church's Thesis says exactly that the set of LC-computable, TM-computable, and general recursive functions (nat -> nat) are all identical. This is somewhat weaker that "express", sure, but I'm very curious what you are pointing at when you invoke that.

pron 11y ago
Parallel or is a classic example. BTW, I'm not implying it's a severe limitation, it's just part of what I see as PFP valuing abstractions over algorithms which -- to my personal taste -- seems like misplaced priorities. The fact that you LC has no good ways of expressing computational complexity is a much bigger limitation, IMO, and another symptom of the same prioritization.
- catnaroek 11y ago
  Once you have fixed an evaluation strategy, you can talk about time complexity just fine. And, with a substructural type system, you can also talk about space complexity just fine. So it's not abstraction vs. algorithms. The lambda calculus gives you both.
  - pron 11y ago
    You're probably right -- I don't have the tools to argue with you -- but you know, as an algorithms person I view this whole abstraction discussion as revolving around UI. To me, UI should be intuitive and never get in your way. I'm appalled to think that I need to spend time learning what a substructural type system is in order to analyze the complexity of my algorithms. I can verify the correctness of my algorithms just fine (to the extent I need them verified, which usually isn't that much, at least not upfront), and so far I have seen zero evidence to support the claim that PFP makes developing software any cheaper. But I see more and more concepts going into abstractions and CH verification that I just can't see the justification for such mental overload standing between me and my algorithms. I'm perfectly happy with a model checker in the very rare cases I need one, and it doesn't require any substructural type systems, or even changing my choice of programming language (there are model checkers that work at the Java bytecode level and verify any program targeting the JVM regardless of the language).
- 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

Parallel or is a classic example. BTW, I'm not implying it's a severe limitation, it's just part of what I see as PFP valuing abstractions over algorithms which -- to my personal taste -- seems like misplaced priorities. The fact that you LC has no good ways of expressing computational complexity is a much bigger limitation, IMO, and another symptom of the same prioritization.

catnaroek 11y ago
Once you have fixed an evaluation strategy, you can talk about time complexity just fine. And, with a substructural type system, you can also talk about space complexity just fine. So it's not abstraction vs. algorithms. The lambda calculus gives you both.
- pron 11y ago
  You're probably right -- I don't have the tools to argue with you -- but you know, as an algorithms person I view this whole abstraction discussion as revolving around UI. To me, UI should be intuitive and never get in your way. I'm appalled to think that I need to spend time learning what a substructural type system is in order to analyze the complexity of my algorithms. I can verify the correctness of my algorithms just fine (to the extent I need them verified, which usually isn't that much, at least not upfront), and so far I have seen zero evidence to support the claim that PFP makes developing software any cheaper. But I see more and more concepts going into abstractions and CH verification that I just can't see the justification for such mental overload standing between me and my algorithms. I'm perfectly happy with a model checker in the very rare cases I need one, and it doesn't require any substructural type systems, or even changing my choice of programming language (there are model checkers that work at the Java bytecode level and verify any program targeting the JVM regardless of the language).
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.