3 ms·

You mean lambda calculus? That model has plenty of shortcomings. Someone recently pinpointed the problem for me. Complexity analysis is impossible in a system t

You mean lambda calculus? That model has plenty of shortcomings. Someone recently pinpointed the problem for me. Complexity analysis is impossible in a system that is inherently unaware of time and computational cost of transition rules. Lambda calculus is inherently timeless (both in the theoretical sense because of turing equivalence and the practical sense of being unable to provide a proper framework for complexity analysis). See http://cstheory.stackexchange.com/questions/376/using-lambda-calculus-to-derive-time-complexity http://cstheory.stackexchange.com/questions/376/using-lambda....

jolux 10y ago
So you list one shortcoming, and don't even cover the position that lambda calculus is better suited as a foundation for a programming language despite not being better at time complexity than a Turing machine would be? http://cstheory.stackexchange.com/questions/21705/what-is-the-contribution-of-lambda-calculus-to-the-field-of-theory-of-computatio http://cstheory.stackexchange.com/questions/21705/what-is-th... My point is basically made here: This algebraic view of computation relates naturally to programming languages used in practise, and much language development can be understood as the search for, and investigation of novel program composition operators.
- dkarapetyan 10y ago
  This is the usual response. I didn't say the algebraic approach does not have advantages but the complexity analysis issue is always swept under the rug by proponents of the algebraic approach. Operational and axiomatic semantics also have their place and if the theoreticians haven't yet settled on "the one true way" why is it that regular programmers think they have? I agree that the search for novel composition mechanisms is a prominent goal of PL theory and research but it is not the only one.
  - jolux 10y ago
    Fair enough. I'll agree that their is no "one true way" and contest whether it's likely there is one, however I do think I understand the frustration some theoreticians have with the mainstream of programming when their contributions to programming language theory through denotational semantics, type theory, monads, etc have been largely ignored for the close to thirty years in favor of recycling the same tired dialects of Algol over and over again.
eru 10y ago
You can count your reduction steps in lambda calculus just fine. Can't you?
- cousin_it 10y ago
  If you want a foundation for computing, may I humbly suggest imperative algorithms in the integer RAM model. That gives correct answers to questions like "what's the time and space complexity of quicksort in the average and worst case?" Good luck answering that with lambda calculus, or Turing machines for that matter.
  - eru 10y ago
    The RAM model is nice for some simple space and runtime complexity analysis. Of course, it doesn't know about eg caches or parallelism, either. (Lambda calculus is an interesting foundation mostly for work on correctness of algorithms---indeed analysing cost of computations is harder. Chris Okasaki has done a good case study of analysing runtimes of purely functional algorithms / data structures.)
    - cousin_it 10y ago
      Can you use lambda calculus to prove the correctness of quicksort? :-)
      - eru 10y ago
        Depends on which version you are talking about. If you are happy to prove correctness of tree-sort, which does the same comparisons as quicksort, it's straight-forward. If you want to talk about the clever in-place quicksort, you'll want to talk about a slightly more complicated model. Either implicitly, where you still model everything as lambdas, or explicitly: you can model state (like an array) and its manipulation inside a lambda calculus framework just fine. Eg using linear typing, or something like Haskell's state monad (which has a pure description, but ghc is smart enough to optimize it to what you would expect when translating to machine code).

jolux 10y ago

So you list one shortcoming, and don't even cover the position that lambda calculus is better suited as a foundation for a programming language despite not being better at time complexity than a Turing machine would be? http://cstheory.stackexchange.com/questions/21705/what-is-the-contribution-of-lambda-calculus-to-the-field-of-theory-of-computatio http://cstheory.stackexchange.com/questions/21705/what-is-th... My point is basically made here: This algebraic view of computation relates naturally to programming languages used in practise, and much language development can be understood as the search for, and investigation of novel program composition operators.

dkarapetyan 10y ago
This is the usual response. I didn't say the algebraic approach does not have advantages but the complexity analysis issue is always swept under the rug by proponents of the algebraic approach. Operational and axiomatic semantics also have their place and if the theoreticians haven't yet settled on "the one true way" why is it that regular programmers think they have? I agree that the search for novel composition mechanisms is a prominent goal of PL theory and research but it is not the only one.
- jolux 10y ago
  Fair enough. I'll agree that their is no "one true way" and contest whether it's likely there is one, however I do think I understand the frustration some theoreticians have with the mainstream of programming when their contributions to programming language theory through denotational semantics, type theory, monads, etc have been largely ignored for the close to thirty years in favor of recycling the same tired dialects of Algol over and over again.

eru 10y ago

You can count your reduction steps in lambda calculus just fine. Can't you?

cousin_it 10y ago
If you want a foundation for computing, may I humbly suggest imperative algorithms in the integer RAM model. That gives correct answers to questions like "what's the time and space complexity of quicksort in the average and worst case?" Good luck answering that with lambda calculus, or Turing machines for that matter.
- eru 10y ago
  The RAM model is nice for some simple space and runtime complexity analysis. Of course, it doesn't know about eg caches or parallelism, either. (Lambda calculus is an interesting foundation mostly for work on correctness of algorithms---indeed analysing cost of computations is harder. Chris Okasaki has done a good case study of analysing runtimes of purely functional algorithms / data structures.)
  - cousin_it 10y ago
    Can you use lambda calculus to prove the correctness of quicksort? :-)
    - eru 10y ago
      Depends on which version you are talking about. If you are happy to prove correctness of tree-sort, which does the same comparisons as quicksort, it's straight-forward. If you want to talk about the clever in-place quicksort, you'll want to talk about a slightly more complicated model. Either implicitly, where you still model everything as lambdas, or explicitly: you can model state (like an array) and its manipulation inside a lambda calculus framework just fine. Eg using linear typing, or something like Haskell's state monad (which has a pure description, but ghc is smart enough to optimize it to what you would expect when translating to machine code).