; that is, 
defines a fixpoint on e1.We can do this by expanding 
as follows:
It has been our experience that this difficulty is most apparent in teaching beginners. Not only does the notion of substitution and lambda capture confound students, as it does experts, but notions of higher-order functions, currying, abstraction, environments and free variables, and least fixpoint recursion also present difficulties.
Part of the problem resides in the syntax: nested lambda expressions break up expressions and separate related items, and the uninitiated student is unable to use such useful visual cues as adjacency to decipher the expressions. Another problem lies in the abstractness of the material, and in the existence of certain features required to give the expression meaning that are only implicitly referred to, such as the notion of an environment that contains bindings of free variables.
In order to address these problems, we introduce VEX (Visual EXpressions), a completely visual representation of the lambda calculus. By completely visual, we do not mean that the notation contains no text (text is suitable for labels and constant values), but only that the semantics of the language is based on a purely graphical set of transformation rules - no knowledge of the underlying textual language is necessary to understand the semantics. VEX has been developed as the expression-oriented component of VIPR (Visual Imperative PRogramming language) [3, 4], a completely visual imperative programming language (see [11] for a discussion of completely visual languages), in order to provide a representation for expressions and functions in that language, but we believe that VEX has value outside that framework, particularly in the teaching of functional concepts.
This paper is organized as follows. In the second (next) section, we present a motivating example comparing use of a complex lambda expression (the Y combinator) with a simpler but equivalent VEX expression. In the third section, we build our visual lambda calculus, first by specifying the syntax, then by providing graphical equivalents for the substitution rule and by showing how graphical equivalents of the three rewrite rules (a, b, and h) may be specified using the graphical substitution rule, and finally by showing how the three rewrite rules may be represented by very simple and intuitive graphical transformation rules that make no explicit reference to the substitution rule. In the fourth section, we discuss some additional issues, including the treatment of recursion, and the use of certain syntactic extensions (particularly, let expressions), and associated concepts such as environments and closures. We then address certain scalability issues, discuss related work, and finally, draw conclusions and report on the current status of the work.
is a construct used, among other purposes, in order to prove results involving fixpoints and recursion. We employ it in our opening example in order to contrast the surprising and non-intuitive behavior of the textual version with the more intuitive behavior of the graphical version.
Textually, we wish to show that, for any lambda expression e, ; that is, defines a fixpoint on e1.We can do this by expanding as follows:
(1) 
The step denoted by the second line above is the difficult one, with its use of a functional argument, and the functional value substituted for the identifier x. We will attempt to do better in our graphical representation.
The VEX representation of the Y combinator is given in figure 1. A few features should be noted. First, an expression (abstraction or not) is represented by a closed figure. Parameters are represented by closed figures that are tangent to, and inside, another closed figure. Thus, the circles labeled f and x represent parameters. Items that would be identifiers in the textual lambda calculus are also represented by circles in VEX. Each of the circles in the two small clusters of three circles represents an identifier. One can determine that they are identifiers because they are connected by undirected edges to a labeled circle, representing the definition of a parameter (in the cases in figure 1) or a free variable (not in figure 1, but described in section 3.0). Application of functions is represented by closed figures tangent to, and external to, each other. A small arrow indicates which figure represents the applied function and which represents the argument (the arrow points to the argument). When application order is ambiguous, application arrows are numbered according to priority, where lower numbers indicate higher priority. These numbers are left out of subsequent figures.
The basic principle of the VEX expression evaluation is that the graphical expressions are elaborated until no further computation is possible. The resulting graphical expression is the value of the original expression. When applying the expression of figure 1 to the value e, we can intuit that the eventual result will resemble one of the clusters of three elements, where the first (leftmost) element will be the argument (in this case, e), and the remaining elements will be copies of the initial configuration (Y e).
Figure 1. VEX representation of the Y combinator
Figures 2 through 4 show the VEX equivalent of the evaluation given in equation (1) above. Figure 2 shows the Y combinator applied to the argument e. Figure 3 shows the results of this application, substituting the argument for all identifiers bound to the parameter f. The result of the application in figure 3 involves substitution of the functional argument represented by the righthand figure for the parameter x in the lefthand figure. The result, in figure 4, is the function e being applied to exactly the figure in figure 3. Since figure 3, as well as figures 2 and 4, represent 
, figure 4 must also represent 
, and we have a fixpoint.
The VEX representation has made explicit the notion of binding and substitution in a way that is much more straightforward than that of the textual lambda calculus. The distinction between the two different but identically named bound identifiers x is explicit. Finally, the notion of functional arguments and higher-order functions is also explicit.
This section will describe the graphical transformation rules informally. Space does not permit a description of the formal specification of VEX through transformation rules, but a more complete description appears in [6], using the same system employed to formally specify the semantics of VIPR [4].
Figure 2. VEX version of 
Figure 3. VEX version of 
Figure 4. VEX version of 
Click here for an animated version of figures 2-4.
Function application is represented by two expressions externally tangent to each other. An ordering on the two expressions is imposed by an arrow at the tangent point. The expression at the tail of the arrow represents the function being applied, and the expression at the head represents the argument. In figure 5, circles 2 and 3 represent a function application, where circle 3 and its contents represents the applied function, and circle 2 represents the argument.
Figure 5. Syntax of a VEX expression
Abstraction is represented by an expression circle containing an identifier root node internally tangent to it. The root node represents the parameter, and the contents of the expression circle represents the abstraction body. Thus, in figure 5, circle 3 and its contents represent an abstraction, where circle 4 is the parameter and circle 5 is the body. Figure 5, therefore, represents the expression 
.
One can see that certain seemingly anomalous situations can occur, such as that in figure 6, in which the identifier x seems to be both free and bound in the expression labeled 1. However, textual names in VEX have no semantic value; the actual "name" of an identifier ring is the root node to which it is connected. Thus, the "name" of the identifier represented by ring 3 is the root node labeled 2 in the diagram, while the root node whose label is 4 is the "name" of the identifier represented by ring 5. The textual label on the root node is simply a comment meant to enhance readability, although we currently require root nodes to have names in order to distinguish them from other types of rings. In this case, it is simply a coincidence that both identifiers are named x. There is no difference in power between VEX and conventional textual lambda calculus in this regard: any expression like that given in figure 6 can be written textually by renaming one of the variables (e.g., 
). It is recommended, however, that names be chosen to avoid such confusion.
Figure 6. Free and bound identifiers - representation of 
It should be noted that this graphical definition exactly reflects the traditional definition of free variables in textual lambda calculus. If we define 
as the set of free variables in a given expression e, then for a single-identifier expression x, 
, and likewise 
, which represents the expression x, clearly indicates that the set of free variables in that expression is 
.
Similarly, 
and the diagram
,
where the unconnected lines are a notation that indicates that the undirected edges each connect to some ring in the interior of rings 
and 
, suggests the same relationship, since, inductively, if a, b, and c are the free identifiers in 
, and c and d are the free identifiers in 
, then clearly a, b, c, and d are the free variables in 
.
Finally, concerning abstractions, 
. Similarly, it is clear from
that if a, b, and x are free in 
, then only a and b are free in 
.
To substitute for a variable in VEX, a "substitution arrow" is used. The arrow originates in the root node of the identifier being substituted for, and ends at the expression being substituted. Thus, as in figure 7, if we wish to substitute the given expression (equivalent to 
) for x, we run an arrow from x's root node to the figure for the expression. The first step is to substitute the thing pointed to for the thing at the tail of the arrow, as in figure 8. In the next step, all identifiers connected to the former root node are substituted for, and the original expression and the undirected edges disappear (figure 9).
Variables may also be substituted for other variables, as is shown in figure 10.
The same simple two-step process holds for all substitutions, thus greatly simplifying the substitution rule by eliminating consideration of various combinations of free and bound variables and by avoiding concerns about renaming.
Figure 7. Substitution - initial configuration
Figure 8. Substitution - first step
Figure 9. Substitution - second step
Click here for an animated version of figures 7-9.
Figure 10. Substitution of one variable for another
Click here for an animated version of figure 10.
The first rule, alpha-conversion, also known as renaming, is specified textually as
.
In other words, one may rename any bound variable with any other name, as long as it doesn't conflict with a name already used for a free variable in the function body.
The VEX equivalent is given in figure 10 above. Note that variable "freeness" is graphically explicit, so we need only worry about using a free variable to the extent that the new identifier not employ a root node already free in the expression. Examination of figure 10 suggests that, in VEX, it is sufficient simply to change the label on a root node representing a bound variable; no explicit substitution need be performed. Thus, the alpha-conversion rule may be applied as in figure 10 without the intermediate step. This simplification is clearly in the spirit of the renaming conversion; the substitution operation in the textual version is merely an artifact resulting from the textual process of renaming.
beta-reduction is a symbolic formulation of function application, and is specified textually as
. In other words, application involves substituting the argument for all instances of the parameter. In VEX, the substitution rule may be explicitly employed to perform the substitution, as in figure 11, or the intermediate steps may be skipped, and the values propagated to their destinations, as was done in the example in figures 2 through 4.
The final rule, eta-reduction, relates an abstraction to its underlying expression body in certain cases:
.
Again, in VEX we detect whether or not x is free in e by looking for connecting links from x's root node into e. Figure 12 suggests that VEX's equivalent of eta-reduction simply involves collapsing the connection between the parameter and the argument and eliminating the pair.
Figure 11. Application
Click here for an animated version of figure 11.
Figure 12. eta-reduction
Click here for an animated version of figure 12.
As we can see, the graphical versions of the rewrite rules provided by VEX at the very least lend insight into the mechanisms and rationale of the more arcane textual rewrite rules, and at best provide a simple, intuitive framework for understanding lambda calculus that requires no knowledge of the underlying textual language.
Constants in VEX are represented by closed figures containing the constants' values. Figure 13 shows sample VEX constants (0, 1, true, and false), and an example of function application involving constants.
Figure 13. VEX constants
In order to aggregate information in lambda calculus, ordered tuple constructs are used. VEX provides the equivalent in the form of the selector construct. Selectors model generalized tuples that may be indexed by values from any domain; that is, for any index set I, and for a set of sets Ai each corresponding to an element i in I:
.
In other words, tuples are represented as functions, and each tuple comes with its own built-in selector operations.
A selector construct is drawn as a function abstraction containing a set of closed figures each representing one possible index value. Each of the internal closed figures is labeled with the corresponding index value and its content is an expression representing its value. Figure 14 shows a selector construct representing the tuple (3,4) and the application of the selection operation 
to obtain the first element of the tuple.
If the parameter is only used for indexing, it may be omitted. The parameter may also be bound to identifiers inside the internal expressions, in which case the conventional undirected edges are employed.
The selector construct generalizes to other things besides tuple construction and selection. It may be used to implement the conditional construct. The internal elements may be indexed with the values true and false, and the result of indexing such a construct is the true (resp. false) case. Thus, the conditional construct 
may be represented as
.
This, incidentally, represents the parallel conditional expression, in which the true and false cases are both evaluated, rather than the sequential conditional expression proposed by McCarthy [13]. We plan to investigate representation of sequential constructs in the future.
Figure 14. A selector construct
In addition to constants, VEX provides for primitive operators, as do most uses of the lambda calculus. A primitive operator, like a constant, is a closed figure labeled with the name of the operator. Thus, the addition operator is a circle labeled '+'. Figure 15 shows the binary addition operator as part of the expression +(3,4). Note the use of the tuple/selector construct.
evaluates to 
Figure 15. Evaluation of 
The semantics of all the primitive operators can be specified by graphical transformation rules employing the conventional semantics of the operators. Our representation of primitive binary operators such as addition, above, is useful in that it may be used to expose the mechanisms of currying, another concept that students often have a hard time grasping. Comparison of the representation of addition in figure 15 and the representation of a curried addition (ultimately employing the primitive binary addition operator) in figure 16 should reveal the links between the two functions.
. Thus, the VEX equivalent of let f be 3 in g is given in figure 17. Note that the free occurrences of f in g may be readily identified, and that the binding may be considered as a substitution that may be performed immediately or deferred until later.
Figure 16. A curried version of addition 
Click here for an animated version of figure 16.
Figure 17. VEX representation of a local binding
In more specific terms, it can be argued that VEX scales better than conventional textual lambda calculus. Consider the lambda expression 
. Note the difficulty in reading the expression and in deciding which identifiers are bound to which values and which identifiers are free in a given expression. The equivalent VEX expression (figure 17), makes these issues plain. In general, VEX avoids the problems of deeply nested expressions by keeping all elements of a given subexpression in a contiguous region, and by making identifiers' bindings explicit.
Figure 18. VEX representation of a deeply nested expression
Display of dynamic Lisp execution is generally connected with debugging, and is typically textual (that is, in the same terms as the expression being evaluated) and spending no additional effort to represent higher-level constructs in a more understandable way. In contrast, Lieberman [12] presented a visual system, employing three dimensions and color, to illustrate the process of evaluation. This system presented active functions being evaluated as sets of nested boxes, and employed a clever set of animations and shifts in perspective to illustrate the evaluation of complex expressions. Still, programs visualized by Lieberman's system were written in textual Lisp, and the visualization environment displayed visual representations of the underlying textual systems.
In contrast to these systems, Edel's Tinkertoy [9] provided a visual version of Lisp, in which Lisp S-expressions were drawn as trees. A user of Tinkertoy would construct Lisp programs by assembling expression trees from prototype components representing basic Lisp programming constructs. This system had the advantage of simplifying complex nested expressions by eliminating parentheses, but the Tinkertoy traded that problem for the problem of complex trees when one of the function calls had a large number of arguments, and in any case the system still did not address the problem of visualization of dynamically executing code.
VEX also provides simple and intuitive graphical transformation rules in place of the more complex textual rewrite rules of the lambda calculus, which often need to incorporate special cases to handle different combinations of free and bound variables. We believe that these simpler rules will also help students understand the important issues in functional programming and lambda calculus. We do not believe that VEX should replace the lambda calculus and be taught exclusively - the lambda calculus is more compact than VEX and possesses a well-founded and extensive theoretical foundation - but we feel that it is useful as a supplement to the lambda calculus, and may profitably be used in parallel with introduction of new and complicated material.
Finally, VEX provides a unified graphical representation by which both static expressions and dynamic evaluations may be visualized.
We are incorporating VEX into the VIPR programming language as the functional and expression-oriented component, to complement the imperative control structures that already have a graphical representation in VIPR. While we feel that VIPR programs will generally be more usable with textual expressions, exploration of a completely visual model for expressions offers a productive field of investigation in formal semantics, visual language design, and visual programming environment design, as our experiences with implementation of VIPR indicate.
[2] Böcker, H.-D. and H. Nieper, "Making the Invisible Visible: Tools for Exploratory Programming," in First Pan Pacific Computer Conference. 1985. Melbourne, Australia, 563-579.
[3] Citrin, W., M. Doherty, and B. Zorn, "The Design of a Completely Visual OOP Language," in Visual Object-Oriented Programming, Burnett, M., A. Goldberg, and T. Lewis, eds. 1995, Prentice-Hall: Englewood Cliffs, NJ. 67-93.
[4] Citrin, W., M. Doherty, and B. Zorn, "Formal Semantics of Control in a Completely Visual Programming Language," in IEEE Symposium on Visual Languages. 1994. St. Louis, 208-215.
[5] Citrin, W., R. Hall, and B. Zorn, "Addressing the Scalability Problem in Visual Programming," Technical report CU-CS-768-95, Dept. of Computer Science, University of Colorado, Boulder, April 1995. ftp://soglio.colorado.edu/pub/CU-CS-768-95.ps.Z.
[6] Citrin, W., R. Hall, and B. Zorn, "Formal Specification of VEX transformation rules," Technical report in preparation, Department of Computer Science, University of Colorado, Boulder.
[7] Citrin, W., R. Hall, and B. Zorn, "A Visual Lambda Calculus," Technical report CU-CS-757-94, Department of Computer Science, University of Colorado, Boulder, January 1995. ftp://soglio.colorado.edu/pub/CU-CS-757-94.ps.Z.
[8] Curry, H. B. and R. Feys, Combinatory Logic I. 1958, Amsterdam: North-Holland.
[9] Edel, M., "The Tinkertoy Graphical Programming Environment," in Visual Programming Environments: Paradigms and Systems, Glinert, E., ed. 1990, IEEE-CS Press: Los Alamitos, CA. 299-304.
[10] Hudak, P., "Conception, Evolution, and Application of Functional Programming Languages." Computing Surveys, 1989. 21(3): 359-411.
[11] Kahn, K. M. and V. A. Saraswat, "Complete Visualizations of Concurrent Programs and Their Executions," in IEEE Workshop on Visual Languages. 1990. Skokie, IL, 7-15.
[12] Lieberman, H., "A Three-Dimensional Representation of Program Execution," in IEEE-CS Workshop on Visual Languages. 1989. Rome, 111-116.
[13] McCarthy, J., "A basis for a mathematical theory of computation," in Computer Programming and Formal Systems, Braffort, P. and D. Hirschberg, eds. 1963, North-Holland: Amsterdam. 33-70.