Lariat

Version 0.3

Lariat is a project to define a total abstract data type for proper lambda terms, consisting of four basic operations: app, abs, var, and destruct.

This repository presents the definition of these operations. It also contains implementations of this abstract data type in various programming languages, currently including:

• Haskell

The version of the Lariat defined by this document is 0.3. This version number will be promoted to 1.0 once vetted sufficiently.

Table of Contents

• Background
• The Operations
• Some Examples
• Discussion

Background

There are several approaches to representing lambda terms in software.

The naive approach is to represent them just as they are written on paper. In this approach, whether a variable, such as x, is free or bound depends on whether it is inside a lambda abstraction λ x or not. If you need to manipulate it (or the abstraction it's bound to), you might need to rename it so that it doesn't conflict with another variable also called x that is perhaps free or perhaps bound to a different lambda abstraction.

This is tiresome and error-prone. So other approaches were developed.

One such alternate approach is De Bruijn indexes (Wikipedia), where variables are represented not by names, but by numbers. The number indicates which lambda abstraction the variable is bound to, if any; a 1 indicates the immediately enclosing lambda abstraction, a 2 indicates the lambda abstraction just above that, and so on. If the number exceeds the number of enclosing lambda abstractions, then it is a free variable.

But this, too, has some drawbacks, so people have devised a number of other approaches:

• "maps" (Viewing Terms through Maps (PDF), Sato et al., 1980) (see also these slides (PDF) from 2012)
• "nominal techniques" (A New Approach to Syntax (PDF), Gabbay and Pitts, 1999)
• "locally nameless" (I am not a number (PDF), McBride and McKinna, 2004)
• "bound" (bound: Making de Bruijn Succ Less, Kmett, 2013)

among others.

But the point I would like to make in this article is this: At some level of abstraction it does not matter which approach is chosen as long as the approach satisfies the essential properties that we require of lambda terms.

To this end, this article presents an abstract data type (ADT) for lambda terms, which we call Lariat, consisting of four operations. The actual, concrete data structure in which they are stored, and the actual, concrete mechanism by which names become bound to terms, are of no consequence (and may well be hidden from the programmer) so long as the implementation of the operations conforms to the stated specification.

This ADT is designed for simplicity and elegance rather than performance. It is a minimal formulation that does not necessarily make any of commonly-used manipulations of lambda terms efficient.

This ADT has two properties, intended to contribute to its elegance. Firstly, it can represent only proper lambda terms; that is, it is not possible for a lambda term constructed by the Lariat operations to contain an invalid bound variable.

Secondly, it is total in the sense that all operations are defined for all inputs that conform to their type signatures. There are no conditions (such as trying to pop from an empty stack in a stack ADT) where the result is undefined, nor any defined to return an error condition. This totality does, however, come at the cost of the operations being higher-order and with polymorphic types.

For more background information, see the Discussion section below.

Names

Lambda terms are essentially about name binding, and in any explication of name binding, we must deal with names. As of 0.3, Lariat requires only two properties of names.

Firstly, it must be possible to compare two names for equality. This is required for operations that replace free variables that have a given name with a value -- there must be some way for them to check that the free variable has the name that they are seeking.

Secondly, given a set of names, it must be possible to generate a new name that is not equal to any of the names in the set (a so-called "fresh" name). This is required to properly implement the destruct operation. If names are modelled as character strings, obtaining a fresh name could be as simple as finding the longest string of a set of strings, and prepending "a" to it.

Note that, although neither of these properties is exposed as an operation, it would be reasonable for a practical implementation of Lariat to expose them so. It would also be reasonable to provide other operations on names, such as constructing a new name from a textual representation, rendering a given name to a canonical textual representation, and so forth. From the perspective of Lariat itself these are ancillary operations, and as such will not be defined in this document.

Terms

We now list the four operations available for manipulating terms.

var(n: name): term

Given a name n, return a free variable with the name n.

Note: A free variable is a term; it can be passed to any operation that expects a term.

app(t: term, u: term): term

Given a term t and a term u, return an application term which contains t as its first subterm and u as its second subterm.

Note: An application term is a term that behaves just like an ordered pair of terms.

abs(n: name, t: term): term

Given a name n and a term t, return an abstraction term containing t', where t' is a version of t where all free variables named n inside t' have been replaced with bound variables. These bound variables are bound to the returned abstraction term.

Note: we may consider a bound variable to be a term, but the user of the abstract data type cannot work with bound variables directly, so it is unlike all other kinds of terms in that respect. A bound variable is always bound to a particular abstraction term. In the case of abs, the abstraction term to which variables are bound is always the term returned by the abs operation.

Note: an abstraction term contains one subterm. This subterm cannot be extracted directly, as it may contain bound variables, which the user cannot work with directly.

destruct(t: term, f1: fun, f2: fun, f3: fun): X

Given a term t and three functions f1, f2, and f3 (each with a different signature, described below), choose one of the three functions based on the structure of t, and evaluate it, returning what it returns.

If t is a free variable, evaluate f1(n) where n is the name of the free variable t.

If t is an application term, evaluate f2(u, v) where u is the first subterm of t and v is the second subterm of t.

If t is an abstraction term, evaluate f3(u, n) where u is a version of t where all bound variables in u that were bound to u itself have been replaced by n, where n is a fresh name (i.e. a name that does not occur in any free variable in any subterm of u).

Note: as stated above, a bound variable is always bound to an abstraction term. The bound variables that are replaced by the destruct of an abstraction term are always and only those that are bound to the abstraction term being destructed.

Note: the destruct operation's signature shown above was abbreviated to make it less intimidating. The full signature would be

destruct(t: term, f1: fun(n: name): X, f2: fun(u: term, v: term): X, f3: fun(u: term, n: name): X): X

Note: see the section on "Names" above for the basic requirements for obtaining a fresh name.

Some Examples

We will now give some concrete examples of how these operations can be used. But first, we would like to emphasize that Lariat is an ADT for lambda terms, not the lambda calculus. Naturally, one ought to be able to write a lambda calculus normalizer using these operations (and this will be one of our goals in the next section), but one is not restricted to that activity. The terms constructed using the Lariat operations may be used for any purpose for which terms-with-name-binding might be useful.

Example 1

A common task is to obtain the set of free variables present in a lambda term. This is not difficult; we only need to remember that every time we destruct an abstraction term, we introduce a fresh free variable of our own, to keep track of these, and make sure not to include any of them when we report the free variables we found.

Note: In the following pseudocode, + is the set union operator.

let freevars = fun(t, ours) ->
    destruct(t,
        fun(n) -> if n in ours then {} else {n},
        fun(u, v) -> freevars(u, ours) + freevars(v, ours),
        fun(u, n) -> freevars(u, ours + {n})
    )

Example 2

Given an abstraction term and a value, return a version of the body of the abstraction term where every instance of the variable bound to the abstraction term is replaced by the given value. We can call this operation resolve.

let resolve = fun(t, x) ->
    destruct(t,
        fun(n) -> t,
        fun(u, v) -> t,
        fun(u, n) -> replace_all(u, n, x)
    )
where replace_all = fun(t, m, x) ->
    destruct(t,
        fun(n) -> if n == m then x else var(n),
        fun(u, v) -> app(replace_all(u, m, x), replace_all(v, m, x))