Most algorithms in programming require some kind of loops/recursion. Lambda calculus and therefore the bruijn programming language don’t have such procedures. Instead, lambda calculus uses “fixed-point combinators” to imitate their behavior.

This article will present a variadic extension to the most common fixed-point combinator. It will also give examples of how to use these combinators in bruijn.

The ideas in this article are heavily inspired by Mayer Goldbergs paper on “A Variadic Extension of Curry’s Fixed-Point Combinator”. You may want to see this article as a translation of their algorithms to bruijn, or pure lambda calculus in general.

Also see my codegolf question and my Rosetta Code task for implementations in other programming languages.

Y-combinator

As in the paper but also because it’s the most common, I want to focus on the Y-combinator. I believe that similar extensions can be applied to the z and θ combinators, though.

The Y-combinator is defined by:

y [[1 (0 0)] [1 (0 0)]]

The reduction of the application with some term g proves its capabilities of finding the fixed-point:

  (y g)
⤳ [[1 (0 0)] [1 (0 0)]] g
⤳ [g (0 0)] [g (0 0)]
⤳ g ([g (0 0)] [g (0 0)])
≡ g (y g)

Example

To see it in action, we can use y to find the factorial of $2$.

:import std/Number .

g [[=?0 (+1) (0 ⋅ (1 --0))]]

factorial y g

As in all reductions in lambda calculus, the specific order of reduction doesn’t matter. Also note the ≡ which uses the previously found equivalence to replace (y g) with (g (y g)).

  (y g (+2))
≡ g (y g) (+2)
⤳ [=?0 (+1) (0 ⋅ (y g --0))] (+2)
⤳ =?(+2) (+1) ((+2) ⋅ (y g --(+2)))
⤳ (+2) ⋅ (y g (+1))
≡ (+2) ⋅ (g (y g) (+1))
⤳ (+2) ⋅ ([=?0 (+1) (0 ⋅ (y g --0))] (+1))
⤳ (+2) ⋅ (=?(+1) (+1) ((+1) ⋅ (y g --(+1))))
⤳ (+2) ⋅ (+1) ⋅ (y g (+0))
≡ (+2) ⋅ (+1) ⋅ (g (y g) (+0))
⤳ (+2) ⋅ (+1) ⋅ ([=?0 (+1) (0 ⋅ (y g --0))] (+0))
⤳ (+2) ⋅ (+1) ⋅ (=?(+0) (+1) ((+0) ⋅ (y g --(+0))))
⤳ (+2) ⋅ (+1) ⋅ (+1)
⤳ (+2)

Notice how we don’t pass the function itself to the “recursive” (1 --0) call – the Y-combinator handles this for us. This behavior is the purpose of fixed-point combinators and will also be relevant for their extensions.

$n$-ary

The $1$-ary Y-combinator y is only capable of finding the fixed-point of a single function. There are ways of writing $n$-ary variations for specific $i$ and $n$, such that we are able to select the fixed-point of the $i$-th term out of $n$ given terms.

# meta notation, read the paper for more information
yin [ⁿ[ⁿn+n-i (n-1ⁿ 0) ...ⁿ⁻² (0 n-1ⁿ⁻¹ 0)] ...ⁿ⁻² [ⁿn+n-i (n-1ⁿ 0) ...ⁿ⁻² (0 n-1ⁿ⁻¹ 0)]]

# example for i=1, n=1 -- normal y!
y11 [[1 (0 0)] [1 (0 0)]]

# example for i=1, n=2
y12 [[[[3 (1 1 0) (0 1 0)]] [[3 (1 1 0) (0 1 0)]] [[2 (1 1 0) (0 1 0)]]]]

# example for i=2, n=2
y22 [[[[2 (1 1 0) (0 1 0)]] [[3 (1 1 0) (0 1 0)]] [[2 (1 1 0) (0 1 0)]]]]

Note: The n+n-i is the result of the “reversed” (in De Bruijn sense) index $i$ and could be simplified such that $i=0$ would refer to the outermost function. Although this introduces some confusing ordering, I will keep it this way to comply with the paper.

Example

Let’s say we want to find out whether a number is even or odd.

One idea would be the following mutual recurrence relation:

:import std/Logic .

