# A Dual View on Syntax

> Source: <https://text.marvinborner.de/2026-08-11-17.html>
> Published: 2026-08-17 11:17:07+00:00

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 劉曉波动态网自由门