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)
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)To see it in action, we can use y to find the
factorial of
.
:import std/Number .
g [[=?0 (+1) (0 ⋅ (1 --0))]]
factorial y gAs 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.
The
-ary
Y-combinator y is only
capable of finding the fixed-point of a single function. There are ways
of writing
-ary
variations for specific
and
,
such that we are able to select the fixed-point of the
-th
term out of
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
and could be simplified such that
would refer to the outermost function. Although this introduces some
confusing ordering, I will keep it this way to comply with the
paper.
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
-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
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 hThis 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.
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)]] <$> 0Be 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?
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 1This 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.
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
functions depend on each other:
th
order mutual recurrence relations.
Some examples:
even?, positive? or
even minmaxI 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