Skip to main content
Taking into account Raphael's comment comment
Source Link
jmad
  • 9.5k
  • 1
  • 39
  • 42

As far as I know, the main models of computability are λ-calculus, Turing machines and recursive functions. I am not aware of the situation regarding complexity in recursive functions, they may or may not be useless for complexity.

It may be seen as a fortunate coincidence that Turing machines, which are not so arguably very inefficient machines, are also a very good model of complexity. What made things natural is that there are a lot of transformations involving TMs that are polynomial. (Universal machine, simulation of a $n$-taped machine with a 1-taped machine, from an arbitrary alphabet to a binary one, simulating a PRAM, ...) and that polynomials are a class of functions stable by arithmetic operations and composition – which makes them a good candidate for complexity theory.

Pure λ-calculus was in itself useless for complexity. However a simple type system came into play and allowed guarantees of termination for some λ-terms in a very easy way. Then some other systems (systems T, F, ..) allowed a great expressiveness while keeping termination.

Efficiency or complexity being a refinement of termination and types being closely related to logic, later came light linear logics which characterizes several classes of complexity. (Elementary, P, and some variations for PSPACE and others). The research in this domain is very active and is not restricted to these complexity classes, and is not even restricted to the λ-calculus.

tl;dr: λ-calculus was useful for computability, termination and complexity theory.

However to give credit where credit is due Turing machines are a good and unanimous way to define what is complexity, but that's true only for loose bounds like "polynomial", not for tight bounds for which PRAM-like models are more suitable.

As far as I know, the main models of computability are λ-calculus, Turing machines and recursive functions. I am not aware of the situation regarding complexity in recursive functions, they may or may not be useless for complexity.

It may be seen as a fortunate coincidence that Turing machines, which are not so arguably very inefficient machines, are also a very good model of complexity. What made things natural is that there are a lot of transformations involving TMs that are polynomial. (Universal machine, simulation of a $n$-taped machine with a 1-taped machine, from an arbitrary alphabet to a binary one, simulating a PRAM, ...) and that polynomials are a class of functions stable by arithmetic operations and composition – which makes them a good candidate for complexity theory.

Pure λ-calculus was in itself useless for complexity. However a simple type system came into play and allowed guarantees of termination for some λ-terms in a very easy way. Then some other systems (systems T, F, ..) allowed a great expressiveness while keeping termination.

Efficiency or complexity being a refinement of termination and types being closely related to logic, later came light linear logics which characterizes several classes of complexity. (Elementary, P, and some variations for PSPACE and others). The research in this domain is very active and is not restricted to these complexity classes, and is not even restricted to the λ-calculus.

tl;dr: λ-calculus was useful for computability, termination and complexity theory.

However to give credit where credit is due Turing machines are a good and unanimous way to define what is complexity.

As far as I know, the main models of computability are λ-calculus, Turing machines and recursive functions. I am not aware of the situation regarding complexity in recursive functions, they may or may not be useless for complexity.

It may be seen as a fortunate coincidence that Turing machines, which are not so arguably very inefficient machines, are also a very good model of complexity. What made things natural is that there are a lot of transformations involving TMs that are polynomial. (Universal machine, simulation of a $n$-taped machine with a 1-taped machine, from an arbitrary alphabet to a binary one, simulating a PRAM, ...) and that polynomials are a class of functions stable by arithmetic operations and composition – which makes them a good candidate for complexity theory.

Pure λ-calculus was in itself useless for complexity. However a simple type system came into play and allowed guarantees of termination for some λ-terms in a very easy way. Then some other systems (systems T, F, ..) allowed a great expressiveness while keeping termination.

Efficiency or complexity being a refinement of termination and types being closely related to logic, later came light linear logics which characterizes several classes of complexity. (Elementary, P, and some variations for PSPACE and others). The research in this domain is very active and is not restricted to these complexity classes, and is not even restricted to the λ-calculus.

tl;dr: λ-calculus was useful for computability, termination and complexity theory.

However to give credit where credit is due Turing machines are a good and unanimous way to define what is complexity, but that's true only for loose bounds like "polynomial", not for tight bounds for which PRAM-like models are more suitable.

Source Link
jmad
  • 9.5k
  • 1
  • 39
  • 42

As far as I know, the main models of computability are λ-calculus, Turing machines and recursive functions. I am not aware of the situation regarding complexity in recursive functions, they may or may not be useless for complexity.

It may be seen as a fortunate coincidence that Turing machines, which are not so arguably very inefficient machines, are also a very good model of complexity. What made things natural is that there are a lot of transformations involving TMs that are polynomial. (Universal machine, simulation of a $n$-taped machine with a 1-taped machine, from an arbitrary alphabet to a binary one, simulating a PRAM, ...) and that polynomials are a class of functions stable by arithmetic operations and composition – which makes them a good candidate for complexity theory.

Pure λ-calculus was in itself useless for complexity. However a simple type system came into play and allowed guarantees of termination for some λ-terms in a very easy way. Then some other systems (systems T, F, ..) allowed a great expressiveness while keeping termination.

Efficiency or complexity being a refinement of termination and types being closely related to logic, later came light linear logics which characterizes several classes of complexity. (Elementary, P, and some variations for PSPACE and others). The research in this domain is very active and is not restricted to these complexity classes, and is not even restricted to the λ-calculus.

tl;dr: λ-calculus was useful for computability, termination and complexity theory.

However to give credit where credit is due Turing machines are a good and unanimous way to define what is complexity.