Skip to content

Commit

Permalink
changed toc, added a file
Browse files Browse the repository at this point in the history
  • Loading branch information
lmoss committed Jan 6, 2025
1 parent 4207b2f commit feeab90
Show file tree
Hide file tree
Showing 29 changed files with 450 additions and 223 deletions.
Binary file modified _build/.doctrees/environment.pickle
Binary file not shown.
Binary file modified _build/.doctrees/index.doctree
Binary file not shown.
Binary file modified _build/.doctrees/introOneSharp/haltDef.doctree
Binary file not shown.
Binary file modified _build/.doctrees/introOneSharp/instructions.doctree
Binary file not shown.
51 changes: 4 additions & 47 deletions _build/html/_sources/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ at Indiana University for quite a few years. In some way, the content is standa
not. It treats the basic topics of the subject: the concept of computability, primitive recursion,
mu-recursion, universal functions, the Enumeration Theorem, 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, and we will try to make pointers to many of the
these results, and so the presentation here will differ, and this book will try to make pointers to many of the
developments in computability theory and computer science that have come from the clasical material.

We are also living in the wake of several revolutions in society coming from the advent of computers and the
Expand All @@ -32,59 +32,16 @@ explicit than most treatments. At the same time, it enables one to go further,
of tiling using 1#, and then deriving as a corollary Church's Theorem that satisfiability in first-order
logic is undecidable.


