Skip to content

Commit a06deb3

Browse files
committed
where is it used?
1 parent 98e1f26 commit a06deb3

43 files changed

Lines changed: 341 additions & 871 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
16 KB
Binary file not shown.
684 Bytes
Binary file not shown.
-2.91 KB
Binary file not shown.
517 Bytes
Binary file not shown.
1.29 KB
Binary file not shown.
1.46 KB
Binary file not shown.
191 Bytes
Binary file not shown.
1.5 KB
Binary file not shown.

booksource/_build/html/_sources/index.md

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
11
# Invitation to Computability
22

3+
Lawrence S. Moss
4+
35
This is a textbook on the basics of computability theory, originating in classes given by the author
46
at Indiana University for quite a few years. My students are mainly graduate students in either mathematics or computer science, always with a few undergraduates and a few grad students from philosophy and other disciplines.
57

6-
In some ways, the content of the book is standard, and in some ways it is not. It treats the basic topics of the subject: the concept of computability, primitive recursion, mu-recursion, universal functions, the Recursion Theorem, and undecidability in computability theory, mathematics, and logic. Of course we are living decades past the original proofs of these results, and so the presentation here will differ. This book will try to make pointers to many of the developments in computability theory and computer science that have come from the classical material.
8+
In some ways, the content of the book is standard, and in some ways it is not. It introduces the basic topics of the subject: the concept of computability, primitive recursion, mu-recursion, universal functions, the Recursion Theorem, relative computability, the arithmetic hierarchy, and undecidability in computability theory, mathematics, and logic. Of course we are living decades past the original results on these topics, and so the presentation here will differ. This book will try to make pointers to many of the developments in computability theory and computer science that have come from the classical material.
79

810
## Why a Jupyter book?
911

@@ -13,42 +15,42 @@ book about computation theory should use up-to-date computational tools. This bo
1315
packages, Jupyter notebooks and everything needed to work with them, $\LaTeX$, github, and more. In the
1416
course of working on the book I became interested in using all of these computational artifacts, mainly as a
1517
way of seeing what would work in a textbook, and what would not. Since working in this medium is new to me
16-
(and pretty much everyone), I became as interested in those aspects of the project as in the content. Here are some of artifacts found here but not in a traditional book on computability theory: a executable Python code, especially in the beginning chapters; a variety of pictures and charts; the ability to hide technical passages and to otherwise structure a text; and clickable references to discussions, papers,
18+
(and pretty much everyone), I became as interested in those aspects of the project as in the content. Here are some of artifacts found here but not in a traditional book on computability theory: a executable Python code, especially in several chapters near the beginning; a variety of pictures and charts; the ability to hide technical passages and to otherwise structure a text; and clickable references to discussions, papers,
1719
[and even poems](http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html), both inside and outside of the book itself. In time I will consider adding animations to illustrate some of the dynamism that I sense with computably enumerable sets which is arrested in any print presentation. I also would like to incorporate tools for readers to annotate and discuss matters, enabling a community of readers. In short, I am aiming for something which is both a short textbook and an intellectual version of a coffee-table book.
1820

1921
# Intended audience
2022

2123
This book is aimed at anyone who frequently encounters the very basic parts of computability theory and has the needed mathematical background to read it. That background is a working familiarity with mathematical notation and discourse. One should know how to read mathematics. This would be the wrong place to learn basic abstract mathematics; the pace and level would be too much. But if you can read mathematics, that is enough: nothing else is really assumed. There are places where it would be good to have seen some induction on the natural numbers and even some basic topics in areas like logic, set theory, and computer programming. But one could do without the background, I think. And I hope to have provided enough background on those topics to make what is here accessible.
2224

23-
Some of the people who will benefit from the book: those in the broad area of interdisciplinary logic but who are not specialists in computability theory per se; computer scientists in areas like programming languages and theory of computation; philosophers interested in areas like the philosophy of logic or philosophy of mathematics. For others, such as those pursuing any area of mathematics, the subject will probably be an "extra". But "extras" are important, too. I really have in mind a broad audience of people who might find the topics here intersting.
25+
Some of the people who will benefit from the book: those in the broad area of interdisciplinary logic but who are not specialists in computability theory per se; computer scientists in areas like programming languages and theory of computation; philosophers interested in areas like the philosophy of logic or philosophy of mathematics. For others, such as those pursuing any area of mathematics, especially areas that might be far from computability theory, the subject will probably be an "extra". But "extras" are important, too. Summing up: I have in mind a broad audience of people who might find the topics of the book intersting.
2426

