VEX

VEX (visual expressions) is a VL for the representation of lambda expressions.


The picture provides two exemplary VEX expressions. The upper one represents the lambda term λy.(x y), i.e. a function that applies the free variable x to its argument. The other one represents the term λx.λy.(x y). Here variable x also is bound by an abstraction.

VEX is a very simple visual language in the sense that there are only three different visual components: the circle, the line and the arrow. The whole meaning of an arrangement of these components is determined by their spatial relations.


A lambda term is inductively defined. It is either a variable, an application of one lambda term to another one or an abstraction that consists of the variable to be bound and its body, i.e. the scope of the particular variable. For these three cases visual representations are defined.

In VEX a single variable is represented by a circle. It does not need to have a name as in the textual form. An abstraction is represented by a circle with a smaller circle internally tangent to it. Elements contained in the bigger circle are part of the abstractions body whereas the smaller circle represents the parameter. The application of an expression e1 to an expression e2 is represented by an arrow that points from e1 to e2. Further the outermost circles of e1 and e2 have to touch each other.

Variables can be bound via lines to parameters of abstractions. If they are free they need to be bound to a free variable circle that must not be inside another circle. The meaning for this is that it has to be possible to identify occurrences of the same free variable.

The main purpose of VEX is to simplify the teaching of lambda calculus. For this sake it is very benefitial that variable bindings are made explicit by lines and not implicitly hidden behind equal names. In particular one does not have to deal with the difficulties resulting from overlapping scopes and thus the need for alpha conversion.



Syntax analysis for VEX diagrams is quite difficult. There are ambiguities (i.e. to circles connected by a line, which one is the variable and which one the free variable circle?) and a lot of combinations of particular patterns and their spatial arrangement. However, there is a quite flexible DiaGen editor for VEX where the language is defined via a hyperedge replacement grammar. However, as you see in the picture "two different kinds of circles" need to be defined restricting the freedom of the user somewhat.