https://text.marvinborner.de/2024-03-25-02.html

Lambda Screen

Fractals in Pure Lambda Calculus

Marvin Borner

2024-04-08

  * Encoding
      + Example
  * Rendering
  * Reduction
  * Fractals
      + Sierpinski Triangle
      + T-Square
      + "Sierpinski Carpet"
      + Cantor Dust
  * Utilities

Pure lambda calculus has encodings for many different data structures
like lists, numbers, strings, and trees. Wrapped in monadic IO,
lambda calculus provides a great interface for computation - as can
be seen in user-friendly syntactic variants like my programming
language bruijn. Such simple languages, however, typically don't
support graphical output (aside from ASCII art).

I present the "Lambda Screen", a way to use terms of pure lambda
calculus for generating images. I also show how recursive terms
(induced by fixed-point combinators) can lead to infinitely detailed
fractals.

If you want to skip the details or want to figure out its inner
workings yourself, go to my reference implementation (source-code)
and flip through the examples.

Encoding

A screen is a term lx.(x tl tr bl br),\lambda x.(x\ \textrm{tl}\ \
textrm{tr}\ \textrm{bl}\ \textrm{br}),lx.(x tl tr bl br), where the
terms tl, tr, bl, and br represent the top-left, top-right,
bottom-left, and bottom-right quadrants of the image. Each of these
terms can either be another screen, or a pixel.

A pixel is either on (white) or off (black). In its on state, a pixel
is defined as the k combinator w=lw b.w\textrm{w}=\lambda w\ b.ww=lw 
b.w In its off state, it's the ki combinator b=lw b.b\textrm{b}=\
lambda w\ b.bb=lw b.b This decision was made for simplicity and could
be any other state encoding, including ones of arbitrary size and
color.

Example

Click the "Render" button to see the results.

  * l_ x.(x b b b b)\lambda \_\ x.(x\ \textrm{b}\ \textrm{b}\ \textrm
    {b}\ \textrm{b})l_ x.(x b b b b)

Render

  * l_ x.(x ly.(y b w w b) w w b)\lambda \_\ x.(x\ \lambda y.(y\ \
    textrm{b}\ \textrm{w}\ \textrm{w}\ \textrm{b})\ \textrm{w}\ \
    textrm{w}\ \textrm{b})l_ x.(x ly.(y b w w b) w w b)

Render

Rendering

For this project, I decided that the entire behavior of the screen is
defined by a single closed lambda term. Upon execution of the
renderer, this function gets applied to the default empty screen
(four white squares). This enables the use of point-free/Tacit
programming (e.g. using combinators), such that you don't necessarily
have to construct screens/colors at all.

Through slightly modified beta-reduction, the screen gets updated
in-place while the term converges to its normal form. High rendering
depths or diverging behavior may stop the renderer before convergence
is reached.

Note that the renderer would also work with normal beta-reduction
until convergence. The additional steps were only made to add support
for in-place rendering of diverging terms.

Reduction

The in-place reduction-rendering works as follows (written as
pseudo-Haskell using de Bruijn indices; actually implemented in
JavaScript).

Figure out if a term looks like a screen:

 isScreen (Abs (App (App (App (App (Idx 0) _) _) _) _)) = True
 isScreen _                                             = False

Color the quadrants depending on pixel state (or grey if term is not
yet figured out):

 quadrantColor (Abs (Abs (Idx 1))) = White
 quadrantColor (Abs (Abs (Idx 0))) = Black
 quadrantColor _                   = Grey

Reduce to normal form (or loop endlessly):

 nf (Abs t)   = Abs $ nf t
 nf (App l r) = case nf l of
   Abs t -> nf $ subst t r
   t     -> App t (nf r)
 nf t         = t

Reduce to weak-head normal form:

 whnf (App l r) = case whnf l of
   Abs t -> whnf $ subst t r
   t     -> App t r
 whnf t         = t

Reduce to screen normal form (either lx.((((x tl) tr) bl) br)\lambda
x.((((x\ \textrm{tl})\ \textrm{tr})\ \textrm{bl})\ \textrm{br})lx.
((((x tl) tr) bl) br), lw b.w\lambda w\ b.wlw b.w, or lw b.b\lambda w
\ b.blw b.b):

 snf t = case whnf t of
   Abs b -> case Abs $ whnf b of
     t@(Abs (Abs _)) -> nf t -- not a screen!
     t ->
       let go t | isScreen t = t
           go (App l r)      = case whnf l of
             (Abs t) -> go $ subst t r
             t       -> go $ App t (whnf r)
           go (Abs t) = go $ Abs $ whnf t
       in  go t
   _ -> error "not a screen/pixel"

