An Entity of Type: software, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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:

Property Value
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
dbo:wikiPageID
  • 10314482 (xsd:integer)
dbo:wikiPageLength
  • 9087 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1013818847 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dct:subject
gold:hypernym
rdf:type
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
prov:wasDerivedFrom
foaf:depiction
foaf:isPrimaryTopicOf
is dbo:knownFor of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:knownFor of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License