bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

Chapter 3: (another) note on note #34

Closed nbloomf closed 6 years ago

nbloomf commented 6 years ago

Extremely minor quibble re. this footnote:

A Turing machine can express any algorithm.

This is only really true since we usually define an algorithm to be that which is computable by a turing machine or an equivalent model. It makes sense to talk about algorithms that run on turing machines with oracles attached, but these may not be computable by a turing machine alone.

I'd express this more like:

"A Turing machine is a very simple abstract machine designed to capture our intuitive understanding of computation in the most general sense. Any formal system that can simulate a Turing machine, and thus also perform arbitrary computations, is called Turing complete. (Untyped) Lambda calculus is Turing complete."