Next: Binding
Up: classnote 14
Previous: Equality Definition
Standard presentations of the 
-calculus begin with some surface
syntax (usually defined by a context-free grammar). The -terms
and 
are abbreviated by 
and
respectively. A convention is also adopted where:
- parentheses are omitted
- function application associates to the left:
abbreviates 
-
abbreviates 
.
It can be difficult at times to determine the structure of an abbreviated
-term. In such instances, it is useful to give a pictorial
depiction. One way of doing so is by using de Bruijn indices.
eg. 
abbreviates 
pictorial form of 
:
de Bruijn's index representation of :
de Bruijn's index representation
eliminates the need for arrows
associating leaf nodes with -nodes through a numbering scheme.
The numbers at the leaf nodes of the representation indicate the number
of -nodes to count up.