Main reduction and rendering loop (assuming drawing functions that
use and return some ctx):

 reduce ((t, ctx) : ts) | quadrantColor t != Grey = reduce ts
 reduce ((t, ctx) : ts) = if isScreen $ snf t
   then
     let (App (App (App (App _ tl) tr) bl) br) = t
     in  reduce ts
           ++ [ (tl, drawTopLeft ctx (quadrantColor tl))
              , (tr, drawTopRight ctx (quadrantColor tr))
              , (bl, drawBottomLeft ctx (quadrantColor bl))
              , (br, drawBottomRight ctx (quadrantColor br))
              ]
   else do -- this is pseudo-Haskell after all
     drawAt ctx (quadrantColor t)
     reduce ts
 
 -- and, finally:
 main t = reduce [(t, Ctx (canvas, width, height))]

See my reference implementation for more details.

Fractals

Sierpinski Triangle

We can't trivially draw the classic "standing-up" Sierpinski triangle
, since drawing the diagonals over square borders would get quite
complex.

Instead, we can draw a rotated variant using a simple rewrite rule:

Every black square stays black forever; each (sub-)quadrant gets
recursively applied to this rewrite rule. Every black square stays
black forever; each (sub-)quadrant gets recursively applied to this
rewrite rule.

Translated to lambda calculus, we get the following:

triangle=lx.(x triangle b triangle triangle)  [?]  triangle'=l_.
(y lt x.(x t b t t)) \begin{aligned} \textrm{triangle}&=\lambda x.(x\
\textrm{triangle}\ \textrm{b}\ \textrm{triangle}\ \textrm{triangle})\
\ \implies\textrm{triangle}'&=\lambda \_.(\textrm{y}\ \lambda t\ x.(x
\ t\ \textrm{b}\ t\ t)) \end{aligned} triangle[?]triangle' =lx.(x 
triangle b triangle triangle)=l_.(y lt x.(x t b t t)) 

Or, golfed in binary lambda calculus to 51 bits:

000100011010000100000101010110110000010110110011010


Render

Here, the rendering is stopped automatically after the smallest
resolution of the canvas is reached. Note how the triangle structure
appears even though we only ever explicitly draw black pixels. This
is because the unresolved recursive triangle\textrm{triangle}triangle
calls get (temporarily) drawn as grey until they also get reduced. If
the reduction wouldn't be stopped, the canvas would slowly become
black entirely.

T-Square

In each iteration, the T-Square adds new overlapping squares to the
quadrants of every square already drawn. For lambda screen we can
interpret this as a recursive split into smaller squares, where in
each iteration one of the quadrants (depending on its position) gets
drawn as black.

The first three iterations look something like this (only black and
non-wavy) The first three iterations look something like this (only
black and non-wavy)

We can model this iteration as a mutual recurrence relation:

tl=lx.(x tl tr bl b)tr=lx.(x tl tr b br)bl=lx.(x tl b bl br)br=lx.
(x b tr bl br)tsquare=lx.(x tl tr bl br) \begin{align*} \textrm{tl}&=
\lambda x.(x\ \textrm{tl}\ \textrm{tr}\ \textrm{bl}\ \textrm{b})\\ \
textrm{tr}&=\lambda x.(x\ \textrm{tl}\ \textrm{tr}\ \textrm{b}\ \
textrm{br})\\ \textrm{bl}&=\lambda x.(x\ \textrm{tl}\ \textrm{b}\ \
textrm{bl}\ \textrm{br})\\ \textrm{br}&=\lambda x.(x\ \textrm{b}\ \
textrm{tr}\ \textrm{bl}\ \textrm{br})\\ \textrm{tsquare}&=\lambda x.
(x\ \textrm{tl}\ \textrm{tr}\ \textrm{bl}\ \textrm{br}) \end{align*} 
tltrblbrtsquare =lx.(x tl tr bl b)=lx.(x tl tr b br)=lx.(x tl b bl br
)=lx.(x b tr bl br)=lx.(x tl tr bl br) 

This relation can be solved using a variadic fixed-point combinator:

