De Bruijn index - Citizendia

In mathematical logic, the de Bruijn index is a notation invented by the Dutch mathematician Nicolaas Govert de Bruijn (pronounced [dɪˈbʁœyn]) for representing terms in the λ calculus. Mathematical logic is a subfield of Logic and Mathematics with close connections to Computer science and Philosophical logic. The Netherlands ( Dutch:, ˈnedərlɑnt is the European part of the Kingdom of the Netherlands, which consists of the Netherlands the Netherlands A mathematician is a person whose primary area of study and research is the field of Mathematics. Nicolaas Govert de Bruijn (born 9 July, 1918) is a Dutch Mathematician, affiliated as Professor emeritus In Mathematical logic and Computer science, lambda calculus, also written as λ-calculus, is a Formal system designed to investigate function ^[1] Terms written using these indexes are invariant with respect to α conversion, so the check for α-equivalence is the same as that for syntactic equality. In Mathematical logic and Computer science, lambda calculus, also written as λ-calculus, is a Formal system designed to investigate function 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. In Mathematics, a natural number (also called counting number) can mean either an element of the set (the positive Integers or an A variable (ˈvɛərɪəbl is an Attribute of a physical or an abstract System which may change its Value while it is under Observation. In Computer programming, scope is an enclosing context where values and expressions are associated The following are some examples:

The term λx. λy. x, sometimes called the K combinator, is written as λ λ 2 with de Bruijn indexes. Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for Variables in Mathematical logic 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 indexes, is λ λ λ 3 1 (2 1). Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for Variables in Mathematical logic
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 indexes are commonly used in higher-order reasoning systems such as automated theorem provers and logic programming systems. In Mathematics, higher-order logic is distinguished from First-order logic in a number of ways Automated theorem proving ( ATP) or automated deduction, currently the most well-developed subfield of Automated reasoning (AR is the Logic programming is in its broadest sense the use of mathematical logic for computer programming ^[2]

1 Formal definition
2 Alternatives to de Bruijn indexes
3 See also
4 References

Formal definition

Formally, λ-terms (M, N, …) written using de Bruijn indexes have the following syntax (parentheses allowed freely):

M, N, … ::= n | M N | λ M

where n — natural numbers greater than 0 — are the variables. In Mathematical logic and Computer science, lambda calculus, also written as λ-calculus, is a Formal system designed to investigate function In Mathematics, a natural number (also called counting number) can mean either an element of the set (the positive Integers or an A variable n is bound if it is in the scope of at least n binders (λ); otherwise it is free. In Mathematics, and in other disciplines involving Formal languages including Mathematical logic and Computer science, a free variable is a In Mathematics, and in other disciplines involving Formal languages including Mathematical logic and Computer science, a free variable is a The binding site for a variable n is the nth binder it is in the scope of, starting from the innermost binder. In Computer programming, scope is an enclosing context where values and expressions are associated

The most primitive operation on λ-terms is substitution: replacing free variables in a term with other terms. In the β-reduction (λ M) N, for example, we must:

find the variables n₁, n₂, …, n_k in M that are bound by the λ in λ M,
decrease the free variables of $M$ to match the removal of the outer $λ$ -binder, and
replace n₁, n₂, …, n_k with N, suitably increasing the free variables occurring in N each time, to match the number of λ-binders the corresponding variable occurs under when substituted. In Mathematical logic and Computer science, lambda calculus, also written as λ-calculus, is a Formal system designed to investigate function

To illustrate, consider the application

(λ λ 4 2 (λ 1 3)) (λ 5 1)

which might correspond to the following term written in the usual notation

(λx. λy. z x (λu. u x)) (λx. w x).

After step 1, we obtain the term λ 4 □ (λ 1 □), where the variables that are substituted for are replaced with boxes. Step 2 lowers the free variables, giving λ 3 □ (λ 1 □). Finally, in step 3 we replace the boxes with the argument; the first box is under one binder, so 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)).

Formally, a substitution is an unbounded list of term replacements for the free variables, written M₁. M₂…, where M_i is the replacement for the ith free variable. The increasing operation in step 3 is sometimes called shift and written ↑^k where k is a natural number indicating the amount to increase the variables; For example, ↑⁰ is the identity substitution, leaving a term unchanged.

The application of a substitution s to a term M is written M[s]. The composition of two substitutions s₁ and s₂ is written s₁ s₂ and defined by

M [s₁ s₂] = (M [s₁]) [s₂].

The rules for application are as follows:

$\begin{align} n [N_1\ldots N_n\ldots] =& N_n \\ (M_1\;M_2) [s] =& (M_1[s]) (M_2[s]) \\ (\lambda\;M) [s] =& \lambda\;(M [1.1[s'].2[s'].3[s']\ldots]) \\ & \text{where } s' = s \uparrow^1 \end{align}$

The steps outlined for the β-reduction above are thus more concisely expressed as:

(λ M) N →_β M [N. 1. 2. 3…].

Alternatives to de Bruijn indexes

When using the standard "named" representation of λ-terms, where variables are treated as labels or strings, one has to explicitly handle α-conversion when defining any operation on the terms. The standard Variable Convention^[3] of Barendregt is one such approach where α-conversion is applied as needed to ensure that:

bound variables are distinct from free variables, and
all binders bind variables not already in scope. Hendrik Pieter (Henk Barendregt (born 1947 is a Dutch Logician, known for his work in Lambda calculus and Type theory.

In practice this is cumbersome, inefficient, and often error-prone. It has therefore led to the search for 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 indexes internally, it will present a user interface with names.

De Bruijn indexes are not the only representation of λ-terms that obviates the problem of α-conversion. Among named representations, the nominal logic of Pitts is one approach, where the representation of a λ-term is treated as an equivalence class of all terms rewritable to it using variable permutations. In Mathematics, Computer science and Logic, rewriting covers a wide range of potentially non-deterministic methods of replacing subterms of a ^[4] This approach is taken by the Nominal Datatype Package of Isabelle/HOL. The Isabelle theorem prover is an interactive theorem proving framework a successor of the HOL theorem prover. ^[5]

Another common alternative is an appeal to higher-order representations where the λ-binder is treated as a true function. In Computer science, higher-order abstract syntax (abbreviated HOAS) is a technique for the representation of Abstract syntax trees for languages with variable In such representations, the issues of α-equivalence, substitution, etc. are identified with the same operations in a meta-logic. Metalogic is the study of the Metatheory of Logic. While logic is the study of the manner in which logical systems can be used to decide the correctness

References

^ De Bruijn, Nicolaas Govert (1972). "Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem". Indagationes Mathematicae 34: 381–392. Elsevier. Elsevier, the world's largest Publisher of Medical and Scientific literature, forms part of the Reed Elsevier group ISSN 0019-3577. An International Standard Serial Number ( ISSN) is a unique eight-digit number used to identify a print or electronic Periodical publication.
^ Gabbay, Murdoch J. ; Pitts, Andy M. (1999). "A New Approach to Abstract Syntax and Binding". 14th Annual Symposium on Logic in Computer Science: 214–224.
^ Barendregt, Henk P. (1984). The Lambda Calculus: Its Syntax and Semantics. North Holland. North Holland ( Dutch: Noord-Holland,, West Frisian: Noôrd-Holland) is a province situated on the North Sea in the ISBN 0-444-87508-5.
^ Pitts, Andy M. (2003). "Nominal Logic: A First Order Theory of Names and Binding". Information and Computation 186: 165–193. doi:10.1016/S0890-5401(03)00138-X. A digital object identifier ( DOI) is a permanent identifier given to an Electronic document. ISSN 0890-5401. An International Standard Serial Number ( ISSN) is a unique eight-digit number used to identify a print or electronic Periodical publication.
^ Nominal Isabelle web-site. Retrieved on 2007-03-28. Year 2007 ( MMVII) was a Common year starting on Monday of the Gregorian calendar in the 21st century. Events 37 - Roman Emperor Caligula accepts the titles of the Principate, entitled to him by the Senate.

© 2009 citizendia.org; parts available under the terms of GNU Free Documentation License, from http://en.wikipedia.org
network: | |

Contents

Formal definition

Alternatives to de Bruijn indexes

See also

References