You’re walking through a term. A term that will take you far away. You know where you hope this term will take you, but you can’t know for sure. Yet it doesn’t matter. Now tell me why?
This will be part of a series, based on some of my notes
(←PoW re. LLM use) Nowadays, the λ-calculus is almost always introduced in the same way: There is the widely-accepted minimal syntax, potentially using some surprising rule for parentheses, or some very unusual way of declaring substitutions – no surprises. Today, I want to show a completely different (dual!) view on its syntax, that you might find surprising, and I have found to be almost more natural. It is what you observe when walking through a λ-term with different strategies, and writing down the views as you go.
However, let’s first introduce the λ-calculus in a standard way. Well, here’s the minimal syntax introducing the two constructors:
Note the coinductive construction: I like to use symbol f and a to mean the function and argument of applications, and x and b to mean the variable and body of abstractions.
You then have the one reduction relation to rule them all,
β-reduction:
(λx.b)a⊳b[a/x],
that annihilates the two constructors by replacing all x in scope with a, being especially careful to preserve the bindings of a and b. Usually, this is then done using some specific strategy that aims to find some kind of normal form of the term.
Yes, this notation works very well, especially given the semantics we would expect. However, the lack of surprises is exactly what I find boring when trying to explore and play with it.
Variables
One thing I was confused by since I learned this definition around five years ago, is the concept of a variable.
(terminology rant) In the context of imperative programming languages, I always believed the term “variable” to refer to its mutability. In the context of maths, I always believed the term “variable” to refer to its variable state, as a function typically ranges over many inputs – if it was fixed, it would be a constant. Yet, in the λ-calculus you cannot mutate a variable, nor can you call a function multiple times with different arguments – they are anonymous! If you were to duplicate a function to apply it to different arguments (e.g. by λfxy.fx(fy)), there would now be two, different functions, both with a constant input! After all, the most appealing part of the λ-calculus is its purity and determinism. Thus there is no such thing as variables in the pure λ-calculus.
Aside from the minor syntactic confusion, this “variable” term also confused me semantically: What does it really mean to construct or destroy a binding? What exactly is the meaning of scope, and why do we need it? Do we even need bindings at all? In fact, named bindings are so annoying that the literature introducing them either defines complex renaming machinery (α-equivalence), tries to ignore all the common fallacies by “Barendregt convention”, introduces sophisticated machinery to make scoping explicit (Hendriks and Oostrom 2003), or attempts using even more annoying schemes like de Bruijn indices/levels.
Just like in the real world, I believe that fully embracing a reductionist point of view may present us with some valuable insights. After some time of working with many various encodings, I finally realized: The λ-calculus is merely a useful abstraction modelling its underlying elementary components. The λ-calculus is not as minimal and elegant as I thought after all! This might not come to a surprise to some of you, but, indeed, variables are merely used for encoding the connections (wires) between its minimal constructors. We do not need them if we do not care about textual presentation – scoped bindings exist only for easier interpretation by humans. The λ-calculus is merely a restrictive, small window into some underlying graph encoding. In fact, even just the operational semantics of graph reduction has many more capabilities than the pure λ-calculus.
Ultimately, my goal is to have no traditional variables anywhere at all, thus eliminating the complexities of renaming and scoping.
Continuations
But let’s start at the beginning – namely the secret that the holy Church (et al.) is trying to hide from you: Continuations are hidden within your precious λ-terms in the form of implicit, syntactic continuations! This magic trick only works by restricting continuations to be used linearly (exactly once), as otherwise the syntax would have to be multi-dimensional, which is both hard to read and write.
Let’s show this using an example: K≏λxy.x, a common term erasing its second argument. If we have, say, ((KK)K), the continuation of (KK) is exactly
(□K). To me, it helps imagining myself to be inside of the λ-term and looking in different directions, observing the views. For this graphical intuition, let us draw both of the constructors as nodes having three wires. Here, all uplinks from nodes encode the continuations – the next immediate connected term.
K then looks like the following:
Observe how the second λ’s body b is connected to x, whereas the first λ’s body is not connected at all, thus matching the definition of K≏λxy.x.
Let’s now imagine being a TikZ duck within the ((KK)K) term. What can we observe from the different positions?
Wizard duck : We see the interpreter (or prompt), eager to interact with the term from the perspective of the real world.
Evil duck : We are at (KK), thus seeing the other K as the right side of the outer application, (□K). We’re not looking at the term behind us (□), nor can we see far enough to see the continuation of the constructor we’re looking at.
Hero duck :
((KK)□). Unicorn duck :
(□K). Harlequin duck :
(K□). You might rightly point out here that I have given no reason why the ducks cannot see far enough to observe the continuations of the terms. This is exactly the idea behind this entire blog post: There is no reason! The only problem is that we then observe the terms from below, which is not the usual perspective for looking upon terms. So, let’s figure out, incrementally, what is required for this unusual perspective.
You can observe how there is seemingly made no difference between the “variable” and “body” fields of an abstraction – they are both just wires. It therefore makes sense to view continuations as just another common wire. Indeed, we can describe the constructors as triples λ(k,x,b) and α(f,a,k), where x,b,f,a,k are now symbols that connect the constructors with each other by having the same name. There is no more syntax-enforced ordering of these constructors; they can just be put into a set, where k is the prompt:
K≏{λ(k,x,b),λ(b,y,x)} However, even this does not provide us with the real observable views that the ducks have at each position – from the perspective of any wire, we now only see even more wires attached to nodes! To continue, we need to recognize another property.
Polarization
Terms have a polarity1 that divides them into
producing (positive) and
consuming (negative) components. For
example, choosing by coin-flip that constructors are producers, we see that K, λx.x, and even (KK) all have positive polarity. The negative polarity only becomes relevant with the introduction of variables, as they wire the individual components with different polarities together. Just as in the real world, wires go from positive to negative polarity, and never connect two components of the same polarity. Specifically, you can imagine wires as enabling the communication between the dual worlds of terms and coterms. Let’s look at the previous graph with arrows as wires:
The reasoning behind the choice of polarization is as follows: Both function f and argument a of applications may contain other producing constructors as immediate subterms, therefore they must be negative, as they are wired to a producers’s continuation k. Similarly for the abstraction’s body b. Only the abstraction’s variable binding is in a confusing position: As variables may be used in consuming position (e.g. in (xy)), the bound occurrences must be negative, whereas the binding instance must be positive.2
The final set of polarized constructors is therefore:
{λ(k,x,b),α(f,a,k)}. As an aside, this duality of opposing polarity between both constructors is precisely the reason why β-reduction works in the first place. During β-reduction, the following abstract components flow into each other: The application’s function f interacts with the abstraction’s continuation k ((λx.b)a), the application’s argument a flows into the abstraction’s x binding ([a/x]), and the substituted body b gets returned to the application’s continuation k
(⊳b[a/x]).
{}λ(k,x,b),α(↑↑↓α(f,a,k)
We have now observed that there is almost nothing special about variables, they are just encoding directed wires. Therefore, in my opinion, the syntax λx.b is downright confusing – it puts x into such a special spot, not allowing for immediate subterms, even though technically a notation exactly dual to b could be used.
Let me show what I mean, by deriving the syntax by walking through a graph of K: In the previous notation λxy.x, we traverse the body b (i.e. λy.x and x) first, and only then wire the remaining free symbols back to a binding instance in producing position x. Instead, we could also traverse the subterms from the other side (the binding instance), thus observing a different view of the traversed constructors.
Syntax
We are now finally able to slightly abstract over the concept of wires and explicit continuations again. Here’s all the different views in a single syntax:
where v-wire/abstraction/application means that we view the wire/abstraction/application from the point of v, thus observing only its fields excluding v. Note how all colorings are exactly dual – in fact, as all of the variations of abstraction and applications have differently colored parentheses, I might as well have used the same symbols (which is why they’re sometimes described as a single ζ-constructor (Mazza 2007)). Note also, how the coloring swapped in comparison to before: Previously, b,f,a,x,k, were merely wires – now they can represent subterms directly, without requiring the wire’s indirection. The wires still connect opposing terms by having the same name, thus having opposite polarization in syntax as well.
We can now view both constructors from all three sides. For the abstraction:
Unicorn duck :
[xb] Wizard duck :
[bk] Harlequin duck :
[kx] You can see that the colors match exactly whether the observable term at the other sides of the wires are consumers/producers.
Of course, compared to before, we can now actually see the terms behind consumers without indirection. Let’s take our beloved K as example. The standard notation now becomes
[x[yx]]
(≏λx.λy.x).
However, a different view shows up if we instead start walking from the abstraction’s x: [[by]b], where b is indeed a k
(try walking the term in your head!) Just as with y in traditional λ-calculus, it occurring only as binding instance y means that nodes trying to consume it shall effectively get garbage-collected – similar with symbols not being bound at all (free variables). The difference in our syntax is that there is no scoping involved – “variables” never get “instantiated”, as they do not exist as such, they merely wire the positive and negative terms together. Barendregt convention emerges by construction!
Theoretically, you could traverse nodes multiple times, thus resulting in larger notations that would not represent the original term anymore. In practice, figuring out the notation for a given graph-encoded λ-term can be done using standard BFS-style graph traversal by storing each end of a visited wire in a visited set.
However, we can still go further without misrepresenting the term. Currently, we start traversal from the real world “prompt” continuation. Instead, we can use explicit starting points in our calculus to allow specifying one of the ends of a wire at the top-level:
Viewspp::=::=σbσkσ−termσ−term
For example, setting as invariant that
k always exists as wire to the outermost continuation (the prompt), we can traverse K again, this time from k explicitly: k[x[yx]], and k[[by]b]. Yet, we could also start from, say, y: y[x[kx]], or even y[[bk]b]. I’ll leave it as a task to the reader to find the remaining 4 valid encodings.
Here’s the route you got to take to observe
y[x[kx]]
(red path) and
y[[bk]b]
(blue path):
It might be interesting to observe that this is now a combinatorial problem. For example, to count the number of valid encodings of a Church numeral n, we’d calculate (n+4)[(n+33)+(n+12)]. Here are the 78 valid encodings of
λsz.s(sz): View
a([[k(za)]z]s)
a([[ks](as)]s)
a([b(a[bk])]s)
a([b(as)][bk])
a(b1[[(as)b1]k])
b1[[k((sz)b1)]z]
b1[[k(ab1)](as)]
b1[[k(z(b1s))]z]
b1[[ks]((b1s)s)]
b1[b((b1[bk])s)]
b1[b((b1s)[bk])]
b[k((s[b1b])b1)]
b[k((sz)[bz])]
b[k([(sa)b]a)]
b[k([b1b](b1s))]
b[k(a[b(as)])]
b[k(z([bz]s))]
s(([[zb1]k]z)b1)
s(([bk][b1b])b1)
s(([bk]z)[bz])
s((s[b1[ks]])b1)
s((sz)[[ks]z])
s([([bk]a)b]a)
s([(sa)[ks]]a)
s([b1[k(ab1)]]a)
s([b1[ks]](b1s))
s([b1b](b1[bk]))
s(a[[k(za)]z])
s(a[[ks](as)])
s(a[b(a[bk])])
s(z([[ks]z]s))
s(z([bz][bk]))
s(z(b1[[zb1]k]))
z(([[ks]z]s)s)
z(([bz][bk])s)
z(([bz]s)[bk])
z((b1[[zb1]k])s)
z((b1s)[[zb1]k])
z(a[[z(sa)]k])
a([[z(sa)]k]z)
a([bk][(sa)b])
a(s[([bk]a)b])
a(s[(sa)[ks]])
a(s[b1[k(ab1)]])
b1([[(as)b1]k]a)
b1([[zb1]k](sz))
b1([bk](s[b1b]))
b1(s([[zb1]k]z))
b1(s([bk][b1b]))
b1(s(s[b1[ks]]))
b[((b1[bk])s)b1]
b[((b1s)[bk])b1]
b[(a[bk])(sa)]
b[(as)([bk]a)]
b[z([bk](sz))]
b[z(s([bk]z))]
k[((s[b1b])b1)b]
k[((sz)[bz])b]
k[((sz)b1)[zb1]]
k[([(sa)b]a)b]
k[([b1b](b1s))b]
k[(a[b(as)])b]
k[(ab1)[(as)b1]]
k[(z([bz]s))b]
k[(z(b1s))[zb1]]
k[(za)[z(sa)]]
k[s[((b1s)s)b1]]
k[s[(as)(sa)]]
k[s[z(s(sz))]]
s[[((b1s)s)b1]k]
s[[(as)(sa)]k]
s[[z(s(sz))]k]
z[([bk](sz))b]
z[(s([bk]z))b]
z[(s(sz))[ks]]
z[(sa)[k(za)]]
z[b1[k((sz)b1)]]
z[b1[k(z(b1s))]]
Inference
You may have realized that I have omitted the highlighting of positive/negative parentheses. This is in part due to being lazy, but also due to being able to always infer it based on the polarity of its subterms (which, inductively, can be inferred based on the polarity of the symbols). In fact, one can even infer the polarity of all the symbols based on the polarity of a single symbol. Making use of the invariant of k, we can infer its neighboring term’s polarity, and then inductively the polarity of all the terms. This is, with the assumption that we follow standard restrictions of λ-terms. Here’s a small sketch of how this inference might look like, typing terms ⊢e:τ either as positive (⊢e:+) or negative (⊢e:−), arranged to showcase the duality:
And, indeed, there is no other valid coloring, as k cannot be combined with negative terms – you would also have to swap the positions to
k[[xy]x]. Semantics
Let’s assume that, for simpler reduction, the term structure is fully lifted again – every subterm is a wire to another term, there are no immediate subterm relations. We can easily transform from the graph encoding into a map of
σ→e,
σ→e,
interconnected by wires.
However, let’s still keep the notation of immediate
subterms,
e.g. ([xb]a)
instead of {σ1↦[xb],k↦(σ1a),…}. A traditional β-redex then looks like ([xb]a)⊳b,[a/x], where [a/x] is now a global substitution (remember, there is no lexical scope). We assume that any x/x always has matching x/x somewhere, or it is supposed to get (co-)erased (nothing gets substituted)
Due to the many different introduced views, there now exist multiple ways to write this β-redex. And, of course, they are perfectly dual again, encoding the flows of β-reduction even inbetween:
The subfix v in ev indicates the view from which we look upon the redex.
Here are all combinations of different views on abstractions and applications and whether they form valid
β-redexes: Term
[kx]
[xb]
[bk]
(fa)
𐄂
✔
𐄂
(ak) ✔
𐄂
✔
(kf) 𐄂
✔
𐄂
You may realize that technically there are many more valid terms involving both abstraction and application in a subterm relation (e.g. [(fa)k] or even [(kf)b]). However, this relation is not between the abstraction’s k and the application’s f. Yet, it turns out that these other terms have very interesting behavior when seen as redexes, and I plan to discuss them in one of my next posts (RSS) – as a spoiler: call/cc and fixpoint recursion just appear out of nowhere!
Next
There are many more things I plan to discuss next. For example, I did not yet discuss the programs where unscoped bindings are truly useful in practice. What I also did not explain yet, is that these wired bindings are in fact hyperedges: Both of its sides may connect to multiplepositive/negative terms. Theoretically our syntax then allows mentioning k (in fact, any continuation symbol) multiple times, or not at all. This goes exactly against one of the imposed restrictions I discussed in the beginning, namely that continuations must be used linearly. The concept of duplicating continuations is typically referred to as superposition, coduplication, cocontraction, or even multiple resumption. In our case it is n-ary, as k can be mentioned an arbitrary number of times, therefore implementing coerasure/coweakening as well. The idea is that, since constructors are producers, referring to multiple continuations of constructors as a single continuation essentially merges (superposes) them into a single producer. We will see that such cases are exactly where we actually require the use of dual syntax, non-existent in traditional λ-calculus.
Related Work
You may be interested in further information about the duality of λ-abstraction and its graph encodings. Here are some resources related to this post:
Zeilberger (2016) presents a graph encoding for the linearλ-calculus
with support for re-rooting the graph (without syntax)
Lafont (1997) and Mazza (2007) present (symmetric)
interaction combinators as an encoding of programs as graphs of nodes, though they use explicit, incremental resource management (problematic (Asperti 2017)) and do not present a dual syntax
Ostermann et al. (2022) aim to develop a shared symmetric syntax for producer/consumer symmetry
(not based on graphs) As always, thanks for reading! Don’t take anything too serious here, it may contain many mistakes, as it is mostly a playground. I’d still love your input on this, I’m very interested in formalization and additional details. There might be a lot more coming in the next few months though, anyway.
Also, I’ll be at the “coICFP” FPW26 in Paris next week, presenting “Graph Rewriting via Lexical Effect Handlers” at HOPE, introducing an approach for effect-directed programming. Let me know if you want to meet or explore Paris together! (email, signal, discord)
Asperti, Andrea. 2017. “About the Efficient Reduction of Lambda Terms.”arXiv Preprint arXiv:1701.04240.
Curien, Pierre-Louis, and Hugo Herbelin. 2000. “The Duality of
Computation.”ACM Sigplan Notices 35 (9): 233–43. Hendriks, RDA, and Vincent van Oostrom. 2003. “Adbmal.”Lecture Notes in Computer Science 2741: 136–50.
Lafont, Yves. 1997. “Interaction Combinators.”Information and Computation 137 (1): 69–101.
Mazza, Damiano. 2007. “A Denotational Semantics for the Symmetric Interaction Combinators.”Mathematical Structures in Computer
Science 17 (3): 527–62. Ostermann, Klaus, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen. 2022. “Introduction and Elimination, Left and Right.”Proceedings of the ACM on Programming Languages
6 (ICFP): 438–65. Sabry, Amr, and Philip Wadler. 1997. “A Reflection on Call-by-Value.”ACM Transactions on Programming Languages and
Systems (TOPLAS) 19 (6): 916–41. Zeilberger, Noam. 2016. “Linear Lambda Terms as Invariants of Rooted Trivalent Maps.”Journal of Functional Programming 26: e21.
动态网自由门 天安門 天安门 法輪功 李洪志 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 劉曉波动态网自由门