tl'=ltl tr bl br.lx.(x tl tr bl b)tr'=ltl tr bl br.lx.(x tl tr b br)
bl'=ltl tr bl br.lx.(x tl b bl br)br'=ltl tr bl br.lx.(x b tr bl br)
mutual=(y* la.(a tl' lb.(b tr' lc.(c bl' ld.(d br' nil))))) \begin
{align*} \textrm{tl}'&=\lambda tl\ tr\ bl\ br.\lambda x.(x\ tl\ tr\
bl\ \textrm{b})\\ \textrm{tr}'&=\lambda tl\ tr\ bl\ br.\lambda x.(x\
tl\ tr\ \textrm{b}\ br)\\ \textrm{bl}'&=\lambda tl\ tr\ bl\ br.\
lambda x.(x\ tl\ \textrm{b}\ bl\ br)\\ \textrm{br}'&=\lambda tl\ tr\
bl\ br.\lambda x.(x\ \textrm{b}\ tr\ bl\ br) \end{align*}\\ \textrm
{mutual}=(\textrm{y*}\ \lambda a.(a\ \textrm{tl}'\ \lambda b.(b\ \
textrm{tr}'\ \lambda c.(c\ \textrm{bl}'\ \lambda d.(d\ \textrm{br}'\
\textrm{nil}))))) tl'tr'bl'br' =ltl tr bl br.lx.(x tl tr bl b)=ltl tr
 bl br.lx.(x tl tr b br)=ltl tr bl br.lx.(x tl b bl br)=ltl tr bl br.
lx.(x b tr bl br) mutual=(y* la.(a tl' lb.(b tr' lc.(c bl' ld.(d br' 
nil)))))

Thus giving us the final term tsquare'\textrm{tsquare}'tsquare',
where the indices indicate the nnnth head selection of Church lists:

tsquare'=l_ x.(x mutual0 mutual1 mutual2 mutual3)\textrm{tsquare}'=\
lambda \_\ x.(x\ \textrm{mutual}_0\ \textrm{mutual}_1\ \textrm
{mutual}_2\ \textrm{mutual}_3)tsquare'=l_ x.(x mutual0  mutual1  
mutual2  mutual3 )

Render

"Sierpinski Carpet"

The exact drawing of the Sierpinski Carpet is left as an exercise to
the reader.

Since it's a bit more straightforward, I decided to generate a slight
variant^1 where each quadrant isn't split into 9 but 4 quadrants per
iteration.

Beautifully drawn visualization of the first three iterations. The
red marks will be stable (non-recursive) black squares, while the
grey squares will be stable white squares. Green and yellow lines
added to indicate the splitting of squares at each level. Beautifully
drawn visualization of the first three iterations. The red marks will
be stable (non-recursive) black squares, while the grey squares will
be stable white squares. Green and yellow lines added to indicate the
splitting of squares at each level.

Each new stable quadrant will be one of the following:

sub-tl=lx.(x b w w ly.(y w w w b))sub-tr=lx.(x w b ly.(y w w b w) w)
sub-bl=lx.(x w ly.(y w b w w) b w)sub-br=lx.(x ly.(y b w w w) w w b)
\begin{align*} \textrm{sub-tl}&=\lambda x.(x\ \textrm{b}\ \textrm{w}\
\textrm{w}\ \lambda y.(y\ \textrm{w}\ \textrm{w}\ \textrm{w}\ \textrm
{b}))\\ \textrm{sub-tr}&=\lambda x.(x\ \textrm{w}\ \textrm{b}\ \
lambda y.(y\ \textrm{w}\ \textrm{w}\ \textrm{b}\ \textrm{w})\ \textrm
{w})\\ \textrm{sub-bl}&=\lambda x.(x\ \textrm{w}\ \lambda y.(y\ \
textrm{w}\ \textrm{b}\ \textrm{w}\ \textrm{w})\ \textrm{b}\ \textrm
{w})\\ \textrm{sub-br}&=\lambda x.(x\ \lambda y.(y\ \textrm{b}\ \
textrm{w}\ \textrm{w}\ \textrm{w})\ \textrm{w}\ \textrm{w}\ \textrm
{b}) \end{align*} sub-tlsub-trsub-blsub-br =lx.(x b w w ly.(y w w w b
))=lx.(x w b ly.(y w w b w) w)=lx.(x w ly.(y w b w w) b w)=lx.(x ly.(
y b w w w) w w b) 

