1151:
104:. The syntax is the detail of how the program is written, or its "intension", and the semantics is how the program behaves when run, or its "extension". Rice's theorem asserts that it is impossible to decide a property of programs which depends only on the semantics and not on the syntax, unless the property is trivial (true of all programs, or false of all programs).
141:
In terms of general software verification, this means that although one cannot algorithmically check whether a given program satisfies a given specification, one can require programs to be annotated with extra information that proves the program is correct, or to be written in a particular restricted
142:
form that makes the verification possible, and only accept programs which are verified in this way. In the case of type safety, the former corresponds to type annotations, and the latter corresponds to
138:(taken in a broad sense) of those languages. In order to type check a program, its source code must be inspected; the operation does not depend merely on the hypothetical semantics of the program.
1010:. The proof works just as well if we have an algorithm for deciding any other non-trivial property of program behavior (i.e. a semantic and non-trivial property), and is given in general below.
1084:
is a function for computing squares if and only if step (1) terminates. Since we have assumed that we can infallibly identify programs for computing squares, we can determine whether
953:
841:
685:
601:
775:
1013:
The claim is that we can convert our algorithm for identifying squaring programs into one that identifies functions that halt. We will describe an algorithm that takes inputs
1138:. We could have had a method for recognizing programs for computing square roots, or programs for computing the monthly payroll, or programs that halt when given the input
342:
249:
212:
1555:
913:
887:
711:
523:
979:
801:
627:
497:
861:
735:
543:
471:
1108:, but only passes its description to the squaring-identification program, which by assumption always terminates; since the construction of the description of
1630:
1570:
1625:
1179:: we assume that there is a non-trivial property that is decided by an algorithm, and then show that it follows that we can decide the
1154:
If we have an algorithm that decides a non-trivial property, we can construct a Turing machine that decides the halting problem.
1491:
Since the halting problem is known to be undecidable, this is a contradiction and the assumption that there is an algorithm
134:
feature a type system which statically prevents type errors. In essence, this should be understood as a feature of the
69:
of programs. It implies that it is impossible, for example, to implement a tool that checks whether a given program is
17:
146:. Taken beyond type safety, this idea leads to correctness proofs of programs through proof annotations such as in
1215:
being the representation of an algorithm that never halts. If this is not true, then this holds for the algorithm
1162:
and are themselves represented by strings. The partial function computed by the algorithm represented by a string
1126:
This method does not depend specifically on being able to recognize functions that compute squares; as long as
918:
806:
97:
70:
632:
548:
1635:
714:
123:
101:
1032:
The algorithm for deciding this is conceptually simple: it constructs (the description of) a new program
185:
740:
409:
107:
By Rice's theorem, it is impossible to write a program that automatically verifies for the absence of
1159:
319:
1517:
1112:
can also be done in a way that always terminates, the halting-decision cannot fail to halt either.
325:
232:
195:
1527:
158:
93:
66:
892:
866:
690:
502:
473:
is a non-trivial, extensional and computable set of natural numbers. There is a natural number
958:
780:
606:
476:
1521:
1176:
181:
112:
50:
for all inputs?"), unlike a syntactic property (for instance, "does the program contain an
31:
1568:
Rice, H. G. (1953), "Classes of recursively enumerable sets and their decision problems",
8:
312:
127:
81:
39:
1600:
1589:
846:
720:
528:
456:
1584:
58:
property is one which is neither true for every program, nor false for every program.
1533:
77:
1579:
168:, which can only apply to finite-state programs, not to Turing-complete languages.
1096:, is such a program; thus we have obtained a program that decides whether program
153:
Another way of working around Rice's theorem is to search for methods which catch
1512:
1180:
381:
62:
47:
1560:
1550:
1158:
For the formal proof, algorithms are presumed to define partial functions over
165:
143:
46:
property is one about the program's behavior (for instance, "does the program
1619:
1546:
994:
Suppose, for concreteness, that we have an algorithm for examining a program
131:
130:, it is impossible to verify the absence of type errors. On the other hand,
108:
51:
1608:
1142:; in each case, we would be able to solve the halting problem similarly.
147:
115:
as input, and checking whether the program satisfies the specification.
1593:
1499:) that decides a non-trivial property for the function represented by
1002:
is an implementation of the squaring function, which takes an integer
1130:
program can do what we are trying to recognize, we can add a call to
1229:
decides a non-trivial property, it follows that there is a string
1150:
96:
can be performed automatically. One can distinguish between the
38:
states that all non-trivial semantic properties of programs are
984:
1194:) is an algorithm that decides some non-trivial property of
1556:
Introduction to
Automata Theory, Languages, and Computation
1104:. Note that our halting-decision algorithm never executes
1442:, i.e., the partial function that is never defined. Since
92:
Rice's theorem puts a theoretical bound on which types of
1605:
Theory of
Recursive Functions and Effective Computability
65:. It has far-reaching implications on the feasibility of
1183:, which is not possible, and therefore a contradiction.
80:, who proved it in his doctoral dissertation of 1951 at
448:
961:
921:
895:
869:
849:
809:
783:
743:
723:
693:
635:
609:
551:
531:
505:
479:
459:
328:
235:
198:
122:
of bugs. For example, Rice's theorem implies that in
157:
bugs, without being complete. This is the theory of
433:
terminate and return the same value for all inputs?
1530:, an analogue to Rice's theorem in lambda calculus
973:
947:
907:
881:
855:
835:
795:
769:
729:
705:
679:
621:
595:
537:
517:
491:
465:
336:
243:
206:
61:The theorem generalizes the undecidability of the
1571:Transactions of the American Mathematical Society
318:A more concise statement can be made in terms of
1617:
1203:. Without loss of generality we may assume that
118:This does not imply an impossibility to prevent
955:, which again contradicts extensionality since
1545:
1115:halts (a,i) { define t(n) { a(i)
1250:) = "yes". We can then define an algorithm
368:), the following questions are undecidable:
1221:that computes the negation of the property
985:Proof by reduction from the halting problem
1631:Theorems in the foundations of mathematics
1522:Kreisel-Lacombe-Shoenfield-Tseitin theorem
322:: The only decidable index sets are ∅ and
164:Yet another direction for verification is
111:in other programs, taking a program and a
1583:
1416:Assume that the algorithm represented by
1342:Assume that the algorithm represented by
948:{\displaystyle \varphi _{e}=\varphi _{a}}
836:{\displaystyle \varphi _{e}=\varphi _{b}}
330:
237:
200:
1149:
1056:being hard-coded into the definition of
680:{\displaystyle Q_{e}(x)=\varphi _{a}(x)}
596:{\displaystyle Q_{e}(x)=\varphi _{b}(x)}
124:dynamically typed programming languages
14:
1618:
1599:
1076:never gets to step (2), regardless of
1060:), and (2) then returns the square of
843:, contradicting the extensionality of
419:terminate and return 0 on every input?
132:statically typed programming languages
426:terminate and return 0 on some input?
1567:
1524:, generalizations of Rice's theorem
1284:first simulates the computation of
1040:, which (1) first executes program
998:and determining infallibly whether
449:Proof by Kleene's recursion theorem
171:
24:
770:{\displaystyle \varphi _{e}=Q_{e}}
73:, or even executes without error.
25:
1647:
1626:Theorems in theory of computation
1585:10.1090/s0002-9947-1953-0053041-6
1145:
1021:and determines whether program
989:
87:
27:Theorem in computability theory
674:
668:
652:
646:
590:
584:
568:
562:
453:Assume for contradiction that
440:equivalent to a given program
13:
1:
1539:
1338:decides the halting problem:
1304:simulates the computation of
1270:that represents an algorithm
1233:that represents an algorithm
1123:is_a_squaring_function(t) }
360:and returns a natural number
356:which takes a natural number
1376:) = "yes" and the output of
337:{\displaystyle \mathbb {N} }
244:{\displaystyle \mathbb {N} }
207:{\displaystyle \mathbb {N} }
186:partial computable functions
7:
1506:
1450:) = "no" and the output of
347:
76:The theorem is named after
10:
1652:
715:Kleene's recursion theorem
1401:) = "yes" and, therefore
1317:) and returns its result.
1175:. This proof proceeds by
908:{\displaystyle e\notin P}
882:{\displaystyle b\notin P}
706:{\displaystyle e\notin P}
518:{\displaystyle b\notin P}
1475:) = "no" and, therefore
1420:does not halt on input
1186:Let us now assume that
1025:halts when given input
159:abstract interpretation
1266:1. construct a string
1155:
975:
974:{\displaystyle a\in P}
949:
909:
883:
857:
837:
797:
796:{\displaystyle e\in P}
771:
731:
707:
681:
623:
622:{\displaystyle e\in P}
597:
539:
519:
493:
492:{\displaystyle a\in P}
467:
338:
245:
208:
100:of a program, and its
1334:We can now show that
1153:
1072:) runs forever, then
976:
950:
910:
889:, and conversely, if
884:
858:
838:
798:
772:
732:
708:
682:
624:
598:
540:
520:
499:and a natural number
494:
468:
376:terminate on a given
339:
246:
229:is neither empty nor
209:
1636:Undecidable problems
1518:Rice–Shapiro theorem
1177:reductio ad absurdum
959:
919:
893:
867:
847:
807:
781:
741:
721:
691:
633:
607:
549:
529:
525:. Define a function
503:
477:
457:
326:
233:
196:
182:admissible numbering
32:computability theory
1601:Rogers, Hartley Jr.
1528:Scott–Curry theorem
1088:, which depends on
1036:taking an argument
261:: for all integers
82:Syracuse University
18:Rice's Theorem
1563:, pp. 185–192
1551:Ullman, Jeffrey D.
1467:, it follows that
1458:) depends only on
1393:, it follows that
1384:) depends only on
1156:
971:
945:
905:
879:
853:
833:
793:
767:
727:
703:
677:
619:
593:
535:
515:
489:
463:
334:
241:
204:
1547:Hopcroft, John E.
1080:. Then clearly,
856:{\displaystyle P}
730:{\displaystyle e}
538:{\displaystyle Q}
466:{\displaystyle P}
78:Henry Gordon Rice
16:(Redirected from
1643:
1612:
1607:(2nd ed.),
1596:
1587:
1564:
1219:
1141:
980:
978:
977:
972:
954:
952:
951:
946:
944:
943:
931:
930:
914:
912:
911:
906:
888:
886:
885:
880:
862:
860:
859:
854:
842:
840:
839:
834:
832:
831:
819:
818:
802:
800:
799:
794:
776:
774:
773:
768:
766:
765:
753:
752:
736:
734:
733:
728:
712:
710:
709:
704:
686:
684:
683:
678:
667:
666:
645:
644:
628:
626:
625:
620:
602:
600:
599:
594:
583:
582:
561:
560:
544:
542:
541:
536:
524:
522:
521:
516:
498:
496:
495:
490:
472:
470:
469:
464:
352:Given a program
343:
341:
340:
335:
333:
250:
248:
247:
242:
240:
214:. Suppose that:
213:
211:
210:
205:
203:
172:Formal statement
54:statement?"). A
21:
1651:
1650:
1646:
1645:
1644:
1642:
1641:
1640:
1616:
1615:
1542:
1513:Halting problem
1509:
1503:must be false.
1466:
1441:
1432:
1424:. In this case
1392:
1367:
1358:
1350:. In this case
1346:halts on input
1312:
1292:
1241:
1217:
1211:) = "no", with
1202:
1181:halting problem
1174:
1148:
1139:
1124:
1100:halts on input
992:
987:
960:
957:
956:
939:
935:
926:
922:
920:
917:
916:
894:
891:
890:
868:
865:
864:
848:
845:
844:
827:
823:
814:
810:
808:
805:
804:
782:
779:
778:
761:
757:
748:
744:
742:
739:
738:
722:
719:
718:
717:, there exists
692:
689:
688:
662:
658:
640:
636:
634:
631:
630:
608:
605:
604:
578:
574:
556:
552:
550:
547:
546:
530:
527:
526:
504:
501:
500:
478:
475:
474:
458:
455:
454:
451:
391:terminate on 0?
382:halting problem
380:? (This is the
350:
329:
327:
324:
323:
286:
277:
236:
234:
231:
230:
199:
197:
194:
193:
192:be a subset of
174:
128:Turing-complete
94:static analysis
90:
67:static analysis
63:halting problem
28:
23:
22:
15:
12:
11:
5:
1649:
1639:
1638:
1633:
1628:
1614:
1613:
1597:
1578:(2): 358–366,
1565:
1561:Addison-Wesley
1541:
1538:
1537:
1536:
1534:Turing's proof
1531:
1525:
1515:
1508:
1505:
1489:
1488:
1462:
1437:
1428:
1414:
1388:
1363:
1354:
1332:
1331:
1320:
1319:
1318:
1308:
1298:
1288:
1262:) as follows:
1237:
1198:
1170:
1147:
1144:
1134:to obtain our
1114:
991:
988:
986:
983:
970:
967:
964:
942:
938:
934:
929:
925:
904:
901:
898:
878:
875:
872:
852:
830:
826:
822:
817:
813:
792:
789:
786:
764:
760:
756:
751:
747:
726:
702:
699:
696:
676:
673:
670:
665:
661:
657:
654:
651:
648:
643:
639:
618:
615:
612:
592:
589:
586:
581:
577:
573:
570:
567:
564:
559:
555:
534:
514:
511:
508:
488:
485:
482:
462:
450:
447:
446:
445:
434:
427:
420:
413:
392:
385:
349:
346:
332:
305:
304:
282:
273:
252:
239:
202:
173:
170:
166:model checking
144:type inference
89:
86:
36:Rice's theorem
26:
9:
6:
4:
3:
2:
1648:
1637:
1634:
1632:
1629:
1627:
1624:
1623:
1621:
1610:
1606:
1602:
1598:
1595:
1591:
1586:
1581:
1577:
1573:
1572:
1566:
1562:
1558:
1557:
1552:
1548:
1544:
1543:
1535:
1532:
1529:
1526:
1523:
1519:
1516:
1514:
1511:
1510:
1504:
1502:
1498:
1494:
1486:
1482:
1478:
1474:
1470:
1465:
1461:
1457:
1453:
1449:
1445:
1440:
1436:
1431:
1427:
1423:
1419:
1415:
1412:
1408:
1404:
1400:
1396:
1391:
1387:
1383:
1379:
1375:
1371:
1368:and, because
1366:
1362:
1357:
1353:
1349:
1345:
1341:
1340:
1339:
1337:
1329:
1325:
1321:
1316:
1311:
1307:
1303:
1299:
1296:
1291:
1287:
1283:
1280:
1279:
1277:
1273:
1269:
1265:
1264:
1263:
1261:
1257:
1253:
1249:
1245:
1240:
1236:
1232:
1228:
1225:. Now, since
1224:
1220:
1214:
1210:
1206:
1201:
1197:
1193:
1189:
1184:
1182:
1178:
1173:
1169:
1165:
1161:
1152:
1143:
1137:
1133:
1129:
1122:
1118:
1113:
1111:
1107:
1103:
1099:
1095:
1091:
1087:
1083:
1079:
1075:
1071:
1067:
1063:
1059:
1055:
1051:
1047:
1043:
1039:
1035:
1030:
1028:
1024:
1020:
1016:
1011:
1009:
1005:
1001:
997:
982:
968:
965:
962:
940:
936:
932:
927:
923:
902:
899:
896:
876:
873:
870:
850:
828:
824:
820:
815:
811:
790:
787:
784:
762:
758:
754:
749:
745:
724:
716:
700:
697:
694:
671:
663:
659:
655:
649:
641:
637:
616:
613:
610:
587:
579:
575:
571:
565:
557:
553:
532:
512:
509:
506:
486:
483:
480:
460:
443:
439:
435:
432:
428:
425:
421:
418:
414:
411:
408:
404:
401:
398:terminate on
397:
393:
390:
386:
383:
379:
375:
371:
370:
369:
367:
363:
359:
355:
345:
321:
316:
314:
310:
302:
298:
294:
290:
285:
281:
276:
272:
268:
264:
260:
256:
253:
228:
224:
220:
217:
216:
215:
191:
187:
183:
179:
169:
167:
162:
160:
156:
151:
149:
145:
139:
137:
133:
129:
125:
121:
120:certain types
116:
114:
113:specification
110:
105:
103:
99:
95:
85:
83:
79:
74:
72:
68:
64:
59:
57:
53:
49:
45:
41:
37:
33:
19:
1604:
1575:
1569:
1554:
1500:
1496:
1492:
1490:
1484:
1480:
1476:
1472:
1468:
1463:
1459:
1455:
1451:
1447:
1443:
1438:
1434:
1429:
1425:
1421:
1417:
1410:
1406:
1402:
1398:
1394:
1389:
1385:
1381:
1377:
1373:
1369:
1364:
1360:
1355:
1351:
1347:
1343:
1335:
1333:
1327:
1323:
1314:
1309:
1305:
1301:
1294:
1289:
1285:
1281:
1278:) such that
1275:
1271:
1267:
1259:
1255:
1251:
1247:
1243:
1238:
1234:
1230:
1226:
1222:
1216:
1212:
1208:
1204:
1199:
1195:
1191:
1187:
1185:
1171:
1167:
1163:
1157:
1146:Formal proof
1135:
1131:
1127:
1125:
1120:
1119:n×n }
1116:
1109:
1105:
1101:
1097:
1093:
1089:
1085:
1081:
1077:
1073:
1069:
1065:
1061:
1057:
1053:
1049:
1045:
1041:
1037:
1033:
1031:
1026:
1022:
1018:
1014:
1012:
1007:
1006:and returns
1003:
999:
995:
993:
990:Proof sketch
452:
441:
437:
430:
423:
416:
406:
402:
399:
395:
388:
377:
373:
365:
361:
357:
353:
351:
317:
308:
306:
300:
296:
292:
288:
283:
279:
274:
270:
266:
262:
258:
254:
226:
222:
218:
189:
177:
175:
163:
154:
152:
140:
135:
119:
117:
106:
91:
88:Introduction
75:
60:
55:
52:if-then-else
43:
35:
29:
1609:McGraw-Hill
1166:is denoted
777:. Then, if
313:undecidable
259:extensional
223:non-trivial
148:Hoare logic
56:non-trivial
40:undecidable
1620:Categories
1540:References
1413:) = "yes".
1322:2. return
915:, we have
803:, we have
737:such that
405:(i.e., is
320:index sets
126:which are
1487:) = "no".
1140:"Abraxas"
1044:on input
966:∈
937:φ
924:φ
900:∉
874:∉
825:φ
812:φ
788:∈
746:φ
698:∉
660:φ
614:∈
576:φ
510:∉
484:∈
102:semantics
48:terminate
1603:(1987),
1553:(1979),
1507:See also
348:Examples
44:semantic
1611:, §14.8
1594:1990888
1448:no-halt
1439:no-halt
1213:no-halt
1209:no-halt
1160:strings
287:, then
251:itself.
71:correct
1592:
1121:return
1117:return
1048:(both
863:since
188:. Let
180:be an
136:syntax
98:syntax
1590:JSTOR
1300:then
1064:. If
713:. By
687:when
603:when
429:Does
422:Does
415:Does
410:total
394:Does
387:Does
372:Does
307:Then
269:, if
1520:and
1242:and
1128:some
1092:and
1052:and
1017:and
629:and
265:and
176:Let
155:many
109:bugs
42:. A
1580:doi
545:by
436:Is
400:all
311:is
257:is
221:is
184:of
30:In
1622::
1588:,
1576:74
1574:,
1559:,
1549:;
1483:,
1433:=
1409:,
1359:=
1330:).
1297:),
1258:,
1029:.
981:.
412:)?
384:.)
344:.
315:.
299:∈
295:⟺
291:∈
278:=
225::
161:.
150:.
84:.
34:,
1582::
1501:a
1497:a
1495:(
1493:P
1485:i
1481:a
1479:(
1477:H
1473:t
1471:(
1469:P
1464:x
1460:F
1456:x
1454:(
1452:P
1446:(
1444:P
1435:F
1430:t
1426:F
1422:i
1418:a
1411:i
1407:a
1405:(
1403:H
1399:t
1397:(
1395:P
1390:x
1386:F
1382:x
1380:(
1378:P
1374:b
1372:(
1370:P
1365:b
1361:F
1356:t
1352:F
1348:i
1344:a
1336:H
1328:t
1326:(
1324:P
1315:j
1313:(
1310:b
1306:F
1302:T
1295:i
1293:(
1290:a
1286:F
1282:T
1276:j
1274:(
1272:T
1268:t
1260:i
1256:a
1254:(
1252:H
1248:b
1246:(
1244:P
1239:b
1235:F
1231:b
1227:P
1223:P
1218:P
1207:(
1205:P
1200:a
1196:F
1192:a
1190:(
1188:P
1172:a
1168:F
1164:a
1136:t
1132:a
1110:t
1106:t
1102:i
1098:a
1094:i
1090:a
1086:t
1082:t
1078:n
1074:t
1070:i
1068:(
1066:a
1062:n
1058:t
1054:i
1050:a
1046:i
1042:a
1038:n
1034:t
1027:i
1023:a
1019:i
1015:a
1008:d
1004:d
1000:p
996:p
969:P
963:a
941:a
933:=
928:e
903:P
897:e
877:P
871:b
851:P
829:b
821:=
816:e
791:P
785:e
763:e
759:Q
755:=
750:e
725:e
701:P
695:e
675:)
672:x
669:(
664:a
656:=
653:)
650:x
647:(
642:e
638:Q
617:P
611:e
591:)
588:x
585:(
580:b
572:=
569:)
566:x
563:(
558:e
554:Q
533:Q
513:P
507:b
487:P
481:a
461:P
444:?
442:Q
438:P
431:P
424:P
417:P
407:P
403:n
396:P
389:P
378:n
374:P
366:n
364:(
362:P
358:n
354:P
331:N
309:P
303:.
301:P
297:n
293:P
289:m
284:n
280:φ
275:m
271:φ
267:n
263:m
255:P
238:N
227:P
219:P
201:N
190:P
178:φ
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
