Edits
Chris Pressey
3 years ago
| 25 | 25 | |
| 26 | 26 | There are several approaches for representing lambda terms in software. |
| 27 | 27 | |
| 28 | The naive approach is to represent them just as they are written on paper. In this approach, if you see | |
| 29 | a variable, such as _x_, whether _x_ is free or bound depends on whether it is inside a lambda abstraction | |
| 28 | The naive approach is to represent them just as they are written on paper. In this approach, whether | |
| 29 | a variable, such as _x_, is free or bound depends on whether it is inside a lambda abstraction | |
| 30 | 30 | λ _x_ or not. If you need to manipulate it, you might need to rename it so that it doesn't conflict with |
| 31 | 31 | another variable also called _x_ that is bound to a different lambda abstraction. |
| 32 | 32 | |
| 33 | 33 | This is tiresome and error-prone. So other approaches were developed. |
| 34 | 34 | |
| 35 | One such approach is called De Bruijn indexes. In this approach, variables are represented not by names, | |
| 36 | but by numbers. The number indicates which lambda abstraction the variable is bound to, if any. That is, | |
| 37 | a 1 indicates it is bound to the immediately enclosing lambda abstraction, a 2 indicates it is bound to | |
| 38 | the lambda abstraction just above that, and so on. If the number exceeds the number of lambda abstractions | |
| 39 | which enclose the variable, it is a free variable. | |
| 40 | ||
| 41 | This, too, has some drawbacks, so people have devised a number of other approaches: | |
| 35 | One such approach alternate is De Bruijn indexes, where variables are represented not by names, | |
| 36 | but by numbers. The number indicates which lambda abstraction the variable is bound to, if any; | |
| 37 | a 1 indicates the immediately enclosing lambda abstraction, a 2 indicates the lambda abstraction | |
| 38 | just above that, and so on. If the number exceeds the number of enclosing lambda abstractions, | |
| 39 | then it is a free variable. | |
| 40 | ||
| 41 | But this, too, has some drawbacks, so people have devised a number of other approaches: | |
| 42 | 42 | |
| 43 | 43 | * "nominal techniques" (Gabbay and Pitts) |
| 44 | 44 | * "locally nameless" (various?) |
| 45 | 45 | * "maps" (Sato et al.) |
| 46 | 46 | * "bound" (Kmett) |
| 47 | 47 | |
| 48 | and so forth. | |
| 49 | ||
| 50 | But the point is, at some level of abstraction _it does not matter_ which | |
| 51 | approach is chosen _as long as_ the approach satisfies the essential properties | |
| 52 | that we require lambda terms to have. | |
| 48 | among others. | |
| 49 | ||
| 50 | But the point we would like to make is this: At some level of abstraction _it does not matter_ | |
| 51 | which approach is chosen _as long as_ the approach satisfies the essential properties | |
| 52 | that we require of lambda terms. | |
| 53 | 53 | |
| 54 | 54 | To this end, we present this abstract data type for lambda terms, which we |
| 55 | call "Lariat", consisting of six operations. The actual, concrete data type | |
| 55 | call "Lariat", consisting of six operations. The actual, concrete data structure | |
| 56 | 56 | in which they are stored, and the actual, concrete mechanism by which names |
| 57 | become bound to terms, are of no real consequence (and may well be hidden | |
| 57 | become bound to terms, are of no consequence (and may well be hidden | |
| 58 | 58 | from the programmer) so long as the implementation of the operations conforms |
| 59 | 59 | to the stated specification. |
| 60 | 60 | |
| 71 | 71 | ### `app(t1: term, t2: term): term` |
| 72 | 72 | |
| 73 | 73 | Given a term _t1_ and a term _t2_, return an _application term_ |
| 74 | which contains _t1_ as its head and _t2_ as its tail. | |
| 74 | which contains _t1_ as its first subterm and _t2_ as its second | |
| 75 | subterm. | |
| 76 | ||
| 77 | > **Note**: An application term is a term that is an | |
| 78 | > ordered pair of terms. | |
| 75 | 79 | |
| 76 | 80 | ### `abs(n: name, t: term): term` |
| 77 | 81 | |
| 78 | 82 | Given a name _n_ and a term _t_, return an _abstraction term_ |
| 79 | containing _t'_, where _t'_ is a version of _t_ where all free | |
| 80 | variables named _n_ inside _t'_ have been replaced with | |
| 83 | containing _t_', where _t_' is a version of _t_ where all free | |
| 84 | variables named _n_ inside _t_' have been replaced with | |
| 81 | 85 | bound variables. These bound variables are bound to |
| 82 | 86 | the returned abstraction term. |
| 83 | 87 | |
| 84 | 88 | > **Note**: a bound variable is a term, but the user cannot |
| 85 | 89 | > work with bound variables directly. A bound variable is always |
| 86 | > bound to an abstraction term. In the case of `abs`, | |
| 90 | > bound to a particular abstraction term. In the case of `abs`, | |
| 87 | 91 | > the abstraction term to which variables are bound, is |
| 88 | 92 | > the term returned by the operation. |
| 89 | 93 | |