Lambda Diagrams

A few days ago, partly inspired by Dave Keenan's To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction, I discovered an interesting way to denote lambda terms.

Lambda Diagrams are a graphical notation for closed lambda terms, in which abstractions (lambdas) are represented by horizontal lines, variables by vertical lines emanating down from their binding lambda, and applications by horizontal links connecting the leftmost variables and extending the leftmost one down. In the alternative style, the final extension is omitted, and applications link the nearest deepest variables, for a more stylistic, if less uniform, look.

The following table shows diagrams of identity, the booleans, the standard combinators, some Church numerals, and Omega.

term	definition	diagram	alternative
I	λx.x
K/true	λx.λy.x
false	λx.λy.y
S	λx.λy.λz.(x z)(y z)
Y	λf.(λx.x x)(λx.f(x x))
2	λf.λx.f(f x)
3	λf.λx.f(f(f x))
4	λf.λx.f(f(f(f x)))
Ω	(λx.x x)(λx.x x)

Curiously, the alternative Omega diagram somewhat resembles an (upside-down) Omega.

As an example of a significantly more complex term, here (in alternative style) is the prime number sieve from John's Lambda Calculus and Combinatory Logic Playground:

which reduces to an infinite list of booleans that starts out as

In terms of pixels, a diagram's width is one less than 4 times the number of variables (vertical lines), and its height is one more than twice the maximum number of nested abstractions and applications (one less for alternaitve diagrams with multiple variables).

The size of the binary encoding of a term is closely related to the graphical complexity: it is exactly twice the number of lines plus the number of (4-way) intersections.

Open terms could be partially represented by letting free variables stick out on top, but their identity would be lost.

HOAS evaluation

This literatare Haskell program demonstrates how Higher Order Abstract Syntax (HOAS)
allows for very simple step-wise evaluation in the untyped lambda calculus.

> module HOAS where
> import Text.PrettyPrint.HughesPJ(Doc, renderStyle, style, text, (<>), (<+>), parens)
> import Data.List(unfoldr)
> import Control.Monad(mplus)
> import Data.Maybe(Maybe,fromJust)

A term is either an abstraction, represented by a Haskell function binding a variable identifier,
an application, or a bound variable identifier.

> data HOAS = Lam (HOAS -> HOAS) | App HOAS HOAS | Var Char

Var is not used for only for printing terms, not for representing them.
The identity function is simply represented as

> i :: HOAS
> i = Lam(\f-> f)

and the two basis functions in combinatory logic as

> k :: HOAS
> k = Lam(\x-> Lam(\y-> x))
> s :: HOAS
> s = Lam(\x-> Lam(\y-> Lam(\z-> (x `App` z) `App` (y `App` z))))

Evalution to normal form is a simple matter
of evaluating the body in an abstraction, both the function and argument
in an application, and applying the representing Haskell function when
the former evaluates to an abstraction, which will perform substitution
without all the usual headaches, like free variable capture, of a classical representation.

> nf :: HOAS -> HOAS
> nf (Lam f)   = Lam (nf . f)
> nf (App f a) = case nf f of { Lam g -> g; g -> App g } $ nf a
> nf x         = x

Performing individual beta reduction steps is almost as easy,
only complicated by the need to determine if an abstraction body has a redex:

> step :: HOAS -> Maybe HOAS
> step (App (Lam f) a) = Just $ f a
> step (App f       a) = fmap (`App` a) (step f) `mplus` fmap (f `App`) (step a)
> step (Lam f)         = step (f (Var undefined)) >> Just (Lam (fromJust . step . f))
> step x               = Nothing

Combining steps by unfolding

> steps :: HOAS -> [HOAS]
> steps = unfoldr (fmap (\x->(x,x)) . step)

gives us an alternative way to derive normal forms as

> slownf :: HOAS -> HOAS
> slownf = last . steps

It remains to show off the fruits of our efforts with a pretty printer

> pp :: Int -> Char -> HOAS -> Doc
> pp _ g (Var   v) = text $ [v]
> pp p g (Lam   e) = (if p>0 then parens else id) $ text ['\\',g,' '] <> pp 0 (succ g) (e (Var g))
> pp p g (App f a) = (if p>1 then parens else id) $ pp 1 g f   <+> pp 2 g a

> instance Show HOAS where
>   show = renderStyle style . pp 0 'a'

Example reduction of predecessor of Church numeral one

> prd = Lam(\n->Lam(\f->Lam(\x->n`App`Lam(\g->Lam(\h->h`App`(g`App`f)))`App`Lam(\u->x)`App`i)))
> example1 = prd `App` i

Infinite reduction

> dbl = Lam (\x -> x `App` x)
> example2 = dbl `App` dbl

Ackermann

> ack = Lam(\n->n`App`Lam(\f->Lam(\m->f`App`(m`App`f`App`i)))`App`Lam(\m->Lam(\f->Lam(\x->f`App`(m`
App`f`App`x))))`App`n)
> two = Lam(\f->Lam(\x->f`App`(f`App`x)))
> example3 = ack `App` two

> showoff :: HOAS -> IO ()
> showoff = mapM_ print . steps

> main = showoff example3

The only downside is that variable names do not preserve identity between steps,
and only indicate binding depth.