2527
(content:DistinctiveFeatures)=
2628
# Distinctive features
2729

28-
The are three distinctive features of the book. Theree of the first four chapters are mainly an online resource. For this part of the book, this more important than the printed book. Most of the chapters in that part of the book are Jupyter notebooks. Rather than simply read, these chapters are intended to be *run* and *programmed*. One way to use them is to save them and then run them locally. Alternatively, one could open them on a hosting service like CoCalc, Binder, or Google Colab. The Jupyter book format is not so important for the material that comes after the first sections, and for those a traditional print book is going to be available.
30+
The are three distinctive features of this book. Three of the first four chapters are mainly an online resource. For them, this more important than the printed book. Most of the chapters in that part of the book are Jupyter notebooks. Rather than simply read, these chapters are intended to be *run* and *programmed*. One way to use them is to save them and then run them locally. Alternatively, one could open them on a hosting service like CoCalc, Binder, or Google Colab. The Jupyter book format is not so important for the material that comes after the first sections, and for those a traditional print book is going to be available.
2931

3032

3133
## Text register machines
3234

3335
Compared to the many other books on the subject, the treatment here is in some ways more concrete and in some ways more abstract and sophisticated. How can this be? It is more concrete in the beginning than other books, and more abstract later on. It is more concrete in that it comes with a dedicated computer implementation and because it goes into full details on coding. But later it is more abstract because it discusses matters like recursion on induction on a fairly abstract level and because it also discusses corecursion alongside recursion.
3436

35-
The concrete part in the beginning develops a model of computation which is a variant of a register machine called a *text register machine*. The "text" in "text register machine" is the feature (orignal here) that the programming language of the machine is the same as the language of programs. This language the set of words on the two letter alphabet ```{1,#}```. So the language is called ```1#```. This text comes with two interpreters for ```1#```, so the programs can be run. The programs themselves are unreadable; that is, they are not intended to be human readable but rather to be used in this presentation of computabililty (and nowhere else). The book comes with tool support to help people to write long programs in ```1#```; for example, one can turn a flowchart into a ```1#``` program. Another tool turns a decription of a primitive recursive function into ```1#``` code. Those tools are in Python, and while one need not read the programs to use them, a class for computer science students could indeed do so. Using ```1#``` and the accompanying tools, the main first theorems of computability theory are presented constructively in full detail, with no coding and no hand-waving. One can write explicit universal programs, $s^m_n$ programs, self-writing programs, the T-predicate, and similar artifacts that essentially *are* the main first results in computability theory. One can prove Kleene's Second Recursion Theorem in full detail, too.
37+
The concrete part in the beginning develops a model of computation which is a variant of a register machine called a *text register machine*. The "text" in "text register machine" is the feature that the programming language of the machine is the same as the language of programs. This language the set of words on the two letter alphabet ```{1,#}```. So the language is called ```1#```. This text comes with two interpreters for ```1#```, so the programs can be run. The programs themselves are unreadable; that is, they are not intended to be human readable but rather to be used in this presentation of computabililty (and nowhere else). The book comes with tool support to help people to write long programs in ```1#```; for example, one can turn a flowchart into a ```1#``` program. Another tool turns a decription of a primitive recursive function into ```1#``` code. Those tools are in Python, and while one need not read the programs to use them, a class for computer science students could indeed do so. Using ```1#``` and the accompanying tools, the main first theorems of computability theory are presented constructively in full detail, with no coding and no hand-waving. One can write explicit universal programs, $s^m_n$ programs, self-writing programs, the T-predicate, and similar artifacts that essentially *are* the main first results in computability theory. One can prove Kleene's Second Recursion Theorem in full detail, too.
3638

3739

