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