8
$\begingroup$

Currently, our ToC (Theory of Computation) courses are designed with the following progression of topics:

  1. Finite automata and regular languages
  2. Pushdown automata and context-free languages
  3. Turing Machines
  4. Undecidability and TMs
  5. Complexity classes (P, NP etc.)

If one were to redesign the ToC course where TMs in #3 and #4 above would be replaced by $\lambda$-calculus how would the rest of the course look like? That is, what would we teach in place of #1 & #2 above to progressively lead to $\lambda$-calculus? Also, could there really be chapter on complexity classes with $\lambda$-calculus as THE model of computation?

Improve this question
$\endgroup$
8
  • 5
    $\begingroup$ This is not a very well posed question, but I'd recommend reading Bob Harper's blog where he describes something similar: existentialtype.wordpress.com/2014/09/28/… $\endgroup$
    – Andrej Bauer
    Feb 22, 2015 at 22:37
  • $\begingroup$ @AndrejBauer - I understand. My reason to ask this question was, that when trying to understand the "why" behind lambda-calculus (LC), one visits the lands of intuitionistic logic, combinatory logic, type theory and the like. I wanted to know that if one were to truly understand LC and the connection with math and computing, where should one start, w.r.t. to the origin of the various "logic" concepts that actually led the creation of LC. $\endgroup$
    – PhD
    Feb 22, 2015 at 23:39
  • 4
    $\begingroup$ I agree with Andrej. I think you post too many open ended posts which are not really answerable specific questions but solicitations of opinion and invitations for discussion. I think that is not a good use of the site. I would suggest posting them on your blog or Google+. $\endgroup$
    – Kaveh
    Feb 23, 2015 at 0:54
  • 2
    $\begingroup$ The structure of courses you mention is natural within a machine and formal language-centric view of computation. Other perspectives on computation lead to other topics. For example, Dana Scott taught Recursion Theory in Stanford a couple of years ago. He covered, in this order, primitive recursive functions, computable enumeration, lambda calculus and Church numerals, universality and connection to Turing-, Minsky- and other machines. Then, he covered type theory and logic, building up to dependent types, and modal and intuitionistic logic. $\endgroup$
    – Vijay D
    Feb 23, 2015 at 2:31
  • 1
    $\begingroup$ @PhD Unfortunately I could not find a course page, even before posting the comment. I asked Prof. Scott for his notes. He is trying to locate them but is busy, so it will take some time. $\endgroup$
    – Vijay D
    Feb 23, 2015 at 17:15

2 Answers 2

Reset to default
5
$\begingroup$

The kind of approach to theory of computation you describe is what I like to call an abstract machine based computability theory: i.e. a theory that define computable functions/languages/etc via some abstract kind of machine (automata, linear automata, Turing machine etc).

An approach that uses $\lambda$-calculus instead of Turing machines could be thought as an expressions based computability theory: i.e. a theory where one prescribe some basic operations which are intuitively calculable and some operators defined between them to build other computable operations.

In this expression based computability theory

  • regular expressions correspond to finite state automata;
  • linear and context free grammar correspond to pushdown automaton and linear bounded automaton
  • (untyped) $\lambda$-calculus correspond to Turing machines
  • I don't know very much about complexity in $\lambda$-calculus but I guess it could be approached as done for complexity of $\mu$-recursive function or of logic formulas, classifying $\lambda$-terms in complexity classes by their structure (then of course it would be nice to compare these complexity classes with complexity classes for other models of computation, like Turing machines).

Hope this helps.

Improve this answer
$\endgroup$
1
$\begingroup$

There is a book by Neil Jones:

Computability and Complexity from a Programming Perspective

It uses Lisp S-exps as a more convenient -- from programmer perspective -- 'data-structure' than Gödel numbers and Turing encodings.

It also spends a significant number of pages on complexity. This is also unlike most other classical computability texts that are based on models other than the Turing model (eg Lambda-calculus)

Some paras from the preface..

A concrete connection between computability and programming languages: the dry-as-dust “s-m-n theorem” known in computability since the 1930s has proven its worth under the alias partial evaluation or program specialization.

...

The “universal machine,” is nothing but a self-interpreter, well-known in programming languages. Further, the “simulations” seen in introductory computability and complexity texts are mostly achieved by informal compilers or, sometimes, interpreters.

Do I recommend it??? Well... Depends on your appetite for heavy reading... [No its not easy 🙂 ]

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.