{
localUrl: '../page/uncomputability.html',
arbitalUrl: 'https://arbital.com/p/uncomputability',
rawJsonUrl: '../raw/46h.json',
likeableId: '2635',
likeableType: 'page',
myLikeValue: '0',
likeCount: '4',
dislikeCount: '0',
likeScore: '4',
individualLikes: [
'EricBruylant',
'JaimeSevillaMolina',
'EricRogstad',
'StephanieZolayvar'
],
pageId: 'uncomputability',
edit: '12',
editSummary: '',
prevEdit: '11',
currentEdit: '12',
wasPublished: 'true',
type: 'wiki',
title: 'Uncomputability',
clickbait: 'The diagonal function and the halting problem',
textLength: '6281',
alias: 'uncomputability',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2016-06-14 22:59:38',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-06-11 21:20:17',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '2',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '71',
text: 'Imagine you were tasked with the mission of finding out which things can and cannot be calculated with a computer, given that you had infinite memory and infinite time.\n\nGiven the generality of computers, you might be tempted to say everything, but it turns out that this is not the case.\n\nTo begin tackling this problem, we need a formal notion of what it means to compute something. We are going to focus on computing **natural functions**; that is, [3jy functions] which transform [45h natural numbers] to natural numbers.\n\nAs natural numbers can be used to encode pretty much anything, this class of computations is far wider than one might initially think. For example, we can [-encode] finite sequences of arbitrary length of natural numbers in a single natural number, and we can encode words in sequences of numbers.\n\nWe are going to say that a computer program computes a certain natural function if on input $n$ it returns the result of applying such function to $n$, for every natural $n$. We note that programs do not have to halt on inputs; they may just run forever. In that case, we will say that the program is computing a partial function, which is not defined on some inputs.\n\n%%%knows-requisite([2w0]):\nNow, the first thing to notice is that the set of possible functions from $\\mathbb{N}$ to $\\mathbb{N}$ is not [-enumerable], while the set of possible programs, which are finite sequences of a finite quantity of symbols, is enumerable. Thus, there cannot be a one-to-one correspondence between functions and programs; there must necessarily exist a function which is not computed by any program.\n\nSo computers cannot compute everything!\n%%%\n\n----\n##The diagonal function\n\nWe are going to construct a concrete example of a function which is not computable.\n\nImagine an infinite list of every possible Python program, associated with the infinite outputs each would produce if we feed it the sequence of natural numbers $1,2,3,...$.\n\nThus, we may end up with a table such as this:\n\nprogram #1: 0->1, 1->X, 2->3,...\n\nprogram #2:\n\netc...\n\nWhere an X means that the program does not halt on that input or does not return an output, and thus the function it represents is not defined there.\n\nNow, we are going to construct an explicit function which is not computable using this table.\n\nLet $DIAG$ be such that:\n$$\nDIAG(n) = \\left\\{\n \\begin{array}{lr}\n 1\\ if\\ M_n(n) = 0\\\\\n 0\\ if\\ M_n(n)\\mbox{ is undefined or defined and greater than 0}\n \\end{array}\n\\right.\n$$\n\nThe notation $M_n$ means *"the $n$th program in our enumeration of programs"*. \nLet's see what we have done there. We are looking at the $n$th entry of every program and saying that this function on input $n$ outputs something different that the $n$th program. This technique is called [-diagonalization], and it is ubiquitous in computability and logic.\n\nThe function $DIAG$, known as the [-diagonal_function], is guaranteed to disagree with every program on at least one input. Thus, there cannot be a program which computes $DIAG$!\n\n----\n##The halting function\nThe reader may at this point be however not satisfied with such an unnatural example of an uncomputable function. After all, who is going to want to compute such a weird thing? Do not dismay, for there is a much better example: the halting function.\n\nLet $HALT$ be defined as:\n$$\nHALT(n,x) = \\left\\{\n \\begin{array}{lr}\n 1\\ if\\ M_n(x)\\mbox{ halts}\\\\\n 0\\ if\\ M_n(x)\\mbox{ does not halt }\n \\end{array}\n\\right.\n$$\n\nThat is, the function $HALT$ decides whether a given program is going to halt on a particular input. Now that is interesting.\n\nTo cite one imaginative use of the halting function, one could for example code a program which on any input simply ignores the input and starts looking for a counterexample of the Collatz conjecture, halting [-46m] it finds one. Then we could use the halting function to see whether the conjecture is true or false.\n\nSadly, $HALT$ is not computable. We are going to give two proofs of this fact, one by **reduction** to the diagonal function and other by **diagonalization**.\n\n###Proof by reduction\nProofs by **reduction** are quite common in computability. We start by supposing that the function we are dealing with, in this case $HALT$, is computable, and then we proceed to use this assumption to show that if that was the case we could compute another function we know is uncomputable.\n\nSuppose we have a program, which we are going to represent by $HALT$, which computes the halting function.\n\nThen we could write a program such as this one:\n\n DIAGONAL(n):\n if HALT(n,n):\n return 1 if M_n==0 else return 0\n else return 0\n\n\nWhich computes the diagonal function. As we know such a program cannot possibly exist, we conclude by *reductio ad absurdum* that $HALT$ is not computable.\n\n###Exercise\nProve that $HALT$ is reducible to $DIAGONAL$; ie, that if $DIAGONAL$ was computable we could compute $HALT$.\n\n%%hidden(Show solution):\nSuppose we want to know whether the program $PROG$ halts on input $n$. Then we first code the auxiliary program:\n\n AUX(x): \n PROG(n)\n return 0\n\n\nThat is, $AUX$ is the program which on any input first runs $PROG$ on input $n$ and then outputs $0$ if $PROG$ ever halts.\n\nThen $DIAG(\\ulcorner AUX\\urcorner)==1$ iff $PROG$ halts on input $n$.\n%%\n\n\n\n###Proof by diagonalization\nAnother nifty proof of uncomputability comes from diagonalization.\n\nAs before, let's suppose $HALT$ is computable. Then we could write a program such as this one:\n\n prog(n):\n if HALT(n,n)==1: \n loop forever\n else return 0\n\nThe program halts on input $n$ iff $M_n$ does not halt on input $n$.\n\nNow, let $\\ulcorner prog\\urcorner$ represent the number in the list of the program which occupies the $prog$ program. Here comes the question: does $prog$ halt when its input is $\\ulcorner prog \\urcorner$?\n\nSupposing either yes or no leads to a contradiction, so we conclude that such a program cannot possibly exist, and it follows from the contradiction that $HALT$ is not computable.\n\n---\nSo now you are ready to start your journey through the realm of computability!\n\nSuggested next steps include examining other uncomputable functions such as the [ busy beaver sequence], or proceeding to [ complexity theory].\n',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '2',
maintainerCount: '2',
userSubscriberCount: '0',
lastVisit: '',
hasDraft: 'false',
votes: [],
voteSummary: [
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0'
],
muVoteSummary: '0',
voteScaling: '0',
currentUserVote: '-2',
voteCount: '0',
lockedVoteType: '',
maxEditEver: '0',
redLinkCount: '0',
lockedBy: '',
lockedUntil: '',
nextPageId: '',
prevPageId: '',
usedAsMastery: 'false',
proposalEditNum: '0',
permissions: {
edit: {
has: 'false',
reason: 'You don't have domain permission to edit this page'
},
proposeEdit: {
has: 'true',
reason: ''
},
delete: {
has: 'false',
reason: 'You don't have domain permission to delete this page'
},
comment: {
has: 'false',
reason: 'You can't comment in this domain because you are not a member'
},
proposeComment: {
has: 'true',
reason: ''
}
},
summaries: {
Summary: 'Imagine you were tasked with the mission of finding out which things can and cannot be calculated with a computer, given that you had infinite memory and infinite time.'
},
creatorIds: [
'JaimeSevillaMolina',
'EricRogstad',
'EricBruylant'
],
childIds: [],
parentIds: [
'math'
],
commentIds: [
'46p',
'46s'
],
questionIds: [],
tagIds: [],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [
{
id: '3785',
parentId: 'uncomputability',
childId: 'uncomputability',
type: 'subject',
creatorId: 'AlexeiAndreev',
createdAt: '2016-06-17 21:58:56',
level: '1',
isStrong: 'false',
everPublished: 'true'
}
],
requirements: [
{
id: '3811',
parentId: 'uncountable',
childId: 'uncomputability',
type: 'requirement',
creatorId: 'AlexeiAndreev',
createdAt: '2016-06-17 21:58:56',
level: '1',
isStrong: 'false',
everPublished: 'true'
}
],
subjects: [
{
id: '3785',
parentId: 'uncomputability',
childId: 'uncomputability',
type: 'subject',
creatorId: 'AlexeiAndreev',
createdAt: '2016-06-17 21:58:56',
level: '1',
isStrong: 'false',
everPublished: 'true'
}
],
lenses: [],
lensParentId: '',
pathPages: [],
learnMoreTaughtMap: {},
learnMoreCoveredMap: {},
learnMoreRequiredMap: {},
editHistory: {},
domainSubmissions: {},
answers: [],
answerCount: '0',
commentCount: '0',
newCommentCount: '0',
linkedMarkCount: '0',
changeLogs: [
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12871',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '12',
type: 'newEdit',
createdAt: '2016-06-14 22:59:39',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12616',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '11',
type: 'newEdit',
createdAt: '2016-06-14 11:18:05',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12614',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '10',
type: 'newEdit',
createdAt: '2016-06-14 08:43:56',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12613',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '9',
type: 'newEdit',
createdAt: '2016-06-14 08:41:56',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '2675',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '12612',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '8',
type: 'newEdit',
createdAt: '2016-06-14 08:40:31',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12487',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '5',
type: 'newRequirement',
createdAt: '2016-06-12 08:32:57',
auxPageId: 'uncountable',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '2641',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '12439',
pageId: 'uncomputability',
userId: 'EricBruylant',
edit: '5',
type: 'newEdit',
createdAt: '2016-06-11 22:17:50',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '2640',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '12438',
pageId: 'uncomputability',
userId: 'EricRogstad',
edit: '4',
type: 'newEdit',
createdAt: '2016-06-11 22:02:25',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '2639',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '12437',
pageId: 'uncomputability',
userId: 'EricRogstad',
edit: '3',
type: 'newEdit',
createdAt: '2016-06-11 21:55:05',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '2638',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '12436',
pageId: 'uncomputability',
userId: 'EricRogstad',
edit: '2',
type: 'newEdit',
createdAt: '2016-06-11 21:54:21',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '2649',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '12435',
pageId: 'uncomputability',
userId: 'AlexeiAndreev',
edit: '1',
type: 'newParent',
createdAt: '2016-06-11 21:42:32',
auxPageId: 'math',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12431',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newTeacher',
createdAt: '2016-06-11 21:20:17',
auxPageId: 'uncomputability',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12432',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newSubject',
createdAt: '2016-06-11 21:20:17',
auxPageId: 'uncomputability',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12433',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-06-11 21:20:17',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12425',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'deleteRequirement',
createdAt: '2016-06-11 17:38:08',
auxPageId: 'mindcrime',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '12424',
pageId: 'uncomputability',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newRequirement',
createdAt: '2016-06-11 17:38:03',
auxPageId: 'mindcrime',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}