38-
The use of ```1#``` is why the treatment here is much more explicit than usual. The way the book works is that those main first results are presented in full detail, and then after doing so it becomes more "hand wavy". Probably every book on the topic is going becomes "hand wavy" at some point. But this one does so much later, due to our use of ```1#``` and the extra tools.
40+
The use of ```1#``` is why the treatment here is much more explicit than usual. The way the book works is that those main first results are presented in full detail, and then after doing so it becomes more "hand wavy". Probably every book on the topic becomes "hand wavy" at some point. But this one does fairly late, due to our use of ```1#``` and the extra tools.
3941

4042
## Unsolvable problems
4143

42-
The book also presents quite a bit on undecidability matters and the main negative results of 20th century mathematical logic such as Church's Theorem that satisfiability in first-order logic is undecidable. In this, we use other interesting undecidability results such as tiling and also matrix mortality. Our treatment is fuller than any source we know of on these topics. The reason that we can provide a full treatment is that we build on work done with ```1#``` earlier. For example, the work done in writing the universal program gets called back when we prove the undecidability of tiling, and the undecidability of tiling leads to a fairly easy proof of Church's Theorem.
44+
The book also presents quite a bit on undecidability matters and the main negative results of 20th century mathematical logic such as the Church-Turing Theorem (satisfiability in first-order logic is undecidable). In this, we use other interesting undecidability results such as tiling and also matrix mortality. Our treatment is fuller than any source we know of on these topics. The reason that we can provide a full treatment is that we build on work done with ```1#``` earlier. For example, the work done in writing the universal program gets called back when we prove the undecidability of tiling, and the undecidability of tiling leads to a fairly easy proof of Church's Theorem.
4345

4446

45-
## Recursion principles and the categorical treament of recursion
47+
## Recursion principles and the categorical treatment of recursion
4648

4749
Another way to make the point about the book being both more concrete and also more sophisticated: the text goes into details about coding in a fair amount of detail -- much more so than usual, since we can illustrate much of the coding work using actual programs. But at the same time it discusses the overall issues of coding in an abstract way, using ideas originating in abstract data types.
4850

4951
We include pointers to, and digressions on, topics such as recursion principles in very general settings, combinatory logic, and term rewriting. For example, we discuss recursion on well-founded well-ordered sets. This all comes in the second part of the book. That part demands more mathematical maturity than the concrete work. But the book is also designed so that the first part provides some help to students at beginning levels.
5052

51-
The final distinctive feature of the book is a "gentle introduction" to areas of theoretical computer science related to *algebra* and *coalgebra*. The goal here is to understand Lawvere's point that ordinary recursion on the natural numbers is equivalent to the initiality of the the natural numbers in a certain category. Doing this leads to a deeper understanding of the relation of recursion and induction. So all of this is presented from scratch. The payoff comes when we "turn the arrows around" to see corecursion and bisimulation, matching recursion and induction. These are not traditional topics for an introductory course on this subject, but I no reason why they would not be. And for my intended audicence, they make more sense than the traditional topics which I have chosen to omit, such as oracle computation, c.e. sets and priority arguments, and complexity theory. These all are the main focus topics of other textbooks and do not fit with what I am trying to do here.
53+
The final distinctive feature of the book is a "gentle introduction" to areas of theoretical computer science related to *algebra* and *coalgebra*. The goal here is to understand the point that ordinary recursion on the natural numbers is equivalent to the initiality of the natural numbers in a certain category. Doing this leads to a deeper understanding of the relation of recursion and induction. So all of this is presented from scratch. The payoff comes when we "turn the arrows around" to see corecursion and bisimulation, matching recursion and induction. These are not traditional topics for an introductory course on this subject, but I no reason why they would not be. And for my intended audience, they make more sense than the traditional topics which I have chosen to omit, such as oracle computation, c.e. sets and priority arguments, and complexity theory. These all are the main focus topics of other textbooks and do not fit with what I am trying to do here.
5254

5355
# Using it in a classroom or for self-study
5456

booksource/_build/html/_sources/introOneSharp/functions.ipynb

