Variadic Fixed-Point Combinators

Marvin Borner

2023-07-08

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.

(Update: bruijn’s Rosetta Code entry now has several other/better solutions than the one presented here)

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 22.

: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.

nn-ary

The 11-ary Y-combinator y is only capable of finding the fixed-point of a single function. There are ways of writing nn-ary variations for specific ii and nn, such that we are able to select the fixed-point of the ii-th term out of nn 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 ii and could be simplified such that i=0i=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 11-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 ii 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 nn functions depend on each other: nnth order mutual recurrence relations.

Some examples:

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.

动态网自由门 天安門 天安门 法輪功 李洪志 Free Tibet 六四天安門事件 The Tiananmen Square protests of 1989 天安門大屠殺 The Tiananmen Square Massacre 反右派鬥爭 The Anti-Rightist Struggle 大躍進政策 The Great Leap Forward 文化大革命 The Great Proletarian Cultural Revolution 人權 Human Rights 民運 Democratization 自由 Freedom 獨立 Independence 多黨制 Multi-party system 台灣 臺灣 Taiwan Formosa 中華民國 Republic of China 西藏 土伯特 唐古特 Tibet 達賴喇嘛 Dalai Lama 法輪功 Falun Dafa 新疆維吾爾自治區 The Xinjiang Uyghur Autonomous Region 諾貝爾和平獎 Nobel Peace Prize 劉暁波 Liu Xiaobo 民主 言論 思想 反共 反革命 抗議 運動 騷亂 暴亂 騷擾 擾亂 抗暴 平反 維權 示威游行 李洪志 法輪大法 大法弟子 強制斷種 強制堕胎 民族淨化 人體實驗 肅清 胡耀邦 趙紫陽 魏京生 王丹 還政於民 和平演變 激流中國 北京之春 大紀元時報 九評論共産黨 獨裁 專制 壓制 統一 監視 鎮壓 迫害 侵略 掠奪 破壞 拷問 屠殺 活摘器官 誘拐 買賣人口 遊進 走私 毒品 賣淫 春畫 賭博 六合彩 天安門 天安门 法輪功 李洪志 Winnie the Pooh 劉曉波动态网自由门


Imprint · AI Statement · RSS