{
  localUrl: '../page/proof_of_rice_theorem.html',
  arbitalUrl: 'https://arbital.com/p/proof_of_rice_theorem',
  rawJsonUrl: '../raw/5t9.json',
  likeableId: '3369',
  likeableType: 'page',
  myLikeValue: '0',
  likeCount: '2',
  dislikeCount: '0',
  likeScore: '2',
  individualLikes: [
    'EricBruylant',
    'JaimeSevillaMolina'
  ],
  pageId: 'proof_of_rice_theorem',
  edit: '2',
  editSummary: '',
  prevEdit: '1',
  currentEdit: '2',
  wasPublished: 'true',
  type: 'wiki',
  title: 'Proof of Rice's theorem',
  clickbait: 'A standalone proof of Rice's theorem, including one surprising lemma.',
  textLength: '9513',
  alias: 'proof_of_rice_theorem',
  externalUrl: '',
  sortChildrenBy: 'likes',
  hasVote: 'false',
  voteType: '',
  votesAnonymous: 'false',
  editCreatorId: 'PatrickStevens',
  editCreatedAt: '2016-08-08 14:35:54',
  pageCreatorId: 'PatrickStevens',
  pageCreatedAt: '2016-08-08 14:26:18',
  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: '136',
  text: '[summary: This lens proves [5mv Rice's theorem] via a fixed-point theorem on computable functions.]\n\nRecall the formal statement of [5mv Rice's theorem]:\n\n> We will use the notation $[n]$ for the $n$th [5pd Turing machine] under some fixed [description_number numbering system].\nEach such machine induces a [-3jy], which we will also write as $[n]$ where this is unambiguous due to context; then it makes sense to write $[n](m)$ for the value that machine $[n]$ outputs when it is run on input $m$.\n\n> Let $A$ be a non-empty, proper %%note:That is, it is not the entire set.%% subset of $\\{ \\mathrm{Graph}(n) : n \\in \\mathbb{N} \\}$, where $\\mathrm{Graph}(n)$ is the [graph_of_a_function graph] of the [-5p2] computed by $[n]$, the $n$th Turing machine.\nThen there is no Turing machine $[r]$ such that:\n\n> - $[r](i)$ is $1$ if $\\mathrm{Graph}(i) \\in A$\n> - $[r](i)$ is $0$ if $\\mathrm{Graph}(i) \\not \\in A$.\n\nWe give a proof that is (very nearly) constructive: one which (if we could be bothered to work it all through) gives us an explicit example %%note:Well, very nearly; see the next note.%% of a [5pd Turing machine] whose "am-I-in-$A$" nature cannot be determined by a Turing machine.\n%%note:It's only "very nearly" constructive. It would be *actually* constructive if we knew in advance a specific example of a program whose function is in $A$, and a program whose function is in $B$. The proof here assumes the existence of a program of each type, but ironically the theorem itself guarantees that there is no fully-general way to *find* such programs.%%\n\nWe will present an intermediate lemma which does all the heavy lifting; this makes the actual reasoning rather unclear but very succinct, so we will also include an extensive worked example of what this lemma does for us.\n\n# Fixed point theorem\n\nThe intermediate lemma is a certain fixed-point theorem.\n\n> Let $h: \\mathbb{N} \\to \\mathbb{N}$ be [total_function total] computable: that is, it halts on every input.\nThen there is $n \\in \\mathbb{N}$ such that $\\mathrm{Graph}(n) = \\mathrm{Graph}(h(n))$. %%note:And, moreover, we can actually *find* such an $n$.%%\n\nThat is, the "underlying function" of $n$ - the partial function computed by $[n]$ - has the same output, at every point, as the function computed by $[h(n)]$.\nIf we view $h$ as a way of manipulating a program (as specified by its [-description_number]), then this fixed-point theorem states that we can find a program whose underlying function is not changed at all by $h$.\n\nThe proof of this lemma is quite simple once the magic steps have been discovered, but it is devilishly difficult to intuit, because it involves two rather strange and confusing recursions and some self-reference.\n\nRecall the [translation_lemma $s_{mn}$ theorem], which states that there is a total computable function $S$ of two variables $m, n$ such that for every $e \\in \\mathbb{N}$, we have $[e](m, n) = [S(e,m)](n)$: that is, there is a total computable way $S$ of [-50p] computable functions.\n(Strictly speaking, our Turing machines only take one argument. Therefore we should use a computable pairing scheme such as [cantor_pairing_function Cantor's pairing function], so that actually $[e](m,n)$ should be interpreted as $[e](\\mathrm{pair}(m, n))$.)\n\nThen the function which takes the pair $(e, x)$ and outputs the value of $[ h(S(e,e)) ](x)$ is computable, so it has a description number $a$, say.\n%%note:This is the first strange part: we are treating $e$ both as a description number, and as an input to $[e]$, when we consider $S(e,e)$.%%\n\nNow we claim that $S(a, a)$ is the $n$ we seek. %%note:This is the second strange part, for the same reason as $S(e,e)$ was the first; but this one is even worse, because the definition of $a$ already involves a weird recursion and we've just added another one on top.%%\nIndeed, for any $x$, $[n](x) = [S(a,a)](x)$ by definition of $n$; this is $[a](a, x)$ by the $s_{mn}$ theorem; this is $[h(S(a,a))](x)$ by definition of $[a]$; and that is $[h(n)](x)$ by definition of $n$.\n\nTherefore $[n](x) = [h(n)](x)$, so we have found our fixed point.\n\n%%hidden(Worked example):\n[todo: I'm not clever enough to check this properly, but someone should]\n\nSuppose our description numbering scheme is just "expand $n$ as a number in base $128$, and interpret the result as an [ASCII](https://en.wikipedia.org/wiki/ASCII) %%note:This is a standard, agreed-upon method of turning a number between $0$ and $128$ into a character.%% string; then interpret that string as [Python](https://en.wikipedia.org/wiki/Python_(programming_language)) code".\n\nThen our function $h$, whatever it may be, can be viewed just as transforming Python code.\n\nSuppose $h$ does nothing more than insert the following line of code as the second line of its input:\n\n\tx = 0\n\nSo, for instance, it takes the string \n\n\tx = 1\n\tprint(x)\n\nand returns\n\n\tx = 1\n\tx = 0\n\tprint(x)\n\nthereby changing the function computed from "return the constant $1$" to "return the constant $0$", in this case.\nNote that many other functions will not change at all: for example, those which don't contain a variable $x$ in the first place will be unchanged, because all the modification does is add in an initialisation of a variable which will never subsequently be used.\n\nThe fixed-point theorem guarantees that there is indeed a Python program which will not change at all under this modification (though in this case it's very obvious).\nIn fact the theorem *constructs* such a program; can we work out what it is?\n\nFirst of all, $S(m, n)$ can be implemented as follows.\nWe will take our Python code to be written so that their input is given in the variable `r1`, so $[e](5)$ is simply the Python code represented by $e$ but where the code-variable `r1` is initialised to $5$ first; that is, it can be found by prepending the line `r1 = 5` to the code represented by $e$.\nThen we will assume that Python comes with a function `eval` (corresponding to $S$) which takes as its input a string %%note:The string is standing in place of $m$, but we have just skipped the intermediate step of "unpack the integer into a string" and gone straight to assuming it is a string.%% and another argument with which `eval` initialises the variable `x` before running the string as a Python program in a separate instance of Python:\n\n\teval("print(r1)", 5)  # does nothing other than print the number 5\n\teval("print(y)", 5)  # throws an error because `y` is not defined when it comes to printing it\n\teval("print(6)", 5)  # prints 6, ignoring the fact that the variable `r1` is equal to `5` in the sub-instance\n\nRemember, our proof of the fixed point theorem says that the program we want has code $S(a, a)$, where $a$ takes a pair $(e, x)$ as input, and outputs $[h(S(e,e))](x)$.\nWhat is $a$ specifically here?\nWell, on the one hand we're viewing it as a string of code (because it comes as the first argument to $S$), and on the other we're viewing it as an integer (because it also comes as the second argument to $S$).\n\nAs code, `a` is the following string, where `h` is to be replaced by whatever we've already decided $h$ is:\n\n\teval("r1 = e; h(eval(r1, str_as_int(r1)))", x)\n\nWe are assuming the existence of a function `str_as_int` which takes an ASCII string and returns the integer whose places in base 128 are the ASCII for each character of the string in turn.\n\nFor example, we have $h$ inserting the line `x = 0` as the second line, so our `a` is:\n\n\teval("r1 = e; x = 0; eval(r1, str_as_int(r1))", x)\n\nAs a number, `a` is just the ASCII for this, interpreted in base 128 (i.e. a certain number which in this case happens to have 106 digits, which is why we don't give it here).\n\nThe claim of the fixed-point theorem, then, is that the following program is unchanged by $h$:\n\n\teval("eval(\\"r1 = e; x = 0; eval(r1, str_as_int(r1))\\", x)", str_to_int("eval(\\"r1 = e; x = 0; eval(r1, str_as_int(r1))\\", x)"))\n\nYou may recognise this as a [322 quining] construction.\n%%\n\n# Deducing Rice's theorem from the fixed point theorem\n\nFinally, Rice's theorem follows quickly: suppose we could decide in general whether $\\mathrm{Graph}(n) \\in A$ or not, and label by $\\iota$ the computable function which decides this (that is, whose value is $1$ if $\\mathrm{Graph}(n) \\in A$, and $0$ otherwise).\n\nSince $A$ is nonempty and proper, there are natural numbers $a$ and $b$ such that $\\mathrm{Graph}(a) \\in A$ but $\\mathrm{Graph}(b) \\not \\in A$.\nDefine the computable function $g$ which takes $n$ and outputs $a$ if $\\iota(n) = 0$, and $b$ otherwise.\n(That is, it flips its input: if its input had the property of $A$, the function $g$ outputs $b$ whose graph is not in $A$, and vice versa.\nInformally, it is the program-transformer that reads in a program, determines whether the program computes a function in $A$ or not, and transforms the program into a specific canonical example of something which has the *opposite* $A$-ness status.)\n\nBy the fixed-point theorem, we can find $n$ such that $\\mathrm{Graph}(n) = \\mathrm{Graph}(g(n))$.\n\nBut now we can ask whether $\\mathrm{Graph}(n)$ is in $A$ (and therefore whether $\\mathrm{Graph}(g(n))$ is in $A$).\n\n- If it is in $A$, then $g(n) = b$ and so $\\mathrm{Graph}(g(n)) = \\mathrm{Graph}(b)$ which is not in $A$.\n- If it is not in $A$, then $g(n) = a$ and so $\\mathrm{Graph}(g(n)) = \\mathrm{Graph}(a)$ is in $A$.\n\nWe have obtained [46z contradictions] in both cases (namely that $\\mathrm{Graph}(g(n))$ is both in $A$ and not in $A$), so it must be the case that $\\iota$ does not exist after all.',
  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: {},
  creatorIds: [
    'PatrickStevens'
  ],
  childIds: [],
  parentIds: [
    'rice_theorem'
  ],
  commentIds: [],
  questionIds: [],
  tagIds: [
    'b_class_meta_tag'
  ],
  relatedIds: [],
  markIds: [],
  explanations: [],
  learnMore: [],
  requirements: [],
  subjects: [],
  lenses: [],
  lensParentId: 'rice_theorem',
  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: '18611',
      pageId: 'proof_of_rice_theorem',
      userId: 'EricBruylant',
      edit: '0',
      type: 'newTag',
      createdAt: '2016-08-08 15:11:22',
      auxPageId: 'b_class_meta_tag',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '18603',
      pageId: 'proof_of_rice_theorem',
      userId: 'PatrickStevens',
      edit: '2',
      type: 'newEdit',
      createdAt: '2016-08-08 14:35:55',
      auxPageId: '',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '18596',
      pageId: 'proof_of_rice_theorem',
      userId: 'PatrickStevens',
      edit: '0',
      type: 'newParent',
      createdAt: '2016-08-08 14:26:40',
      auxPageId: 'rice_theorem',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '18594',
      pageId: 'proof_of_rice_theorem',
      userId: 'PatrickStevens',
      edit: '1',
      type: 'newEdit',
      createdAt: '2016-08-08 14:26:18',
      auxPageId: '',
      oldSettingsValue: '',
      newSettingsValue: ''
    }
  ],
  feedSubmissions: [],
  searchStrings: {},
  hasChildren: 'false',
  hasParents: 'true',
  redAliases: {},
  improvementTagIds: [],
  nonMetaTagIds: [],
  todos: [],
  slowDownMap: 'null',
  speedUpMap: 'null',
  arcPageIds: 'null',
  contentRequests: {}
}