Lines changed: 5 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -26,28 +26,10 @@
2626
"id": "kagQ3xd6nzIL"
2727
},
2828
"source": [
29-
"\n",
30-
"At this point we know what programs of ```1#``` are and how they work.\n",
29+
"At this point [we know what programs of ```1#``` are and how they work](content:whatArePrograms).\n",
3130
"We are interested not just in the programs themselves\n",
3231
"but in *what* they compute. \n",
3332
"\n",
34-
"We call the set ```{1,#}``` our *alphabet*, and we use the letter $A$ for it.\n",
35-
"\n",
36-
"\n",
37-
"We know that it is odd to call such a small set an \"alphabet\",\n",
38-
"even more so when that set doesn't have any letters in it!\n",
39-
"But this usage is standard, and so we'll adopt it.\n",
40-
"When used in situations like ours, the word \"alphabet\"\n",
41-
"just means a set that you use to build words from. \n",
42-
"\n",
43-
"But if ```{1,#}``` is our alphabet, what in\n",
44-
"the world are our words?!\n",
45-
"\n",
46-
"Answer:\n",
47-
"A *word* is just a sequence of symbols from our alphabet.\n",
48-
"\n",
49-
" Examples of words include \n",
50-
"```11#11####``` and also the empty word $\\varepsilon$.\n",
5133
"\n",
5234
" \n",
5335
"Let us be clear about the difference between\n",
@@ -57,15 +39,6 @@
5739
"in programs. \n",
5840
" \n",
5941
"\n",
60-
" \n",
61-
"A *program* of ```1#``` is just a sequence of\n",
62-
"instructions, \n",
63-
"run together to make a big word.\n",
64-
"An instruction counts as a program, \n",
65-
"but programs of length $\\geq 2$ are not instructions.\n",
66-
"\n",
67-
"\n",
68-
"\n",
6942
"```{prf:definition}\n",
7043
":label: phi-notation\n",
7144
"Every word $p$ gives us a function\n",
@@ -149,7 +122,7 @@
149122
"id": "ZhaXDhZfFra5"
150123
},
151124
"source": [
152-
"# Partial functions\n",
125+
"## Partial functions\n",
153126
"\n",
154127
"Suppose we run a program $p$ with an input word $x$ in R1 and all other registers empty. This run might, or might not, halt. The first example of this is when $p$ is a loop $\\one\\hash^3\\one\\hash^4$. For this program $p$, $\\phifn_p(x)$ is *undefined* for all $x$.\n",
155128
" \n",
@@ -247,7 +220,7 @@
247220
"id": "PQzllCr-Fu2y"
248221
},
249222
"source": [
250-
"# Functions of two or more arguments\n",
223+
"## Functions of two or more arguments\n",
251224
"\n",
252225
"A program $p$ of ```1#``` can also be used as a function of zero or more arguments. Here is the relevant definition.\n",
253226
"\n",
@@ -388,7 +361,7 @@
388361
"id": "WOy1_0mpgsJ9"
389362
},
390363
"source": [
391-
"# Functions of zero inputs\n",
364+
"## Functions of zero inputs\n",
392365
"\n",
393366
"We started by associating to each program $p$ a function $\\phifn_p$ of one argument, and then for each $n \\geq 2$ we associated a function $\\phifn_p^n$ of $n$ arguments. This general definition works in case $n = 0$ also. "
394367
]
@@ -611,8 +584,7 @@
611584
"\n",
612585
"For example, ```1###``` and ```1###1###``` are not equal, but they are strongly equivalent (and thus equivalent as one-place functions).\n",
613586
"\n",
614-
"For an example of programs $p$ and $q$ which are equivalent as one-place functions but not strongly equivalent, let $p$ be ```1#```, and let $q$ be ```clear_2 + 1#```.\n",
615-
"Running $q$ when R1 and R2 both have ```1``` results in a halting computation where R1 has ```11``` and R2 is empty. But running $p$ this way preserves R2.\n",
587+
"For an example of programs $p$ and $q$ which are equivalent as one-place functions but not strongly equivalent, let $p$ be ```1#```, and let $q$ be ```clear_2 + 1#```. Running $q$ when R1 and R2 both have ```1``` results in a halting computation where R1 has ```11``` and R2 is empty. But running $p$ this way preserves R2.\n",
616588
"\n"
617589
]
618590
}

0 commit comments

Comments
 (0)