| dbo:abstract |
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. The following are some examples: * The term λx. λy. x, sometimes called the K combinator, is written as λ λ 2 with De Bruijn indices. The binder for the occurrence x is the second λ in scope. * The term λx. λy. λz. x z (y z) (the S combinator), with De Bruijn indices, is λ λ λ 3 1 (2 1). * The term λz. (λy. y (λx. x)) (λx. z x) is λ (λ 1 (λ 1)) (λ 2 1). See the following illustration, where the binders are coloured and the references are shown with arrows. De Bruijn indices are commonly used in higher-order reasoning systems such as automated theorem provers and logic programming systems. (en) ド・ブラウン・インデックス（英語: de Bruijn Index）とは、ラムダ計算において、名前を使わずに引数（束縛変数）を参照するための記法である。オランダ人数学者ニコラース・ホーヴァート・ド・ブラウンによって発明された。 (ja) |
| dbo:thumbnail |
wiki-commons:Special:FilePath/De_Bruijn_index_illustration_1.svg?width=300 |
| dbo:wikiPageID |
10314482 (xsd:integer) |
| dbo:wikiPageLength |
12718 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID |
1123617511 (xsd:integer) |
| dbo:wikiPageWikiLink |
dbr:Proof_assistant dbc:Lambda_calculus dbr:De_Bruijn_notation dbr:K_combinator dbr:Combinatory_logic dbr:Mathematical_logic dbr:Nominal_techniques dbr:Rewriting dbr:Free_variables_and_bound_variables dbr:Substitution_(logic) dbr:Mathematician dbr:Automated_theorem_proving dbr:Logic_programming dbr:Nicolaas_Govert_de_Bruijn dbr:Equivariant dbr:Free_variable dbr:Lambda_calculus dbr:Higher-order_abstract_syntax dbr:Higher-order_logic dbr:Meta-logic dbr:Natural_number dbr:Netherlands dbr:Bound_variable dbr:S_combinator dbr:Variable_(mathematics) dbr:Isabelle_theorem_prover dbr:Scope_(programming) dbr:Β-reduction dbr:Λ_calculus dbr:Α-conversion dbr:File:De_Bruijn_index_illustration_1.svg |
| dbp:wikiPageUsesTemplate |
dbt:About dbt:Reflist dbt:Short_description |
| dcterms:subject |
dbc:Lambda_calculus |
| gold:hypernym |
dbr:Notation |
| rdf:type |
dbo:Software |
| rdfs:comment |
ド・ブラウン・インデックス（英語: de Bruijn Index）とは、ラムダ計算において、名前を使わずに引数（束縛変数）を参照するための記法である。オランダ人数学者ニコラース・ホーヴァート・ド・ブラウンによって発明された。 (ja) 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. The following are some examples: (en) |
| rdfs:label |
De Bruijn index (en) ド・ブラウン・インデックス (ja) |
| owl:sameAs |
freebase:De Bruijn index wikidata:De Bruijn index dbpedia-ja:De Bruijn index https://global.dbpedia.org/id/4iWKF |
| prov:wasDerivedFrom |
wikipedia-en:De_Bruijn_index?oldid=1123617511&ns=0 |
| foaf:depiction |
wiki-commons:Special:FilePath/De_Bruijn_index_illustration_1.svg |
| foaf:isPrimaryTopicOf |
wikipedia-en:De_Bruijn_index |
| is dbo:knownFor of |
dbr:Nicolaas_Govert_de_Bruijn |
| is dbo:wikiPageDisambiguates of |
dbr:De_Bruijn |
| is dbo:wikiPageRedirects of |
dbr:De_Bruijn_indices dbr:De_bruijn_index dbr:Barendregt_convention |
| is dbo:wikiPageWikiLink of |
dbr:De_Bruijn_indices dbr:De_Bruijn dbr:Nominal_techniques dbr:Nominal_terms_(computer_science) dbr:De_bruijn_index dbr:McCarthy_Formalism dbr:Nicolaas_Govert_de_Bruijn dbr:List_of_Delft_University_of_Technology_faculty dbr:Barendregt_convention dbr:Lambda_calculus dbr:Higher-order_abstract_syntax dbr:Explicit_substitution |
| is dbp:knownFor of |
dbr:Nicolaas_Govert_de_Bruijn |
| is foaf:primaryTopic of |
wikipedia-en:De_Bruijn_index |
