About: De Bruijn index

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: De Bruijn index Goto Sponge NotDistinct Permalink

An Entity of Type : dbo:Software, within Data Space : dbpedia.org associated with source document(s)
QRcode icon

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:

Attributes	Values
rdf:type	software
rdfs:label	De Bruijn index (en) ド・ブラウン・インデックス (ja)
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)
foaf:depiction
dct:subject	Lambda calculus
Wikipage page ID	10314482 (xsd:integer)
Wikipage revision ID	1123617511 (xsd:integer)
Link from a Wikipage to another Wikipage	Proof assistant Lambda calculus De Bruijn notation K combinator Combinatory logic Mathematical logic Nominal techniques Rewriting Free variables and bound variables Substitution (logic) Mathematician Automated theorem proving Logic programming Nicolaas Govert de Bruijn Equivariant Free variable Lambda calculus Higher-order abstract syntax Higher-order logic Meta-logic Natural number Netherlands Bound variable S combinator Variable (mathematics) Isabelle theorem prover Scope (programming) Β-reduction Λ calculus Α-conversion
sameAs	De Bruijn index De Bruijn index De Bruijn index De Bruijn index
dbp:wikiPageUsesTemplate	dbt:About dbt:Reflist dbt:Short_description
thumbnail	wiki-commons:Special:FilePath/De_Bruijn_index_illustration_1.svg?width=300
has 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)
gold:hypernym	Notation
prov:wasDerivedFrom	wikipedia-en:De_Bruijn_index?oldid=1123617511&ns=0
page length (characters) of wiki page	12718 (xsd:nonNegativeInteger)
foaf:isPrimaryTopicOf	wikipedia-en:De_Bruijn_index
is Link from a Wikipage to another Wikipage of	De Bruijn indices De Bruijn Nominal techniques Nominal terms (computer science) De bruijn index McCarthy Formalism Nicolaas Govert de Bruijn List of Delft University of Technology faculty Barendregt convention Lambda calculus Higher-order abstract syntax Explicit substitution
is Wikipage redirect of	De Bruijn indices De bruijn index Barendregt convention
is Wikipage disambiguates of	De Bruijn
is known for of	Nicolaas Govert de Bruijn
is known for of	Nicolaas Govert de Bruijn
is foaf:primaryTopic of	wikipedia-en:De_Bruijn_index

Faceted Search & Find service v1.17_git147 as of Sep 06 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Sep 2 2024, on Linux (x86_64-generic-linux-glibc212), Single-Server Edition (378 GB total memory, 52 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software