Languages Features Creators Calendar CSV Resources Blog About Pricing Add Language
GitHub icon

De Bruijn index

De Bruijn index - Notation

< >

De Bruijn index is a notation created in 1972 by Nicolaas Govert de Bruijn.

#1615on PLDB 51Years Old 250Users
0Books 0Papers

In mathematical logic, the de Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bound variables. Terms written using these indices are invariant with respect to 伪-conversion, so the check for 伪-equivalence is the same as that for syntactic equality. Each de Bruijn index is a natural number that represents an occurrence of a variable in a 位-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. Read more on Wikipedia...

Example from the web:
位 位 位 3 1 (2 1)
tmtp.html 路 de-bruijn-index-notation.html 路 pro-star-c.html

View source

- Build the next great programming language Search v2023 Day 205 Docs Acknowledgements Traffic Traffic Today Mirrors GitHub