{
localUrl: '../page/6bf.html',
arbitalUrl: 'https://arbital.com/p/6bf',
rawJsonUrl: '../raw/6bf.json',
likeableId: '3580',
likeableType: 'page',
myLikeValue: '0',
likeCount: '3',
dislikeCount: '0',
likeScore: '3',
individualLikes: [
'EricBruylant',
'JaimeSevillaMolina',
'DylanHendrickson'
],
pageId: '6bf',
edit: '4',
editSummary: '',
prevEdit: '3',
currentEdit: '4',
wasPublished: 'true',
type: 'wiki',
title: 'Rice's Theorem: Intro (Math 1)',
clickbait: 'You can't write a program that looks at another programs source code, and tells you whether it computes the Fibonacci sequence.',
textLength: '6186',
alias: '6bf',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'DylanHendrickson',
editCreatedAt: '2016-11-18 20:38:43',
pageCreatorId: 'DylanHendrickson',
pageCreatedAt: '2016-10-07 17:54:16',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '0',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '65',
text: 'Rice's Theorem says that you can't in general figure out anything about what a computer program outputs just by looking at the program. Specifically, we think of programs as taking inputs, doing some kind of computation on the input, and possibly eventually stopping and giving an output. Only "possibly" because sometimes programs get in an infinite loop and go forever. The assignment that takes an input to the output of a program on that input (if it exists) is called the [-5p2] computed by that program %%note:"Partial" functions because the output doesn't exist if the program runs forever.%%. \n\nRice's Theorem says that for any property of partial functions, you can't write a program that looks at some other program's source code, and tells you whether that program computes a function with the property %%note:This is true except for "trivial" properties like "all partial functions" or "no partial functions," which are easy to write programs to test.%%.\n\nFor example, say we want to know whether a program computes the [Fibonacci_sequence], i.e. returns the $n$th Fibonacci number on input $n$. If we try to write a Fibonacci-checker program that tells us whether programs compute the Fibonacci sequence, we're going to have a hard time, because by Rice's Theorem it's impossible!\n\nThere might be some programs for which we can say "yes, this program definitely computes the Fibonacci sequence," but we can't write a general procedure that always tells whether some program computes the Fibonacci sequence; there are some very convoluted programs that compute it, but not obviously, and if you modify the Fibonacci-checker to handle some of them, there will always be even more convoluted programs that it doesn't work on.\n\nWe make a distinction between *programs* and *(partial) functions computed by programs*. There are usually many programs that compute the same function. Rice's Theorem only cares about the partial functions; it's possible to test statements about programs, like "has fewer than 100 lines." But this kind of statement won't always tell you something about the function the program computes.\n\n# Proof\n\nTo prove Rice's Theorem, we'll use the [46h halting theorem], which says that you can't write a program that can always tell whether some program will halt on some input. Here's how the proof will go: suppose you come up with a program that checks whether programs compute partial functions with some property, e.g. you successfully write a Fibonacci-checker. We'll then use the Fibonacci-checker to design a Halt-checker, which can tell when a program halts. But this is impossible by the Halting theorem, so this couldn't be the case: your Fibonacci-checker must not work!\n\nWe need to make a couple of assumptions. First, that the empty function, meaning the function "computed" by a program that always enters an infinite loop regardless of its input, does not satisfy the property. If it does, we can replace the property by its opposite (say, replace "computes the Fibonacci sequence" with "doesn't compute the Fibonacci sequence"). If we can tell whether a program computes a function that *doesn't* have the property, then we can tell when it does, simply be reversing the output.\n\nSecond, we assume there is *some* program that does compute a function with the property, i.e. a program that the checker says "yes" to. If there isn't, we could have the checker always say "no." Say the program $s$ computes a function with the property.\n\n Now suppose you have a checker $C$ that, when given a program as input, returns whether the program computes a function with some property of interest. We want to test whether some program $M$ halts, when given input $x$. \n\nWe start by building a new program, called $Proxy_s$, which does the following on some input $z$:\n\n- Run $M$ on input $x$.\n- Run $s$ on input $z$, and return the result.\n\nIf $M$ halts on $x$, $Proxy_s$ moves on to the second step, and returns the same value as $s$. Since they return the same value (or no value, because of an infinite loop) on every possible input, $s$ and $Proxy_s$ compute the same function. So $Proxy_s$ computes a function with the property.\n\nIf $M$ doesn't halt on $x$, $Proxy_s$ never finishes the first step, and runs forever. So $Proxy_s$ always ends up in an infinite loop, which means it computes the empty function. So $Proxy_s$ computes a function that doesn't have the property.\n\nWhat happens if we plug $Proxy_s$ as input into $C$? If $C$ says "yes," $Proxy_s$ computes a function with the property, which means $M$ halts on $x$. If $C$ says "no," $Proxy_s$ doesn't compute a function with the property, so $M$ doesn't halt on $x$.\n\nSo we can tell whether $M$ halts on $x$! All we have to do is write this proxy function, and ask $C$ whether its function has the property. But the Halting theorem says we can't do this! That means $C$ can't exist, and we can't write a checker to see whether programs compute functions with the property.\n\nAs an example, suppose we have a Fibonacci-checker $fib\\_checker$. The following Python program computes the Fibonacci numbers, and so $fib\\_checker$ says "yes" to it:\n\n def fib(n):\n a, b = 0, 1\n for i in range(n):\n a, b = b, a+b\n return a\n\nThen, for some program $M$ and input $x$, $Proxy_{fib}$ is the program:\n\n def Proxy_fib(z):\n M(x)\n return fib(z)\n\nIf $fib\\_checker$ works, this program says whether $M$ halts on $x$:\n\n def halts(M,x)\n return fib_checker(Proxy_fib)\n\nExpanding this, we have the program:\n\n def halts(M,x)\n return fib_checker('''\n M(x)\n a, b = 0, 1\n for i in range(n):\n a, b = b, a+b\n return a\n ''')\n\nIf $M$ halts on $x$, the program inside the triple quotes computes the Fibonacci sequence, so $fib\\_checker$ returns $true$, and so does $halts$. If $M$ doesn't halt on $x$, the program in the triple quotes also doesn't halt, and returns the empty function, which isn't the Fibonacci sequence. So $fib\\_checker$ returns $false$, and so does $halts$. ',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '1',
maintainerCount: '1',
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: 'Rice's Theorem says that you can't in general figure out anything about what a computer program outputs just by looking at the program. Specifically, we think of programs as taking inputs, doing some kind of computation on the input, and possibly eventually stopping and giving an output. Only "possibly" because sometimes programs get in an infinite loop and go forever. The assignment that takes an input to the output of a program on that input (if it exists) is called the [-5p2] computed by that program %%note:"Partial" functions because the output doesn't exist if the program runs forever.%%.'
},
creatorIds: [
'DylanHendrickson'
],
childIds: [],
parentIds: [
'rice_theorem'
],
commentIds: [],
questionIds: [],
tagIds: [
'math1',
'start_meta_tag'
],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [],
requirements: [
{
id: '6523',
parentId: 'math1',
childId: '6bf',
type: 'requirement',
creatorId: 'DylanHendrickson',
createdAt: '2016-10-07 17:03:53',
level: '2',
isStrong: 'false',
everPublished: 'true'
},
{
id: '6524',
parentId: 'programming_familiarity',
childId: '6bf',
type: 'requirement',
creatorId: 'DylanHendrickson',
createdAt: '2016-10-07 17:53:42',
level: '2',
isStrong: 'false',
everPublished: 'true'
}
],
subjects: [
{
id: '6539',
parentId: 'rice_theorem',
childId: '6bf',
type: 'subject',
creatorId: 'EricRogstad',
createdAt: '2016-10-09 02:36:15',
level: '2',
isStrong: 'true',
everPublished: 'true'
}
],
lenses: [],
lensParentId: 'rice_theorem',
pathPages: [],
learnMoreTaughtMap: {},
learnMoreCoveredMap: {},
learnMoreRequiredMap: {},
editHistory: {},
domainSubmissions: {},
answers: [],
answerCount: '0',
commentCount: '0',
newCommentCount: '0',
linkedMarkCount: '0',
changeLogs: [
{
likeableId: '3717',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '20361',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '4',
type: 'newEdit',
createdAt: '2016-11-18 20:38:43',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3713',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '2',
dislikeCount: '0',
likeScore: '2',
individualLikes: [],
id: '20360',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '3',
type: 'newEdit',
createdAt: '2016-11-18 16:48:56',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '19974',
pageId: '6bf',
userId: 'EricRogstad',
edit: '0',
type: 'newSubject',
createdAt: '2016-10-09 02:36:15',
auxPageId: 'rice_theorem',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '19883',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '0',
type: 'newTag',
createdAt: '2016-10-07 17:54:18',
auxPageId: 'math1',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '19884',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '0',
type: 'newTag',
createdAt: '2016-10-07 17:54:18',
auxPageId: 'start_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '19880',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '0',
type: 'newParent',
createdAt: '2016-10-07 17:54:17',
auxPageId: 'rice_theorem',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '19881',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '0',
type: 'newRequirement',
createdAt: '2016-10-07 17:54:17',
auxPageId: 'math1',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '19882',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '0',
type: 'newRequirement',
createdAt: '2016-10-07 17:54:17',
auxPageId: 'programming_familiarity',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3592',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '19878',
pageId: '6bf',
userId: 'DylanHendrickson',
edit: '1',
type: 'newEdit',
createdAt: '2016-10-07 17:54:16',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}