169:
990:
different representations of such terms. On the other hand, the named representation of λ-terms is more pervasive and can be more immediately understandable by others because the variables can be given descriptive names. Thus, even if a system uses de Bruijn indices internally, it will present a user interface with names.
956:
993:
An alternative way to view de Bruijn indices is as de Bruijn levels, which indexes variables from the bottom of the stack rather than from the top. This eliminates the need to reindex free variables, for example when weakening the context, whereas de Bruijn indices eliminate the need to reindex bound
1054:
In the general context of an inductive definition, it is not possible to apply α-conversion as needed to convert an inductive definition using the convention to one where the convention is not used, because a variable may appear in both a binding position and a non-binding position in the rule. The
430:
After step 1, we obtain the term λ 4 □ (λ 1 □), where the variables that are destined for substitution are replaced with boxes. Step 2 decrements the free variables, giving λ 3 □ (λ 1 □). Finally, in step 3, we replace the boxes with the argument, namely λ 5 1; the first box is under one binder, so
989:
When using the standard "named" representation of λ-terms, where variables are treated as labels or strings, one must explicitly handle α-conversion when defining any operation on the terms. In practice this is cumbersome, inefficient, and often error-prone. It has therefore led to the search for
694:
1031:
uses a mixed representation of variables—de Bruijn indices for bound variables and names for free variables—that is able to benefit from the α-canonical form of de Bruijn indexed terms when appropriate.
699:
431:
we replace it with λ 6 1 (which is λ 5 1 with the free variables increased by 1); the second is under two binders, so we replace it with λ 7 1. The final result is λ 3 (λ 6 1) (λ 1 (λ 7 1)).
545:
1016:
where the λ-binder is treated as a true function. In such representations, the issues of α-equivalence, substitution, etc. are identified with the same operations in a
951:{\displaystyle {\begin{aligned}n=&N_{n}\\(M_{1}\;M_{2})=&(M_{1})(M_{2})\\(\lambda \;M)=&\lambda \;(M)\\&{\text{where }}s'=s\uparrow ^{1}\end{aligned}}}
1367:
1160:
1199:
1437:
1397:
19:
This article is about a method for avoiding naming bound variables in lambda calculus. For an alternative syntax for lambda expressions, see
1109:"Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem"
1133:
997:
De Bruijn indices are not the only representation of λ-terms that obviates the problem of α-conversion. Among named representations, the
168:
1027:, it is sometimes desirable to limit oneself to first-order representations and to have the ability to name or rename assumptions. The
65:
1173:
1361:
163:) is λ (λ 1 (λ 1)) (λ 2 1). See the following illustration, where the binders are colored and the references are shown with arrows.
1293:
1443:
1066:
assuming the premises of the rule, the variables in binding positions in the rule are distinct and are free in the conclusion
1001:
of Pitts and Gabbay is one approach, where the representation of a λ-term is treated as an equivalence class of all terms
1343:
1013:
1336:
1227:
475:
1116:
1104:
179:
41:
1264:
1191:
1466:
1006:
61:
275:
48:
without naming the bound variables. Terms written using these indices are invariant with respect to
592:.(n+1).(n+2)... leaving all variables greater than n unchanged. The application of a substitution
268:
69:
1345:
Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on
Principles of programming languages
1063:
in the sense of nominal logic, that is to say that its validity is unchanged by renaming variables
1328:
1077:
998:
175:
27:
20:
362:
each time, to match the number of λ-binders, under which the corresponding variable occurs when
206:, ...) written using de Bruijn indices have the following syntax (parentheses allowed freely):
1433:
1393:
1357:
1332:
1246:
1125:
1108:
1083:
550:
For example, ↑ is the identity substitution, leaving a term unchanged. A finite list of terms
183:
1005:
to it using variable permutations. This approach is taken by the
Nominal Datatype Package of
1425:
1349:
1302:
1236:
1165:
1151:
1381:
1024:
53:
45:
49:
1414:
1310:
469:
is a natural number indicating the amount to increase the variables, and is defined by
279:
248:
240:
72:
between that occurrence and its corresponding binder. The following are some examples:
57:
1241:
1222:
1460:
1389:
1289:
256:
195:
38:
961:
The steps outlined for the β-reduction above are thus more concisely expressed as:
126:
89:
1043:
is a convention commonly used in proofs and definitions where it is assumed that:
994:
variables, for example when substituting a closed expression in another context.
1429:
1060:
1055:
induction principle holds if every rule satisfies the following two conditions:
35:
1023:
When reasoning about the meta-theoretic properties of a deductive system in a
1017:
1250:
1169:
1129:
1353:
1306:
1002:
92:, is written as λ λ 2 with de Bruijn indices. The binder for the occurrence
385:
which might correspond to the following term written in the usual notation
461:
th free variable. The increasing operation in step 3 is sometimes called
1268:
56:
is the same as that for syntactic equality. Each de Bruijn index is a
1424:. Lecture Notes in Computer Science. Vol. 4603. pp. 35–50.
434:
Formally, a substitution is an unbounded list of terms, written
1413:
Urban, Christian; Berghofer, Stefan; Norrish, Michael (2007).
278:: replacing free variables in a term with other terms. In the
1223:"Nominal Logic: A First Order Theory of Names and Binding"
1295:
Functional Pearl: I am not a Number—I am a Free
Variable
358:, suitably incrementing the free variables occurring in
1415:"Barendregt's Variable Convention in Rule Inductions"
1348:. New York, New York, USA: ACM Press. pp. 3–15.
1152:"A New Approach to Abstract Syntax Involving Binders"
1047:
bound variables are distinct from free variables, and
697:
478:
1086:, a more essential way to eliminate variable names.
243:greater than 0—are the variables. A variable
950:
539:
688:and substitution is defined on terms as follows:
1050:all binders bind variables not already in scope.
330:to match the removal of the outer λ-binder, and
129:), with de Bruijn indices, is λ λ λ 3 1 (2 1).
1386:The Lambda Calculus: Its Syntax and Semantics
540:{\displaystyle \uparrow ^{k}=(k+1).(k+2)....}
8:
1192:"How to implement dependent type theory III"
1161:IEEE Symposium on Logic in Computer Science
1150:Gabbay, Murdoch J.; Pitts, Andy M. (1999).
1012:Another common alternative is an appeal to
274:The most primitive operation on λ-terms is
883:
859:
769:
1240:
938:
915:
831:
806:
774:
763:
746:
725:
712:
698:
696:
483:
477:
377:To illustrate, consider the application
271:of, starting from the innermost binder.
16:Mathematical notation in lambda calculus
1096:
604:. The composition of two substitutions
174:De Bruijn indices are commonly used in
64:in a λ-term, and denotes the number of
1301:. New York, New York, USA: ACM Press.
1327:Aydemir, Brian; Charguéraud, Arthur;
7:
294:find the instances of the variables
1035:
60:that represents an occurrence of a
259:. The binding site for a variable
251:if it is in the scope of at least
14:
1036:Barendregt's variable convention
985:Alternatives to de Bruijn indices
1449:from the original on 2017-07-06.
1370:from the original on 2010-07-27.
1179:from the original on 2004-07-27.
1139:from the original on 2011-05-20.
1041:Barendregt's variable convention
326:decrement the free variables of
167:
1337:"Engineering formal metatheory"
1202:from the original on 2016-08-07
935:
907:
904:
890:
884:
872:
866:
863:
853:
846:
843:
837:
824:
821:
818:
812:
799:
789:
783:
780:
756:
734:
705:
522:
510:
504:
492:
480:
1:
1422:Automated Deduction – CADE-21
1242:10.1016/S0890-5401(03)00138-X
571:abbreviates the substitution
319:that are bound by the λ in λ
255:binders (λ); otherwise it is
1014:higher-order representations
1430:10.1007/978-3-540-73595-3_4
1265:"Nominal Isabelle web-site"
1228:Information and Computation
1196:Mathematics and Computation
457:is the replacement for the
366:substitutes for one of the
1483:
1382:Barendregt, Hendrik Pieter
1105:de Bruijn, Nicolaas Govert
178:reasoning systems such as
44:for representing terms of
34:is a tool invented by the
18:
1329:Pierce, Benjamin Crawford
1292:; McKinna, James (2004).
1117:Indagationes Mathematicae
1029:locally nameless approach
381:(λ λ 4 2 (λ 1 3)) (λ 5 1)
180:automated theorem provers
96:is the second λ in scope.
42:Nicolaas Govert de Bruijn
1170:10.1109/LICS.1999.782617
673:satisfying the property
1354:10.1145/1328438.1328443
1307:10.1145/1017472.1017477
1221:Pitts, Andy M. (2003).
290:, for example, we must
267:th binder it is in the
88:, sometimes called the
959:
952:
541:
953:
690:
542:
1164:. pp. 214–224.
695:
476:
465:and written ↑ where
52:, so the check for
1333:Weirich, Stephanie
1331:; Pollack, Randy;
1078:de Bruijn notation
999:nominal techniques
948:
946:
633:and is defined by
537:
28:mathematical logic
21:De Bruijn notation
1439:978-3-540-73594-6
1399:978-0-444-87508-2
1084:Combinatory logic
918:
190:Formal definition
184:logic programming
1474:
1451:
1450:
1448:
1419:
1410:
1404:
1403:
1378:
1372:
1371:
1341:
1324:
1318:
1317:
1315:
1309:. Archived from
1300:
1286:
1280:
1279:
1277:
1276:
1267:. Archived from
1261:
1255:
1254:
1244:
1218:
1212:
1211:
1209:
1207:
1187:
1181:
1180:
1178:
1156:
1147:
1141:
1140:
1138:
1113:
1101:
957:
955:
954:
949:
947:
943:
942:
927:
919:
916:
913:
903:
836:
835:
811:
810:
779:
778:
768:
767:
751:
750:
730:
729:
717:
716:
546:
544:
543:
538:
488:
487:
171:
1482:
1481:
1477:
1476:
1475:
1473:
1472:
1471:
1467:Lambda calculus
1457:
1456:
1455:
1454:
1446:
1440:
1417:
1412:
1411:
1407:
1400:
1380:
1379:
1375:
1364:
1339:
1326:
1325:
1321:
1313:
1298:
1288:
1287:
1283:
1274:
1272:
1263:
1262:
1258:
1220:
1219:
1215:
1205:
1203:
1190:Bauer, Andrej.
1189:
1188:
1184:
1176:
1154:
1149:
1148:
1144:
1136:
1111:
1103:
1102:
1098:
1093:
1073:
1038:
1025:proof assistant
987:
976:
945:
944:
934:
920:
911:
910:
896:
878:
850:
849:
827:
802:
795:
770:
759:
753:
752:
742:
740:
721:
708:
693:
692:
668:
661:
650:
643:
632:
626:
619:
612:
591:
584:
577:
570:
563:
556:
479:
474:
473:
456:
447:
440:
371:
353:
346:
339:
314:
307:
300:
241:natural numbers
217:, ... ::=
192:
46:lambda calculus
32:de Bruijn index
24:
17:
12:
11:
5:
1480:
1478:
1470:
1469:
1459:
1458:
1453:
1452:
1438:
1405:
1398:
1392:. p. 26.
1373:
1362:
1319:
1316:on 2013-09-28.
1290:McBride, Conor
1281:
1256:
1235:(2): 165–193.
1213:
1182:
1142:
1095:
1094:
1092:
1089:
1088:
1087:
1081:
1072:
1069:
1068:
1067:
1064:
1052:
1051:
1048:
1037:
1034:
986:
983:
982:
981:
974:
941:
937:
933:
930:
926:
923:
914:
912:
909:
906:
902:
899:
895:
892:
889:
886:
882:
879:
877:
874:
871:
868:
865:
862:
858:
855:
852:
851:
848:
845:
842:
839:
834:
830:
826:
823:
820:
817:
814:
809:
805:
801:
798:
796:
794:
791:
788:
785:
782:
777:
773:
766:
762:
758:
755:
754:
749:
745:
741:
739:
736:
733:
728:
724:
720:
715:
711:
707:
704:
701:
700:
686:
685:
671:
670:
666:
659:
648:
641:
630:
624:
617:
608:
589:
582:
575:
568:
561:
554:
548:
547:
536:
533:
530:
527:
524:
521:
518:
515:
512:
509:
506:
503:
500:
497:
494:
491:
486:
482:
452:
445:
438:
428:
427:
383:
382:
375:
374:
369:
351:
344:
337:
331:
324:
312:
305:
298:
233:
232:
191:
188:
165:
164:
130:
97:
58:natural number
15:
13:
10:
9:
6:
4:
3:
2:
1479:
1468:
1465:
1464:
1462:
1445:
1441:
1435:
1431:
1427:
1423:
1416:
1409:
1406:
1401:
1395:
1391:
1390:North Holland
1387:
1383:
1377:
1374:
1369:
1365:
1363:9781595936899
1359:
1355:
1351:
1347:
1346:
1338:
1334:
1330:
1323:
1320:
1312:
1308:
1304:
1297:
1296:
1291:
1285:
1282:
1271:on 2014-12-14
1270:
1266:
1260:
1257:
1252:
1248:
1243:
1238:
1234:
1230:
1229:
1224:
1217:
1214:
1201:
1197:
1193:
1186:
1183:
1175:
1171:
1167:
1163:
1162:
1153:
1146:
1143:
1135:
1131:
1127:
1123:
1119:
1118:
1110:
1106:
1100:
1097:
1090:
1085:
1082:
1079:
1075:
1074:
1070:
1065:
1062:
1058:
1057:
1056:
1049:
1046:
1045:
1044:
1042:
1033:
1030:
1026:
1021:
1019:
1015:
1010:
1008:
1004:
1000:
995:
991:
984:
979:
972:
968:
964:
963:
962:
958:
939:
931:
928:
924:
921:
900:
897:
893:
887:
880:
875:
869:
860:
856:
840:
832:
828:
815:
807:
803:
797:
792:
786:
775:
771:
764:
760:
747:
743:
737:
731:
726:
722:
718:
713:
709:
702:
689:
683:
679:
676:
675:
674:
665:
658:
654:
647:
640:
636:
635:
634:
629:
623:
616:
611:
607:
603:
599:
595:
588:
581:
574:
567:
560:
553:
534:
531:
528:
525:
519:
516:
513:
507:
501:
498:
495:
489:
484:
472:
471:
470:
468:
464:
460:
455:
451:
444:
437:
432:
425:
422:
418:
414:
411:
407:
403:
400:
396:
392:
388:
387:
386:
380:
379:
378:
372:
365:
361:
357:
350:
343:
336:
332:
329:
325:
322:
318:
311:
304:
297:
293:
292:
291:
289:
285:
281:
277:
272:
270:
266:
262:
258:
254:
250:
246:
242:
238:
231:
227:
224:
220:
216:
212:
209:
208:
207:
205:
201:
197:
189:
187:
185:
181:
177:
172:
170:
162:
159:
155:
151:
147:
143:
139:
135:
131:
128:
124:
121:
117:
114:
110:
106:
102:
98:
95:
91:
87:
83:
79:
75:
74:
73:
71:
67:
63:
59:
55:
54:α-equivalence
51:
47:
43:
40:
39:mathematician
37:
33:
29:
22:
1421:
1408:
1385:
1376:
1344:
1322:
1311:the original
1294:
1284:
1273:. Retrieved
1269:the original
1259:
1232:
1226:
1216:
1204:. Retrieved
1195:
1185:
1159:14th Annual
1158:
1145:
1121:
1115:
1099:
1080:for λ-terms.
1059:the rule is
1053:
1040:
1039:
1028:
1022:
1011:
1007:Isabelle/HOL
996:
992:
988:
977:
970:
966:
960:
691:
687:
681:
677:
672:
663:
656:
652:
645:
638:
627:
621:
614:
609:
605:
601:
597:
593:
586:
579:
572:
565:
558:
551:
549:
466:
462:
458:
453:
449:
442:
435:
433:
429:
423:
420:
416:
412:
409:
405:
401:
398:
394:
390:
384:
376:
367:
363:
359:
355:
348:
341:
334:
327:
320:
316:
309:
302:
295:
287:
283:
276:substitution
273:
264:
260:
252:
244:
236:
234:
229:
225:
222:
218:
214:
210:
203:
199:
193:
176:higher-order
173:
166:
160:
157:
153:
149:
145:
141:
137:
133:
127:S combinator
122:
119:
115:
112:
108:
104:
100:
93:
90:K combinator
85:
81:
77:
68:that are in
50:α-conversion
31:
25:
1124:: 381–392.
1061:equivariant
917:where
620:is written
600:is written
448:..., where
280:β-reduction
1275:2007-03-28
1206:20 October
1091:References
1018:meta-logic
1003:rewritable
596:to a term
194:Formally,
132:The term λ
99:The term λ
76:The term λ
1251:0890-5401
1130:0019-3577
936:↑
881:λ
857:λ
732:…
719:…
481:↑
186:systems.
1461:Category
1444:Archived
1384:(1984).
1368:Archived
1335:(2008).
1200:Archived
1174:Archived
1134:Archived
1107:(1972).
1071:See also
925:′
901:′
333:replace
62:variable
347:, ...,
308:, ...,
263:is the
239:—
196:λ-terms
125:) (the
66:binders
1436:
1396:
1360:
1249:
1128:
235:where
30:, the
1447:(PDF)
1418:(PDF)
1340:(PDF)
1314:(PDF)
1299:(PDF)
1177:(PDF)
1155:(PDF)
1137:(PDF)
1112:(PDF)
651:...)
463:shift
415:)) (λ
354:with
269:scope
249:bound
152:)) (λ
70:scope
36:Dutch
1434:ISBN
1394:ISBN
1358:ISBN
1247:ISSN
1208:2021
1126:ISSN
1076:The
613:and
257:free
228:| λ
182:and
136:. (λ
1426:doi
1350:doi
1303:doi
1237:doi
1233:186
1166:doi
965:(λ
684:) ,
680:= (
669:...
585:...
564:...
393:. λ
315:in
282:(λ
247:is
107:. λ
103:. λ
80:. λ
26:In
1463::
1442:.
1432:.
1420:.
1388:.
1366:.
1356:.
1342:.
1245:.
1231:.
1225:.
1198:.
1194:.
1172:.
1157:.
1132:.
1122:34
1120:.
1114:.
1020:.
1009:.
969:)
894:1.
655:=
426:).
419:.
408:.
404:(λ
397:.
389:(λ
340:,
301:,
286:)
221:|
213:,
202:,
156:.
148:.
144:(λ
140:.
111:.
84:.
1428::
1402:.
1352::
1305::
1278:.
1253:.
1239::
1210:.
1168::
980:.
978:M
975:β
973:→
971:N
967:M
940:1
932:s
929:=
922:s
908:)
905:]
898:s
891:[
888:M
885:(
876:=
873:]
870:s
867:[
864:)
861:M
854:(
847:)
844:]
841:s
838:[
833:2
829:M
825:(
822:)
819:]
816:s
813:[
808:1
804:M
800:(
793:=
790:]
787:s
784:[
781:)
776:2
772:M
765:1
761:M
757:(
748:n
744:N
738:=
735:]
727:n
723:N
714:1
710:N
706:[
703:n
682:M
678:M
667:2
664:M
662:.
660:1
657:M
653:s
649:2
646:M
644:.
642:1
639:M
637:(
631:2
628:s
625:1
622:s
618:2
615:s
610:1
606:s
602:M
598:M
594:s
590:n
587:M
583:2
580:M
578:.
576:1
573:M
569:n
566:M
562:2
559:M
557:.
555:1
552:M
535:.
532:.
529:.
526:.
523:)
520:2
517:+
514:k
511:(
508:.
505:)
502:1
499:+
496:k
493:(
490:=
485:k
467:k
459:i
454:i
450:M
446:2
443:M
441:.
439:1
436:M
424:x
421:w
417:x
413:x
410:u
406:u
402:x
399:z
395:y
391:x
373:.
370:i
368:n
364:N
360:N
356:N
352:k
349:n
345:2
342:n
338:1
335:n
328:M
323:,
321:M
317:M
313:k
310:n
306:2
303:n
299:1
296:n
288:N
284:M
265:n
261:n
253:n
245:n
237:n
230:M
226:N
223:M
219:n
215:N
211:M
204:N
200:M
198:(
161:x
158:z
154:x
150:x
146:x
142:y
138:y
134:z
123:z
120:y
118:(
116:z
113:x
109:z
105:y
101:x
94:x
86:x
82:y
78:x
23:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
