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

<p>An approach that uses $\lambda$-calculus instead of Turing machines could be thought as an <em>expressions based computability theory</em>:
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.</p>

<p>In this <em>expression based computability theory</em></p>

<ul>
<li>regular expressions correspond to finite state automata;                                                                             </li>
<li>linear and context free grammar correspond to pushdown automaton and linear bounded automaton</li>
<li>(untyped) $\lambda$-calculus correspond to Turing machines</li>
<li>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).</li>
</ul>

<p>Hope this helps.</p>

CC BY-SA 3.0
2015-02-23T15:08:12.710Z
2015-02-26T10:52:29.970Z
2015-02-26T10:52:29.970Z
Giorgio Mossa
<p>There is a book by Neil Jones:</p>

<p><a href="http://www.diku.dk/~neil/comp2book2007/book-whole.pdf" rel="nofollow">Computability and Complexity from a Programming Perspective</a></p>

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

<p>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)</p>

<p>Some paras from the preface..</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>...</p>

<blockquote>
  <p>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.</p>
</blockquote>

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

CC BY-SA 3.0
2015-10-13T16:20:43.867Z
2015-10-13T16:20:43.867Z
Rusi
<p>Currently, our ToC (Theory of Computation) courses are designed with the following progression of topics:</p>

<ol>
<li>Finite automata and regular languages</li>
<li>Pushdown automata and context-free languages</li>
<li>Turing Machines</li>
<li>Undecidability and TMs</li>
<li>Complexity classes (P, NP etc.)</li>
</ol>

<p>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 &amp; #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?</p>

CC BY-SA 3.0
2015-02-22T22:37:17.283Z
This is not a very well posed question, but I'd recommend reading Bob Harper's blog where he describes something similar: https://existentialtype.wordpress.com/2014/09/28/structure-and-efficiency-of-computer-programs/
Andrej Bauer
CC BY-SA 3.0
2015-02-22T23:39:48.717Z
@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.
PhD
CC BY-SA 3.0
2015-02-22T23:42:33.653Z
Also, give the current fascination with functional programming languages, not many people really tend to understand the "why" behind them. Most learn it 'mechanically' without almost ever connecting it with the "math" behind the "computing". Since TMs are mostly taught in schools and people learn imperative programming early on, the "lambda" thinking takes a back seat. But if someone wants to understand the math behind computing and functional programming, they ought to know LC. For which one needs to know quite a bit from a background perspective. Hence the question.
PhD
CC BY-SA 3.0
2015-02-22T23:44:08.887Z
I am still looking for a "holistic" tome on the subject that *covers it all* (at least at the introductory level). The closest one that I found so far is this paper: http://www.dbnet.ece.ntua.gr/~adamo/languages/books/p359-hudak.pdf Hence I framed the question from a 'textbook' layout perspective - but I wanted to know what all does one need to understand to appreciate what LC (and by consequence functional programming) has to offer.
PhD
CC BY-SA 3.0
2015-02-23T00:54:14.280Z
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+.
Kaveh
CC BY-SA 3.0
2015-02-23T02:31:30.077Z
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.
Vijay D
CC BY-SA 3.0
2015-02-23T08:22:40.293Z
@VijayD Any link for that class?
PhD
CC BY-SA 3.0
2015-02-23T17:15:18.167Z
@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.
Vijay D
<soft-question><big-list><big-picture><lambda-calculus><teaching>
How would a theory of computation course that culminated in lambda-calculus as "the" model of computation, instead of Turing machines, look like?
PhD
# How would a theory of computation course that culminated in lambda-calculus as "the" model of computation, instead of Turing machines, look like?

(Asked by: username_0 on 2015-02-22)

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?

**Tags:** soft-question, big-list, big-picture, lambda-calculus, teaching
> **Comments:**
> **username_1**: This is not a very well posed question, but I'd recommend reading Bob Harper's blog where he describes something similar: https://existentialtype.wordpress.com/2014/09/28/structure-and-efficiency-of-computer-programs/  
> **username_0**: @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.  
> **username_0**: Also, give the current fascination with functional programming languages, not many people really tend to understand the "why" behind them. Most learn it 'mechanically' without almost ever connecting it with the "math" behind the "computing". Since TMs are mostly taught in schools and people learn imperative programming early on, the "lambda" thinking takes a back seat. But if someone wants to understand the math behind computing and functional programming, they ought to know LC. For which one needs to know quite a bit from a background perspective. Hence the question.  
> **username_0**: I am still looking for a "holistic" tome on the subject that *covers it all* (at least at the introductory level). The closest one that I found so far is this paper: http://www.dbnet.ece.ntua.gr/~adamo/languages/books/p359-hudak.pdf Hence I framed the question from a 'textbook' layout perspective - but I wanted to know what all does one need to understand to appreciate what LC (and by consequence functional programming) has to offer.  
> **username_2**: 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+.  
> **username_3**: 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.  
> **username_0**: @VijayD Any link for that class?  
> **username_3**: @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.  

---

## 2 answers

### Answer by username_4 on 2015-02-23. Score: 5

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.


---

### Answer by username_5 on 2015-10-13. Score: 1

There is a book by Neil Jones:

[Computability and Complexity from a Programming Perspective](http://www.diku.dk/~neil/comp2book2007/book-whole.pdf)

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 ]


---