We again model the generation as a mutual recurrence relation:

tl=lx.(x tl tr bl sub-br)tr=lx.(x tl tr sub-bl br)bl=lx.
(x tl sub-tr bl br)br=lx.(x sub-tl tr bl br)carpet=lx.(x tl tr bl br)
\begin{align*} \textrm{tl}&=\lambda x.(x\ \textrm{tl}\ \textrm{tr}\ \
textrm{bl}\ \textrm{sub-br})\\ \textrm{tr}&=\lambda x.(x\ \textrm{tl}
\ \textrm{tr}\ \textrm{sub-bl}\ \textrm{br})\\ \textrm{bl}&=\lambda
x.(x\ \textrm{tl}\ \textrm{sub-tr}\ \textrm{bl}\ \textrm{br})\\ \
textrm{br}&=\lambda x.(x\ \textrm{sub-tl}\ \textrm{tr}\ \textrm{bl}\
\textrm{br})\\ \textrm{carpet}&=\lambda x.(x\ \textrm{tl}\ \textrm
{tr}\ \textrm{bl}\ \textrm{br}) \end{align*} tltrblbrcarpet =lx.(x tl
 tr bl sub-br)=lx.(x tl tr sub-bl br)=lx.(x tl sub-tr bl br)=lx.(x 
sub-tl tr bl br)=lx.(x tl tr bl br) 

Giving us, as before, the final term:

mutual=(y* la.(a tl' lb.(b tr' lc.(c bl' ld.(d br' nil)))))carpet'=
l_ x.(x mutual0 mutual1 mutual2 mutual3) \begin{align*} \textrm
{mutual}&=(\textrm{y*}\ \lambda a.(a\ \textrm{tl}'\ \lambda b.(b\ \
textrm{tr}'\ \lambda c.(c\ \textrm{bl}'\ \lambda d.(d\ \textrm{br}'\
\textrm{nil})))))\\ \textrm{carpet}'&=\lambda \_\ x.(x\ \textrm
{mutual}_0\ \textrm{mutual}_1\ \textrm{mutual}_2\ \textrm{mutual}_3)
\end{align*} mutualcarpet' =(y* la.(a tl' lb.(b tr' lc.(c bl' ld.(d 
br' nil)))))=l_ x.(x mutual0  mutual1  mutual2  mutual3 ) 

Render

There's obviously huge potential for golfing the term size - so if
you're into that, have fun!

Cantor Dust

The Cantor dust is another great example of how infinitely detailed
structures appear as unreduced (grey) quadrants when reduction
inevitably gets halted.

In this case, a square gets recursively split into four new squares.
Since we do the same split four times, we can construct the new
quadrant using a quadruple\textrm{quadruple}quadruple function:

quadruple=lq x.(x q q q q)cantor=lx.(tl tr bl br)tl=(quadruple 
(lx.x cantor b b b)tr=(quadruple (lx.x b cantor b b)bl=(quadruple 
(lx.x b b cantor b)br=(quadruple (lx.x b b b cantor) \begin{align*} \
textrm{quadruple}&=\lambda q\ x.(x\ q\ q\ q\ q)\\ \textrm{cantor}&=\
lambda x.(\textrm{tl}\ \textrm{tr}\ \textrm{bl}\ \textrm{br})\\ \
textrm{tl}&=(\textrm{quadruple}\ (\lambda x.x\ \textrm{cantor}\ \
textrm{b}\ \textrm{b}\ \textrm{b})\\ \textrm{tr}&=(\textrm{quadruple}
\ (\lambda x.x\ \textrm{b}\ \textrm{cantor}\ \textrm{b}\ \textrm{b})\
\ \textrm{bl}&=(\textrm{quadruple}\ (\lambda x.x\ \textrm{b}\ \textrm
{b}\ \textrm{cantor}\ \textrm{b})\\ \textrm{br}&=(\textrm{quadruple}\
(\lambda x.x\ \textrm{b}\ \textrm{b}\ \textrm{b}\ \textrm{cantor})\\
\end{align*} quadruplecantortltrblbr =lq x.(x q q q q)=lx.(tl tr bl 
br)=(quadruple (lx.x cantor b b b)=(quadruple (lx.x b cantor b b)=(
quadruple (lx.x b b cantor b)=(quadruple (lx.x b b b cantor) 

After removing the recursive calls using y\textrm{y}y, we get

Render

* * **\ *\ ** * *

All of the examples above (and more) can also be found, rendered, and
modified here.

Utilities

Lastly, here are some useful terms for experimentation (also
available in the "template" preset).

Checking whether a pixel ppp is black or white: w?=lp.pb?=lp.(p b w)
\begin{align*} \textrm{w?}&=\lambda p.p\\ \textrm{b?}&=\lambda p.(p\
\textrm{b}\ \textrm{w}) \end{align*} w?b? =lp.p=lp.(p b w) 

Inverting the state of pixel ppp: invert=c=lp x y.(p y x)\textrm
{invert}=\textrm{c}=\lambda p\ x\ y.(p\ y\ x)invert=c=lp x y.(p y x)

Getting the term at a position ppp of screen sss:

tl=ltl tr bl br.tltr=ltl tr bl br.trbl=ltl tr bl br.blbr=
ltl tr bl br.brget=lp s.(s p) \textrm{tl}=\lambda tl\ tr\ bl\ br.tl\
quad \textrm{tr}=\lambda tl\ tr\ bl\ br.tr\\ \textrm{bl}=\lambda tl\
tr\ bl\ br.bl\quad \textrm{br}=\lambda tl\ tr\ bl\ br.br\\ \textrm
{get}=\lambda p\ s.(s\ p) tl=ltl tr bl br.tltr=ltl tr bl br.trbl=ltl 
tr bl br.blbr=ltl tr bl br.brget=lp s.(s p)

Replacing a quadrant of screen sss with qqq:

tl!=ls q.(s ltl tr bl br x.(x q tr bl br))tr!=ls q.(s ltl tr bl br x.
(x tl q bl br))bl!=ls q.(s ltl tr bl br x.(x tl tr q br))br!=ls q.
(s ltl tr bl br x.(x tl tr bl q)) \begin{align*} \textrm{tl!}&=\
lambda s\ q.(s\ \lambda tl\ tr\ bl\ br\ x.(x\ q\ tr\ bl\ br))\\ \
textrm{tr!}&=\lambda s\ q.(s\ \lambda tl\ tr\ bl\ br\ x.(x\ tl\ q\ bl
\ br))\\ \textrm{bl!}&=\lambda s\ q.(s\ \lambda tl\ tr\ bl\ br\ x.(x\
tl\ tr\ q\ br))\\ \textrm{br!}&=\lambda s\ q.(s\ \lambda tl\ tr\ bl\
br\ x.(x\ tl\ tr\ bl\ q))\\ \end{align*} tl!tr!bl!br! =ls q.(s ltl tr
 bl br x.(x q tr bl br))=ls q.(s ltl tr bl br x.(x tl q bl br))=ls q.
(s ltl tr bl br x.(x tl tr q br))=ls q.(s ltl tr bl br x.(x tl tr bl 
q)) 

Applying each quadrant of a screen sss to a function fff:

map=lf s.(s ltl tr bl br.lx.(x (f tl) (f tr) (f bl) (f br)))\textrm
{map}=\lambda f\ s.(s\ \lambda tl\ tr\ bl\ br.\lambda x.(x\ (f\ tl)\
(f\ tr)\ (f\ bl)\ (f\ br)))map=lf s.(s ltl tr bl br.lx.(x (f tl) (f t
r) (f bl) (f br)))

Of course you could also use the definition of any function in
bruijn's standard library.



Thanks for reading. Contact me via email. Support on Ko-fi. Subscribe
on RSS. Discuss on Reddit. Follow on Mastodon.

I've also applied for a talk about this topic at GPN22 in Karlsruhe,
so you may see me there as well.

Other project updates

I haven't posted in a while, mainly due to university and work, but
also because I worked on some of my projects:

  * bruijn: Implemented new reducers (ION, HigherOrder), added a very
    basic optimizer, wrote many samples (Rosetta Code, Project Euler,
    Advent of Code)
  * infinite-apply: Infinite craft, but for pure lambda calculus
  * BLoC/BLoCade: File format, optimizer and targeted compiler for
    lambda calculus (WIP)

---------------------------------------------------------------------

 1. It may also be a variant of the T-Square, not sure about the
    exact definitions. Looks pretty though.-[?]

  * Share on Twitter
  * Share on Mastodon

[noscript]