```{tip} Most of the chapters in the book are [Jupyter
notebooks](https://docs.jupyter.org/en/latest/index.html).
```{note}
Most of the chapters in the book are Jupyter notebooks.
(Some others are markdown files.)
So rather than simply read, these chapters are intended to
Rather than simply read, these chapters are intended to
be *run*. 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. At the present time, I don't have buttons to run
it on CoCalc, and the best option is to run them on Colab. For this, one starts by clicking on the button
at the top.
```

## Status as of March 15, 2023

I am in the process of adding materials to the book. The original
[source](https://iulg.sitehost.iu.edu/trm) for the course had much of the material, and the centerpiece was
the Javascript interpreter for 1# developed by my former PhD students Robert Rose and David Sprunger. In
2022, I re-wrote the interpreter in Python and turned the website into notebooks. The rest of the course
exists in lecture slides. So much of what I am doing now is revising them and adding them here.

There are a number of still-missing chapters:
models of computation other than register machines,
computably enumerable sets, the arithmetic hierarchy, and
introductions to complexity theory and Kolmogorov complexity.
One nice feature of a project with "continual updates" is that
these can come later.
But the first few chapters have missing discussions as well.
So the book can't quite be used in a class setting.


```{admonition} Credits
:class: warning
Only a tiny fraction of the results here is due to the author.
Most are standard in the literature. In time, I willl add proper credits.
```

## Wish List

If anyone sees this and wants to help, here are a few things which I would like.

1. These notebooks open on Colab, but doing that loses the LaTeX macros that are in my _conf.yml file. It also loses the nice "admonition" boxes, like the "Tip" above. I would like to rectify this,
and the help on the web doesn't address it.

2. The way I get pictures in discussions such as tiling is very painstaking. I would like to find some tools that make this easier.

3. Once nice feature of the [Javascript interpreter for 1#](http://rrose1.github.io/jsonesharp/) is that one could
run it slowly. In this book as it stands, one can't quite do this. One can run a program "step-by-step",
but this means looking at the trace. It would be nice to have an animation the way the Javascript program
had it. For that matter, someone might want to animate some of the proofs in computability theory which
make use of "movable markers" or other such devices.

4. I don't yet have things set up to get feedback and correction from readers.


## Using the book

There are a number of ways the book could be used in courses for students in several disciplines. For computer science students,
Expand Down
95 changes: 48 additions & 47 deletions _build/html/_sources/introOneSharp/haltDef.ipynb
Original file line number Diff line number Diff line change
@@ -1,39 +1,26 @@
{
"nbformat": 4,
"nbformat_minor": 0,
"metadata": {
"colab": {
"provenance": [],
"authorship_tag": "ABX9TyNdJvBPc4d/BKV6wg71UbKH",
"include_colab_link": true
},
"kernelspec": {
"name": "python3",
"display_name": "Python 3"
},
"language_info": {
"name": "python"
}
},
"cells": [
{
"cell_type": "markdown",
"metadata": {
"id": "view-in-github",
"colab_type": "text"
"colab_type": "text",
"id": "view-in-github"
},
"source": [
"<a href=\"https://colab.research.google.com/github/lmoss/onesharp/blob/main/introOneSharp/haltDef.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
]
},
{
"attachments": {},
"cell_type": "markdown",
"metadata": {
"id": "0HV2nGXx89_T"
},
"source": [
"## When does a program halt?\n",
"```1#``` has programs which contain *infinite loops* such as\n",
"\n",
"$\\one\\hash$ has programs which contain *infinite loops* such as\n",
"\n",
"1###1####\n",
"```111###111####```\n",
"\n",
"This program never finishes. If you run this in an interpreter, you will need to figure out how to stop the execution. Most of the time, we are interested in programs which do finish. Actually, we are interested in programs which finish in a special way.\n",
"\n",
Expand All @@ -48,19 +35,19 @@
"```\n",
"\n",
"To see the difference, consider the following two programs: \n",
"$\\one\\one\\hash\\hash\\hash$ and $\\one\\hash$. Suppose we run them with some fixed but arbitrary word $x$ in R1.\n",
"```11###``` and ```1#111. Suppose we run them with some fixed but arbitrary word $x$ in R1.\n",
"\n",
"\n",
"The first says \"Go forward 2,\" and the second \"Add $\\one$ to R1.\"\n",
"The first says \"Go forward 2,\" and the second \"Add ```1``` to R1.\"\n",
"\n",
"The first halts, while the second halts improperly."
],
"metadata": {
"id": "0HV2nGXx89_T"
}
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "3QaKbogZ-iks"
},
"source": [
"```{exercise}\n",
":label: on-halting\n",
Expand All @@ -76,13 +63,13 @@
"\n",
"[It would be better to try to solve this problem without running the programs.]\n",
"````"
],
"metadata": {
"id": "3QaKbogZ-iks"
}
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "nNMNTP62_Hu-"
},
"source": [
"```{exercise}\n",
"{ref}`on-halting` was concerned with programs run on all empty registers. Find a program $p$ and words $w_1$, $w_2$, and $w_3$ so that \n",
Expand All @@ -93,13 +80,14 @@
"\n",
"(c) When started with $w_3$ in R1, $p$ goes into an infinite loop inside $p$.\n",
"```"
],
"metadata": {
"id": "nNMNTP62_Hu-"
}
]
},
{
"attachments": {},
"cell_type": "markdown",
"metadata": {
"id": "Eb0F7IAv_Mim"
},
"source": [
"## Halting: the formal definitions\n",
"\n",
Expand All @@ -111,23 +99,36 @@
"\n",
"3. Instruction $n$ of $p$ (the last instruction) is of the form form ```1```<sup>$k$</sup>```#####```, and at some point in the run of $p$, we reach this last instruction with Rk empty.\n",
"\n",
"4. Instruction $n-1$ of $p$ (the next-to-last instruction) is of the form form ```1```<sup>$k$</sup>```#####```, and at some point in the run of $p$, we reach this instruction with Rk containing a word beginning with $\\one$.\n",
"4. Instruction $n-1$ of $p$ (the next-to-last instruction) is of the form form ```1```<sup>$k$</sup>```#####```, and at some point in the run of $p$, we reach this instruction with Rk containing a word beginning with ```1```.\n",
"\n",
"5. Instruction $n-2$ of $p$ (the second-to-last instruction) is of the form form ```1```<sup>$k$</sup>```#####```, and at some point in the run of $p$, we reach this instruction with Rk containing a word beginning with $\\hash$.\n"
],
"metadata": {
"id": "Eb0F7IAv_Mim"
}
"5. Instruction $n-2$ of $p$ (the second-to-last instruction) is of the form form ```1```<sup>$k$</sup>```#####```, and at some point in the run of $p$, we reach this instruction with Rk containing a word beginning with ```#```.\n"
]
},
{
"cell_type": "markdown",
"metadata": {
"id": "F3WqUTegf1w1"
},
"source": [
"Again, these are the formal conditions. Most of the time it is enough to work with the informal conditions that we started with:\n",
"a program $p$ *halts* on some inputs if at some point during the execution of $p$ on the inputs, the control transfers to right below the last instruction of $p$. \n"
],
"metadata": {
"id": "F3WqUTegf1w1"
}
]
}
]
}
],
"metadata": {
"colab": {
"authorship_tag": "ABX9TyNdJvBPc4d/BKV6wg71UbKH",
"include_colab_link": true,
"provenance": []
},
"kernelspec": {
"display_name": "Python 3",
"name": "python3"
},
"language_info": {
"name": "python"
}
},
"nbformat": 4,
"nbformat_minor": 0
}
Loading

0 comments on commit feeab90

Please sign in to comment.