22:
947:
Instructions of the abstract machine can usually be represented as records. One field of such a record stores an integer tag that identifies the instruction type, other fields may be used for storing additional parameters of the instruction, for example a pointer to another instruction representing a
701:. This also means that we cannot use any universal methods for specializing algorithms, which is usually the case with partial evaluation. Instead, we have to program a specialization procedure for every particular algorithm
597:
There is also an important technical difference. Partial evaluation is applied to algorithms explicitly represented as codes in some programming language. At run-time, we do not need any concrete representation of
1273:, and so on. In such circumstances, full-scale specialization with compilation may not be suitable due to excessive memory usage. However, we can sometimes find a compact specialized representation
1479:
1271:
1212:
1153:
1375:
857:
445:
327:
1420:
1074:
490:
372:
152:
914:
699:
281:
763:
729:
659:
626:
588:
224:
1298:
944:. Then the code itself can be additionally optimized by answer-preserving transformations that rely only on the semantics of instructions of the abstract machine.
51:
1338:
1318:
1094:
1029:
1001:
981:
938:
877:
803:
783:
558:
530:
510:
399:
244:
194:
172:
109:
in optimising program translation. Many core operations in theorem provers exhibit the following pattern. Suppose that we need to execute some algorithm
951:
Interpretation is done by fetching instructions in some order, identifying their type and executing the actions associated with this type. In
94:
is a methodology for creating efficient algorithms for costly computation tasks of certain kinds. The methodology originates in the field of
963:
statement with integer labels from a narrow range rather efficiently by storing the address of the statement corresponding to a value
948:
label, if the semantics of the instruction requires a jump. All instructions of a code can be stored in an array, or list, or tree.
73:
1425:
1591:
1003:-th cell of a special array. One can exploit this by taking values for instruction tags from a small interval of integers.
1494:
1555:
813:
The specialized algorithm has to be represented in a form that can be interpreted. In many situations, usually when
1217:
1158:
1099:
95:
34:
1343:
952:
44:
38:
30:
1499:
816:
404:
286:
1380:
1034:
959:
statement to associate some actions with different instruction tags. Modern compilers usually compile a
450:
332:
112:
99:
55:
882:
667:
249:
738:
704:
634:
601:
563:
199:
1586:
1551:
664:
the specialization procedure. All we need is a concrete representation of the specialized version
1566:
1276:
106:
540:
The key difference between run-time specialization and partial evaluation is that the values of
917:
87:
1533:
1512:
A. Voronkov, "The
Anatomy of Vampire: Implementing Bottom-Up Procedures with Code Trees",
1323:
1303:
1079:
1014:
986:
966:
923:
862:
788:
768:
543:
515:
495:
492:
would have to perform, if they are known to be redundant for this particular parameter
384:
229:
179:
157:
1580:
377:
The specialized algorithm may be more efficient than the generic one, since it can
512:. In particular, we can often identify some tests that are true or false for
1571:
contains the most comprehensive description of the method and many examples
196:. In order to do this efficiently, we can try to find a specialization of
1552:
Efficient
Instance Retrieval with Standard and Relational Path Indexing
1511:
805:, which are beyond the reach of any universal specialization methods.
731:. An important advantage of doing so is that we can use some powerful
1539:
1490:
15:
1096:
in an unpredictable order. For example, we may have to check
1457:
1444:
1438:
1435:
1432:
1392:
1389:
1386:
1362:
1356:
1353:
1350:
1285:
1229:
1226:
1223:
1170:
1167:
1164:
1111:
1108:
1105:
1046:
1043:
1040:
895:
892:
889:
829:
826:
823:
750:
747:
744:
716:
713:
710:
680:
677:
674:
646:
643:
640:
613:
610:
607:
575:
572:
569:
462:
459:
456:
417:
414:
411:
344:
341:
338:
299:
296:
293:
262:
259:
256:
211:
208:
205:
124:
121:
118:
1543:
2004, Lecture Notes in
Artificial Intelligence 3097, 2004 (
1474:{\displaystyle {\mathit {alg}}^{\prime }(A^{\prime },B)}
1545:
compact but self-contained illustration of the method
1536:, "Efficient Checking of Term Ordering Constraints",
1428:
1383:
1346:
1326:
1306:
1279:
1220:
1161:
1102:
1082:
1037:
1017:
989:
969:
926:
885:
865:
819:
791:
771:
741:
707:
670:
637:
604:
566:
546:
518:
498:
453:
407:
387:
335:
289:
252:
232:
202:
182:
160:
115:
1031:
are intended for long-term storage and the calls of
1377:that works on this representation and any call to
1569:, PhD thesis, The University of Manchester, 2003 (
1473:
1414:
1369:
1332:
1312:
1292:
1265:
1206:
1147:
1088:
1068:
1023:
995:
975:
932:
908:
871:
851:
797:
777:
757:
723:
693:
653:
620:
582:
552:
524:
504:
484:
439:
393:
366:
321:
275:
238:
218:
188:
166:
146:
175:is fixed for potentially many different values of
590:is specialised are not known statically, so the
43:but its sources remain unclear because it lacks
8:
1266:{\displaystyle {\mathit {alg}}(A_{1},B_{3})}
1207:{\displaystyle {\mathit {alg}}(A_{2},B_{2})}
1148:{\displaystyle {\mathit {alg}}(A_{1},B_{1})}
1011:There are situations when many instances of
1560:contains another illustration of the method
1567:"Implementing an Efficient Theorem Prover"
1320:, that can be stored with, or instead of,
1456:
1443:
1431:
1430:
1427:
1385:
1384:
1382:
1370:{\displaystyle {\mathit {alg}}^{\prime }}
1361:
1349:
1348:
1345:
1325:
1305:
1284:
1278:
1254:
1241:
1222:
1221:
1219:
1195:
1182:
1163:
1162:
1160:
1136:
1123:
1104:
1103:
1101:
1081:
1039:
1038:
1036:
1016:
988:
968:
925:
900:
888:
887:
884:
864:
834:
822:
821:
818:
790:
770:
743:
742:
740:
709:
708:
706:
685:
673:
672:
669:
639:
638:
636:
606:
605:
603:
568:
567:
565:
545:
517:
497:
455:
454:
452:
422:
410:
409:
406:
386:
337:
336:
334:
304:
292:
291:
288:
267:
255:
254:
251:
231:
204:
203:
201:
181:
159:
117:
116:
114:
74:Learn how and when to remove this message
1493:, a specializing run-time compiler for
1481:, intended to do the same job faster.
852:{\displaystyle {\mathit {alg}}_{A}(B)}
592:specialization takes place at run-time
440:{\displaystyle {\mathit {alg}}_{A}(B)}
322:{\displaystyle {\mathit {alg}}_{A}(B)}
7:
1415:{\displaystyle {\mathit {alg}}(A,B)}
1069:{\displaystyle {\mathit {alg}}(A,B)}
485:{\displaystyle {\mathit {alg}}(A,B)}
367:{\displaystyle {\mathit {alg}}(A,B)}
147:{\displaystyle {\mathit {alg}}(A,B)}
909:{\displaystyle {\mathit {alg}}_{A}}
735:tricks exploiting peculiarities of
694:{\displaystyle {\mathit {alg}}_{A}}
532:, unroll loops and recursion, etc.
276:{\displaystyle {\mathit {alg}}_{A}}
105:The idea is inspired by the use of
536:Difference from partial evaluation
379:exploit some particular properties
14:
1007:Data-and-algorithm specialization
859:is to be computed on many values
92:run-time algorithm specialization
154:in a situation where a value of
20:
809:Specialization with compilation
758:{\displaystyle {\mathit {alg}}}
724:{\displaystyle {\mathit {alg}}}
654:{\displaystyle {\mathit {alg}}}
621:{\displaystyle {\mathit {alg}}}
583:{\displaystyle {\mathit {alg}}}
447:can avoid some operations that
219:{\displaystyle {\mathit {alg}}}
98:and, more specifically, in the
1514:Journal of Automated Reasoning
1468:
1449:
1409:
1397:
1260:
1234:
1201:
1175:
1142:
1116:
1063:
1051:
846:
840:
479:
467:
434:
428:
361:
349:
316:
310:
141:
129:
1:
1550:A. Riazanov and A. Voronkov,
1340:. We also define a variant
1556:Information and Computation
1293:{\displaystyle A^{\prime }}
329:is equivalent to executing
1608:
765:and the representation of
246:, i.e., such an algorithm
96:automated theorem proving
920:, and we often say that
29:This article includes a
1500:multi-stage programming
916:as a code of a special
879:in a row, we can write
58:more precise citations.
1475:
1416:
1371:
1334:
1314:
1294:
1267:
1208:
1149:
1090:
1070:
1025:
997:
977:
934:
910:
873:
853:
799:
779:
759:
725:
695:
655:
622:
584:
554:
526:
506:
486:
441:
395:
368:
323:
277:
240:
220:
190:
168:
148:
100:Vampire theorem prover
1592:Software optimization
1476:
1417:
1372:
1335:
1315:
1295:
1268:
1209:
1150:
1091:
1076:occur with different
1071:
1026:
998:
978:
935:
911:
874:
854:
800:
780:
760:
726:
696:
656:
623:
585:
555:
527:
507:
487:
442:
396:
369:
324:
278:
241:
221:
191:
169:
149:
1426:
1381:
1344:
1324:
1304:
1277:
1218:
1159:
1100:
1080:
1035:
1015:
987:
967:
955:or C++ we can use a
924:
883:
863:
817:
789:
769:
739:
705:
668:
635:
602:
564:
544:
516:
496:
451:
405:
385:
333:
287:
250:
230:
200:
180:
158:
113:
381:of the fixed value
1558:, 199(1-2), 2005 (
1471:
1412:
1367:
1330:
1310:
1290:
1263:
1204:
1145:
1086:
1066:
1021:
993:
973:
930:
906:
869:
849:
795:
775:
755:
721:
691:
651:
628:. We only have to
618:
580:
550:
522:
502:
482:
437:
391:
364:
319:
273:
236:
216:
186:
164:
144:
107:partial evaluation
31:list of references
1333:{\displaystyle A}
1313:{\displaystyle A}
1089:{\displaystyle B}
1024:{\displaystyle A}
996:{\displaystyle i}
976:{\displaystyle i}
933:{\displaystyle A}
872:{\displaystyle B}
798:{\displaystyle B}
778:{\displaystyle A}
553:{\displaystyle A}
525:{\displaystyle A}
505:{\displaystyle A}
394:{\displaystyle A}
283:, that executing
239:{\displaystyle A}
189:{\displaystyle B}
167:{\displaystyle A}
84:
83:
76:
1599:
1532:A. Riazanov and
1480:
1478:
1477:
1472:
1461:
1460:
1448:
1447:
1442:
1441:
1421:
1419:
1418:
1413:
1396:
1395:
1376:
1374:
1373:
1368:
1366:
1365:
1360:
1359:
1339:
1337:
1336:
1331:
1319:
1317:
1316:
1311:
1299:
1297:
1296:
1291:
1289:
1288:
1272:
1270:
1269:
1264:
1259:
1258:
1246:
1245:
1233:
1232:
1213:
1211:
1210:
1205:
1200:
1199:
1187:
1186:
1174:
1173:
1154:
1152:
1151:
1146:
1141:
1140:
1128:
1127:
1115:
1114:
1095:
1093:
1092:
1087:
1075:
1073:
1072:
1067:
1050:
1049:
1030:
1028:
1027:
1022:
1002:
1000:
999:
994:
982:
980:
979:
974:
939:
937:
936:
931:
918:abstract machine
915:
913:
912:
907:
905:
904:
899:
898:
878:
876:
875:
870:
858:
856:
855:
850:
839:
838:
833:
832:
804:
802:
801:
796:
784:
782:
781:
776:
764:
762:
761:
756:
754:
753:
730:
728:
727:
722:
720:
719:
700:
698:
697:
692:
690:
689:
684:
683:
660:
658:
657:
652:
650:
649:
627:
625:
624:
619:
617:
616:
589:
587:
586:
581:
579:
578:
559:
557:
556:
551:
531:
529:
528:
523:
511:
509:
508:
503:
491:
489:
488:
483:
466:
465:
446:
444:
443:
438:
427:
426:
421:
420:
400:
398:
397:
392:
373:
371:
370:
365:
348:
347:
328:
326:
325:
320:
309:
308:
303:
302:
282:
280:
279:
274:
272:
271:
266:
265:
245:
243:
242:
237:
226:for every fixed
225:
223:
222:
217:
215:
214:
195:
193:
192:
187:
173:
171:
170:
165:
153:
151:
150:
145:
128:
127:
88:computer science
79:
72:
68:
65:
59:
54:this article by
45:inline citations
24:
23:
16:
1607:
1606:
1602:
1601:
1600:
1598:
1597:
1596:
1577:
1576:
1529:
1527:Further reading
1508:
1487:
1452:
1429:
1424:
1423:
1422:is replaced by
1379:
1378:
1347:
1342:
1341:
1322:
1321:
1302:
1301:
1280:
1275:
1274:
1250:
1237:
1216:
1215:
1191:
1178:
1157:
1156:
1132:
1119:
1098:
1097:
1078:
1077:
1033:
1032:
1013:
1012:
1009:
985:
984:
965:
964:
922:
921:
886:
881:
880:
861:
860:
820:
815:
814:
811:
787:
786:
767:
766:
737:
736:
703:
702:
671:
666:
665:
662:when we program
633:
632:
600:
599:
562:
561:
542:
541:
538:
514:
513:
494:
493:
449:
448:
408:
403:
402:
383:
382:
331:
330:
290:
285:
284:
253:
248:
247:
228:
227:
198:
197:
178:
177:
156:
155:
111:
110:
80:
69:
63:
60:
49:
35:related reading
25:
21:
12:
11:
5:
1605:
1603:
1595:
1594:
1589:
1579:
1578:
1575:
1574:
1563:
1548:
1528:
1525:
1524:
1523:
1507:
1504:
1503:
1502:
1497:
1486:
1483:
1470:
1467:
1464:
1459:
1455:
1451:
1446:
1440:
1437:
1434:
1411:
1408:
1405:
1402:
1399:
1394:
1391:
1388:
1364:
1358:
1355:
1352:
1329:
1309:
1287:
1283:
1262:
1257:
1253:
1249:
1244:
1240:
1236:
1231:
1228:
1225:
1203:
1198:
1194:
1190:
1185:
1181:
1177:
1172:
1169:
1166:
1144:
1139:
1135:
1131:
1126:
1122:
1118:
1113:
1110:
1107:
1085:
1065:
1062:
1059:
1056:
1053:
1048:
1045:
1042:
1020:
1008:
1005:
992:
972:
929:
903:
897:
894:
891:
868:
848:
845:
842:
837:
831:
828:
825:
810:
807:
794:
774:
752:
749:
746:
718:
715:
712:
688:
682:
679:
676:
648:
645:
642:
615:
612:
609:
577:
574:
571:
549:
537:
534:
521:
501:
481:
478:
475:
472:
469:
464:
461:
458:
436:
433:
430:
425:
419:
416:
413:
390:
363:
360:
357:
354:
351:
346:
343:
340:
318:
315:
312:
307:
301:
298:
295:
270:
264:
261:
258:
235:
213:
210:
207:
185:
163:
143:
140:
137:
134:
131:
126:
123:
120:
82:
81:
39:external links
28:
26:
19:
13:
10:
9:
6:
4:
3:
2:
1604:
1593:
1590:
1588:
1585:
1584:
1582:
1572:
1568:
1565:A. Riazanov,
1564:
1561:
1557:
1553:
1549:
1546:
1542:
1541:
1535:
1531:
1530:
1526:
1521:
1520:original idea
1517:
1516:, 15(2), 1995
1515:
1510:
1509:
1505:
1501:
1498:
1496:
1492:
1489:
1488:
1484:
1482:
1465:
1462:
1453:
1406:
1403:
1400:
1327:
1307:
1281:
1255:
1251:
1247:
1242:
1238:
1196:
1192:
1188:
1183:
1179:
1137:
1133:
1129:
1124:
1120:
1083:
1060:
1057:
1054:
1018:
1006:
1004:
990:
970:
962:
958:
954:
949:
945:
943:
927:
919:
901:
866:
843:
835:
808:
806:
792:
772:
734:
686:
663:
631:
595:
593:
547:
535:
533:
519:
499:
476:
473:
470:
431:
423:
401:. Typically,
388:
380:
375:
358:
355:
352:
313:
305:
268:
233:
183:
176:
161:
138:
135:
132:
108:
103:
101:
97:
93:
89:
78:
75:
67:
64:November 2023
57:
53:
47:
46:
40:
36:
32:
27:
18:
17:
1570:
1559:
1544:
1537:
1519:
1513:
1155:first, then
1010:
960:
956:
950:
946:
941:
812:
732:
661:
629:
596:
591:
539:
378:
376:
174:
104:
91:
85:
70:
61:
50:Please help
42:
1534:A. Voronkov
56:introducing
1587:Algorithms
1581:Categories
1506:References
1300:for every
1458:′
1445:′
1363:′
1286:′
560:on which
102:project.
1485:See also
942:compiled
1214:, then
983:in the
630:imagine
52:improve
1538:Proc.
1495:Python
961:switch
957:switch
733:ad hoc
1540:IJCAR
1491:Psyco
37:, or
785:and
940:is
86:In
1583::
1554:,
594:.
374:.
90:,
41:,
33:,
1573:)
1562:)
1547:)
1522:)
1518:(
1469:)
1466:B
1463:,
1454:A
1450:(
1439:g
1436:l
1433:a
1410:)
1407:B
1404:,
1401:A
1398:(
1393:g
1390:l
1387:a
1357:g
1354:l
1351:a
1328:A
1308:A
1282:A
1261:)
1256:3
1252:B
1248:,
1243:1
1239:A
1235:(
1230:g
1227:l
1224:a
1202:)
1197:2
1193:B
1189:,
1184:2
1180:A
1176:(
1171:g
1168:l
1165:a
1143:)
1138:1
1134:B
1130:,
1125:1
1121:A
1117:(
1112:g
1109:l
1106:a
1084:B
1064:)
1061:B
1058:,
1055:A
1052:(
1047:g
1044:l
1041:a
1019:A
991:i
971:i
953:C
928:A
902:A
896:g
893:l
890:a
867:B
847:)
844:B
841:(
836:A
830:g
827:l
824:a
793:B
773:A
751:g
748:l
745:a
717:g
714:l
711:a
687:A
681:g
678:l
675:a
647:g
644:l
641:a
614:g
611:l
608:a
576:g
573:l
570:a
548:A
520:A
500:A
480:)
477:B
474:,
471:A
468:(
463:g
460:l
457:a
435:)
432:B
429:(
424:A
418:g
415:l
412:a
389:A
362:)
359:B
356:,
353:A
350:(
345:g
342:l
339:a
317:)
314:B
311:(
306:A
300:g
297:l
294:a
269:A
263:g
260:l
257:a
234:A
212:g
209:l
206:a
184:B
162:A
142:)
139:B
136:,
133:A
130:(
125:g
122:l
119:a
77:)
71:(
66:)
62:(
48:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.