even? [=?0 true (odd? --0)]

odd? [=?0 false (even? --0)]

This method, while correct in theory, can’t trivially be written as a single expression: Substituting the respective terms would result in infinite definitions of even?/odd? – a paradox.

We can extend the definitions such that we pass the corresponding functions as an argument. Furthermore, we will define the “recursive” call – similar to before – without passing the functions themself as arguments.

# the odd? recursive call will be the second argument (1)
g [[[=?0 true (1 --0)]]]

# the even? recursive call will be the first argument (2)
h [[[=?0 false (2 --0)]]]

Previously, we used the $1$-ary Y-Combinator to imitate a single “recursive” call. We did this by using its (y g) = g (y g) behavior. This time, we have two functions g/h that can call themself, basically (y* g h) = h (y* g h) and also (y* g h) = g (y* g h).

We can finally use the yin definition to implement the actual functionality. As we have two functions, we use yi2. The $i$ corresponds to the index of the argument whose fixed-point we want to find.

# i=1, n=2: Find fixed-point of g
even? y12 g h

# i=2, n=2: Find fixed-point of h
odd? y22 g h

This might seem quite useless and overly complicated – I will show more useful examples later.

Deriving the respective yin combinator for different use cases manually is very annoying, so let’s look at a way of generating them automagically.

Variadicity

The derivation of the generic version is explained in detail in the paper. I adapted the code to not use variadic list arguments (although one could probably translate them to variadic from std/List):

(define curry-fps
  (lambda (fs)
    (let ((xs
           (map
            (lambda (fi)
              (lambda (xs)
                (apply fi
                       (map
                        (lambda (xi)
                          (lambda (args)
                            ((xi xs) args)))
                        xs))))
            fs)))
      (map (lambda (xi)
             (xi xs)) xs))))

Translating curry-fps to bruijn gives the following function y*:

:import std/List .

y* [[[0 1] <$> 0] xs]
    xs [[1 <! ([[1 2 0]] <$> 0)]] <$> 0

Be aware that apply (…<!…) and map (…<$>…) are in turn implemented using fixed-point combinators and therefore aren’t even remotely as performant as the equivalent Scheme code.

We can now redefine the previous even? and odd? functions using the generic approach:

even? ^(y* (g : {}h))

odd? _(y* (g : {}h))

Isn’t it beautiful?

Performance

Aside from beauty, writing the even?/odd? functions this way is not beneficial at all: Deciding whether (+10000) is even takes around 5 seconds using the mutual recurrence relation with y* and 3 seconds using its equivalent code using y (according to bruijn’s :time command):

:import std/Number .
:import std/Combinator .
:import std/Logic .

even? y [[[=?0 case-end case-rec]]] true
    case-rec 2 ¬1 --0
    case-end 1

This implementation has, in theory, more logical operations than the previous version, yet its performance is much better. This is because the “recursive” behavior of the fixed-point combinators involve quite a lot of copying and garbage collecting (at least in most reducers) – adding multi-layered recursive calls will then take even more resources.

Fun fact: The optimized default even? function takes 0.002 seconds and is defined in std/Number/Ternary. It would obviously be possible to apply similar optimizations to the mutually recursive even? function.

Usecases

First of all, y* enables us to write code in a letrec-style much easier: Expressions of the type (letrec ((f1 M1) ... (fn Mn)) expr) can be translated to the bruijn expression (y* ([ⁿ expr] : ([ⁿ M1] : (... : {}[ⁿ Mn])))).

It follows that the main use case of y* is when $n$ functions depend on eachother: $n$th order mutual recurrence relations.

Some examples:

• $n$-based functions with multiple output states like even?, positive? or even minmax
• parsers with inter-dependent structures (“recursive descent parser”, e.g. many programming languages)
• general traversal operations like leaf-counting in trees
• simulations of more complex finite-state machines

Conclusion

I believe that the y* function serves as a useful addition to the standard library of bruijn. Although its usage is not always trivial and can lead to poor performance, it can also result in quite elegant and expressive functions.

I also think that the reducer of bruijn could be optimized in regard to reduction of fixed-point combinators – feel free to contribute.

$$❦$$

Thanks for reading. Suggest improvements or fixes via email. Discuss on reddit. Support on Ko-fi.