λ-term
A tiny functional program. λx.t means “a function taking x with body t”; t u means “apply t to u.”
λL — linear
Each bound variable appears exactly once.
Read this before the notation
Δ-Nets is a proposed graph-rewriting model: it represents a program as connected nodes, then repeatedly replaces small matching pieces of that graph. Its aim is optimal parallel reduction: avoid work that will later be thrown away, and perform each necessary reduction once even when an expression has several uses.
The core idea
Represent a program as a net of very small agents. Let local pairs interact independently, with sharing described directly in the graph.
The important caveat
“Optimal” and the confluence guarantees here are the author’s claims, argued in the linked paper. This guide presents the design; the formal arguments and proofs are in the source paper.
Six ideas you need before Chapter 1
Bound vs. free
An occurrence of x is bound when a surrounding λx introduced it. It is free when no surrounding abstraction does.
Redex and reduction
A redex is a reducible expression—here, a function already next to its argument. A reduction is one simplification step.
Normal form
A term or net is in normal form when no reduction remains. Normalizing means a sequence of steps eventually reaches that state.
Sharing and erasure
Sharing means one argument has several uses; erasure means a function ignores an argument. They create the two kinds of avoidable work this paper studies.
Net and local rewrite
A net is a graph of small nodes and wires. A local rule uses the tiny connected pattern it changes as its complete input.
01 Motivation
The problem is wasted work.
Ordinary λ-calculus is wonderfully compact, but its familiar “replace a variable with an argument” story hides a cost question: what should happen when the variable is unused—or appears many times?
1.1 A tiny reminder: what reduction does
Read λx.t as a function: x is the name it gives its incoming argument and t is its body. Placing it beside u, as in (λx.t)u, applies the function to that argument. This whole pattern is a β-redex (pronounced “bee-redex”): one place where a β-reduction can occur.
A β-reduction performs that application. In the compact notation below, the argument u is substituted for every occurrence of x in the body t. If there are no β-redexes left, the term is in normal form.
The substitution view
(λx. t) u → t[x := u]
That sentence has two very different edge cases. They are the paper’s starting point.
Work that gets discarded
If t contains zero occurrences of x, the argument u disappears. Any reduction already performed inside u was unnecessary.
Work that gets duplicated
If x occurs more than once, naive substitution duplicates u. If u contains redexes, the same necessary work can be repeated in every copy.
1.2 The four familiar fragments of the λ-calculus
The paper frames the issue using a simple grid of variable-use restrictions. A bound variable is a variable occurrence owned by a surrounding λ-abstraction; for example, the x in λx.x is bound. Start at the linear calculus, where every bound variable appears exactly once. Add the ability to omit a variable, repeat it, or both.
λA — affine
It appears once, or not at all. Erasure is allowed.
λI — relevant
It appears at least once. Sharing is allowed.
λK — full
Any number of appearances. Both erasure and sharing are allowed.
The paper names ΔL, ΔA, ΔI, and ΔK as corresponding Δ-Net subsystems.
1.3 Why choosing a clever order is not enough
A reduction order says which redex to simplify next. For erasure, normal order—try the outermost application before simplifying its argument—can avoid reducing an argument before discovering that a function will discard it. Sharing is the harder case: the paper follows Lévy’s observation that some terms with sharing have no ordinary sequential reduction order that avoids every duplicated reduction.
↯
The design target
Represent sharing directly as graph structure. A shared subgraph can then be reduced once and its result can serve every use.
02 Model shift
Stop treating a program as a tree.
The paper moves from a sequential substitution machine to an interaction system: a graph whose tiny local rewrites can happen independently. First, it helps to know exactly what “local” and “independent” mean here.
2.1 Graphs make sharing visible
A syntax tree represents every occurrence independently. A graph can let several uses point to one shared subgraph—a connected piece of the larger graph. That is the essential move: compute the shared subgraph once, then reuse its result.
2.2 Interaction systems, in one minute
An interaction system has agents and interaction rules. An agent is a small graph node with connection points called ports. It has one special principal port, used to trigger an interaction, and zero or more auxiliary ports, used to connect the rest of the graph.
When two agents connect specifically at their principal ports, they form an active pair. Interaction rules rewrite this pattern by reconnecting its immediately attached wires. The pair and those attached wires provide all the information the rule uses.
01
Find an active pair
Only a principal-to-principal connection is eligible. This makes each local decision sharply bounded.
02
Apply its local rule
The pair either disappears or travels through one another, reconnecting only their nearby wires. This single application is one interaction step.
03
Do independent work together
Each agent has one principal port, so two distinct active pairs share no agent. They can interact simultaneously and choose their local rules independently.
2.3 “Perfect confluence” is the parallelism enabler
Confluence asks whether different valid choices of reduction can lead to incompatible answers. The one-step diamond property is a very strong answer: if a net N has two possible single interaction steps, then performing either choice produces a net that can reach the same next state after exactly one more interaction.
The paper names this property perfect confluence. Each active pair uses the sole principal port of each of its two agents, so distinct active pairs use distinct agents. Their independent rewrites commute: doing the left pair first or the right pair first gives the same nearby wiring.
◇
Agreement and termination are separate questions
The diamond property guarantees agreement between competing local steps. Termination is a separate property: some nets can reduce forever. The paper’s claim is that, when a core interaction order normalizes, every normalizing order reaches the same result in the same number of interactions.
2.4 What earlier optimal-reduction nets struggled with
Previous interaction-net approaches tracked sharing scopes: the regions of a net governed by a particular duplication context, analogous to how a λ-abstraction governs its bound-variable occurrences. They used indexed fans plus delimiter agents such as brackets and croissants to mark those regions. The paper’s critique is practical as much as theoretical: delimiters can accumulate and their interactions can dominate the useful fan interactions. Some approaches also allow indices to grow without bound.
!
The proposed simplification
Δ-Nets uses one variable-arity agent—the replicator—to store a level and per-port level deltas. This concentrates the bookkeeping for a sharing context in one structure.
03 Core vocabulary
Three agents carry the whole core.
A Δ-Net is built from a fan, an eraser, and a replicator. Think of an agent as a tiny component: its principal port is the socket that can start a rewrite, while its auxiliary ports carry the surrounding context through that rewrite.
Fan
Has exactly two auxiliary ports. Fans represent the application and abstraction structure of a λ-term; fan annihilation expresses β-reduction.
Eraser
Has no auxiliary ports. It carries the fact that a bound variable is unused, and erases an agent it encounters in a distinct-agent interaction.
Replicator
Has any natural-number arity, meaning any count of auxiliary ports: 1, 2, 3, and so on. It connects the uses of one shared variable, and records the sharing context with a level plus a delta for each auxiliary port.
Level delta
Each replicator carries an integer level that identifies its sharing context. Each auxiliary port carries an integer delta. A replica leaving through a port adds that port’s delta to its current level.
3.1 Four systems fall out of the same pieces
| System | Agents permitted | Corresponding term fragment |
|---|---|---|
| ΔL | Fan | Linear: exactly one use. |
| ΔA | Fan + eraser | Affine: a use may be absent. |
| ΔI | Fan + replicator | Relevant: a use may repeat. |
| ΔK | Fan + eraser + replicator | Full: absence and repetition are both allowed. |
Here linear means exactly one bound use, affine means at most one, relevant means at least one, and full allows any count. This decomposition mirrors the paper’s opening taxonomy. It reveals which machinery pays for which feature: fans for structure, erasers for omission, replicators for sharing.
3.2 Equality is deliberately local in practice
Formally, equal replicators must match in level, arity, and all level deltas. The paper states that for well-formed nets produced by its λ-term translation, active replicators with the same level are guaranteed to be equal; an implementation can therefore compare only their levels in that setting.
What does “fan-in” versus “fan-out” mean here?
First, parent and child are just direction labels on a wire: in a rooted net, a parent points toward the root and a child points away from it. Canonical nets begin with replicators whose auxiliary ports are parents and whose principal port is a child: the paper calls these unpaired fan-ins. Reduction can also create fan-outs, with the orientation reversed. A fan-out is paired upstream with at least one fan-in, while a fan-in need not have a partner. The level-delta system is used to reason about that pairing locally.
04 Local dynamics
When two principal ports touch, one of three things happens.
The interaction rules are the engine of the model. This chapter groups their wire reconnections into three families: cancellation, deletion, and passage-with-copying. Each name describes the local change to an active pair.
1. Annihilation
Equal agents cancel. For fans, this is the interaction that corresponds to applying a λ-abstraction to an argument.
2. Erasure
An eraser is distinct from its neighbour and has zero auxiliary ports, so the agent it meets has no route to continue through: it is erased.
3. Commutation
Distinct non-eraser agents pass through each other. The number of outgoing copies depends on the other agent’s auxiliary ports.
4.1 Fan meets fan: the familiar redex disappears
Applications and abstractions are both represented by fans, distinguishable from the direction of their connections when viewed from the root (the distinguished top-level entry point of the whole net). When the appropriate fans form an active pair, they annihilate: both fan nodes are removed and their remaining wires are reconnected. This is the net-level form of β-reduction.
4.2 Replicator meets fan: structure splits around sharing
When a replicator meets a fan, it travels out through the fan’s two auxiliary ports, producing two exact replicator copies. At the same time, the fan travels through every auxiliary port of the replicator, producing one fan per port. Both structures preserve their roles, but now occupy the other’s surrounding context.
Read the result in two counts. R has three auxiliary ports, so three fans F₀, F₁, F₂ appear. F has two auxiliary ports, so two replicators Rₗ, Rᵣ appear. The six wires in the right-hand panel connect the two kinds of copies through their individual ports; none begins or ends in the middle of an edge.
4.3 Replicator meets replicator: levels decide the replicas
When two distinct replicators meet, name the lower-level one R and the higher-level one H. R makes one replica of H for each of R’s auxiliary ports; H makes exact duplicates of R for each of H’s ports. Each H replica takes the delta from its exit port on R and adds it to H’s current level.
The right-hand panel is a small version of the paper’s general rule. Three R ports create the three H replicas across the top; two H ports create the two R replicas below. The wires form a complete 3-by-2 connection pattern: each H replica reaches both R copies, and each R copy receives one port from every H replica.
+
The operational rule
Every port supplies one integer. When an H replica leaves through that port, add the integer to H’s current level. The port’s delta therefore records the level change associated with taking that particular exit.
A worked example
Suppose R has level 2 and two auxiliary ports. The first connects to a wire endpoint at level 2, so its delta is 2 − 2 = 0. The second connects to an endpoint at level 5, so its delta is 5 − 2 = +3. Now let a higher-level replicator H, with level 7, meet R.
Write the local differences
R’s own level is 2. Each port stores how its endpoint differs from that 2.
port A: 2 − 2 = 0port B: 5 − 2 = +3
Copy H once per R port
H is the higher-level replicator, so R replicates it. Both replicas start from H’s old level: 7.
old level of H = 7Add the exit’s delta
The copy leaving port A stays at 7. The copy leaving port B is shifted upward by 3.
A: 7 + 0 = 7B: 7 + 3 = 10
The general rule, after the example
new level of an H replica = old H level + delta on the R port it leaves through
“Duplicate” means exact copies. “Replicate” is the paper’s more precise word for copies that can differ by level. This distinction is doing real work: it replaces the separate indexed delimiters of older systems. A delta may be negative, zero, or positive; this example uses zero and a positive delta only because they make the arithmetic easy to see.
How a delta carries context through an interaction
Several higher-level replicators can reach the same R port with different current levels. The port contributes the same local adjustment to each one. For a port with delta +3, an arriving level 7 becomes 10, while an arriving level 12 becomes 15.
You can read the pair as an instruction: the replicator level gives the current context, and the chosen port adds the context change for that exit. Chapter 5 shows how the translation writes these port deltas into the initial net.
05 Translation
Compile a λ-term into one rooted net.
The paper defines, for each of λL, λA, λI, and λK, a bijection φ from terms to canonical Δ-Nets. A bijection is a one-to-one, reversible correspondence: every term has one canonical net, and that canonical net reads back as one term. The translation is inductive: translate the smaller subterms first, then connect their fragments to translate the larger term.
5.1 Start with a uniform interface
Every fragment has an interface: one incoming wire at the top and zero or more outgoing wires at the bottom. The outermost fragment is connected to a single root node; free variables—variable occurrences not owned by any surrounding λ—are represented by named interface nodes. This stable shape makes it possible to plug a fragment inside the fragment for its parent term.
5.2 The variable cases
A named boundary node
A variable free in the outermost term becomes a single-port, non-agent node labelled with that variable’s name. It is part of the net’s interface.
Just a wire—until it meets sharing
A bound variable occurrence is a vertical wire. Its lower endpoint connects to the appropriate auxiliary port of the replicator that shares the variable, when one is required.
5.3 The abstraction cases
An abstraction is an upward-pointing fan (the λ label in the paper is visual only). One auxiliary port connects to the body; the other corresponds to the bound variable. If that variable is unused, the second port goes to an eraser—only in the erasure-capable ΔA and ΔK systems.
When a used variable has multiple occurrences, a replicator connects the abstraction’s variable port to those occurrences. A one-port replicator with zero delta is equivalent to a wire, so canonical construction omits it.
5.4 The application case
An application is a downward-pointing fan (again, the @ label is only visual). Its principal port joins the function fragment and one auxiliary port joins the argument fragment. During reduction, the application fan eventually meets an abstraction fan; their annihilation expresses application.
5.5 Where levels come from
Tie every word here to the source syntax. An abstraction is the literal λ-term λx.M: x is its bound parameter and M is its body. An application is the literal λ-term M N: M is the function position and N is the argument position. A bound occurrence of x is one of the x leaves in M owned by that particular λx.
@
“Context” here is not a runtime closure
Calculate levels by walking through the written λ-term. Start the whole term at level 0. For an abstraction λx.M at level ℓ, continue into M at level ℓ. For every application M N at level ℓ, write level ℓ on its function M and level ℓ + 1 on its argument N. Repeat the same rule inside each subtree. During graph reduction, these coordinates track the corresponding sharing contexts; they do not count captured values or surrounding λ symbols.
| λ-calculus syntax | Given | Assign |
|---|---|---|
| Whole term T | T is the root program. | level(T) = 0 |
| Abstraction λx.M | level(λx.M) = l | level(M) = l; the replicator Rx belongs to level l + 1. |
| Application M N | level(M N) = l | level(M) = l; level(N) = l + 1. |
| Occurrence x | x is reached at level li. | Its wire endpoint has level li. |
Apply exactly the same instructions at every step. For λx.λy.x, start at level 0 and carry 0 through both abstraction bodies, so x receives level 0. For λx.f (g x), carry 0 into the body, assign 0 to the outer function f, and assign 1 to its argument g x. Repeating the application rule there assigns 1 to g and 2 to x.
To calculate an encoding by hand:
- Fully parenthesize the applications so every function and argument position is unambiguous.
- Write level 0 on the whole term, then walk inward. Keep the current level through every λx.M body and every function position; add one only when entering an application’s argument.
- For each binder λx at level l, put its sharing replicator Rx at level l + 1, when a replicator is required.
- Connect each bound occurrence xi to one auxiliary port of Rx. If that occurrence was reached at level li, label its port with di = li − (l + 1).
A wire endpoint level is therefore just the level calculated for that concrete variable occurrence. Its port delta is the difference between where the occurrence sits and where its binder’s replicator sits:
Construction rule
port delta = level of its connected wire endpoint − level of the replicator
This is where the numbers in the Chapter 4 example came from: a replicator at level 2 connected to an occurrence endpoint at level 5 receives delta +3. During reduction, the stored +3 supplies the local level adjustment whenever another replicator exits through that port. Section 5.8 carries out the complete calculation for four occurrences of one bound variable.
5.6 Follow a β-redex from term, to net, to term
The translation rules become much less abstract when the same small program remains visible throughout. Start with the closed linear term (λx.x)(λy.y). Each bound variable occurs exactly once, so this is a ΔL example: its net contains fans only—no eraser and no replicator.
λ-calculus view
(λx.x)(λy.y) →β λy.y
ordinary wire
active principal-port connection
wire exposed after annihilation
5.7 The δ in λx.x x is where Δ-Net levels enter
The Katharos diagram for λx.x x is especially useful because it makes the extra structure visible: the γ nodes carry λ/application shape and the δ node splits the one bound input x into two occurrences. That image uses symmetric interaction combinators, not Δ-Net notation verbatim. The correspondence below is conceptual: each γ role becomes a Δ-Net fan; the binary δ role becomes a two-port Δ-Net replicator R.
The same sharing is exercised by a redex
(λx.x x)(λy.y) →β (λy.y)(λy.y) →β λy.y
Crucially, a level delta is not another copy count and it is not a source-level variable value. The two-port replicator already says “one bound value has two consumers.” Its level and per-port deltas record the relative sharing context at each consumer. When replicators later commute through structure, those deltas adjust the levels of the replicas that leave through their ports. That is the bookkeeping which lets Δ-Nets represent the sharing introduced by δ without separate scope-delimiter agents.
5.8 Let right nesting expose a deeper delta vector
The previous term has only one application, so its two use sites differ by one level. A more revealing closed term is λx. x (x (x x)). The parentheses matter: each successive occurrence on the right sits inside the argument of another application, and every argument edge adds one to the term level.
Source-level effect
(λx. x (x (x x))) N →β N (N (N N))
| Occurrence | Position in the term | Endpoint level | Stored delta |
|---|---|---|---|
| x₀ | Function of the outer application. | 0 | 0 − 1 = −1 |
| x₁ | Function inside the first argument. | 1 | 1 − 1 = 0 |
| x₂ | Function inside the second argument. | 2 | 2 − 1 = +1 |
| x₃ | Argument of the deepest application. | 3 | 3 − 1 = +2 |
If this abstraction is applied to a term N, the replicator represents the four consumers of that one argument. When later interactions move sharing through the nested application structure, an exit through the four ports adjusts an arriving replica’s level by −1, 0, +1, or +2, respectively. The numbers preserve where each use belongs; they still do not say how many copies to make.
06 Beyond core interaction
Reduction needs housekeeping and a schedule.
The full algorithm combines the interaction-net core with canonicalization rules—cleanup rewrites that restore the special term-like net shape—and a global leftmost-outermost discipline for nonlinear systems.
6.1 Canonical and proper are different states
The translation produces a canonical net: one in the standard shape that the reverse translation knows how to read. After zero or more core interactions, the result is a proper net: a reachable intermediate net in the broader shape used during reduction. Canonicalization rewrites return that intermediate structure to the standard canonical form.
| State | Meaning in the paper | Why a reader should care |
|---|---|---|
| Canonical | Directly produced by the φ translation and in the special normal shape the back-translation expects. | It is the stable, term-like representation. |
| Proper | Reachable from a canonical net by zero or more Δ interactions. | It is the broader space where reduction does its work. |
6.2 Erasure needs a root-reachability sweep
In ΔA and ΔK, an eraser can leave disconnected subnets (smaller graph regions) behind. The paper’s canonicalization erasure step collects this unreachable graph material in one reachability sweep:
A
Mark from the root
Traverse parent–child wires that are reachable from the root and mark the nodes encountered.
B
Discard what was not marked
Erase all unreachable nodes. Wires formerly connected to them connect to erasers instead.
C
Choose the space/time trade-off
This sweep can run at the end or earlier to save space. The paper recommends after every application of an abstraction that ignores its argument when minimizing memory is the priority.
6.3 Sharing needs replicator cleanup
In ΔI and ΔK, interactions can form trees made only of replicators. The merge rule applies to consecutive replicators whose unpaired status can be established from a local level condition. This preserves pairing information while compressing the tree.
Δ
The local merge test
For consecutive replicators A and B connected through a port whose delta is d, B can be known unpaired when 0 ≤ lB − lA ≤ d. The paper argues this means B cannot interact before A is annihilated; as A is unpaired, it never will be.
ΔK has one more cleanup: unpaired replicator decay. Auxiliary ports of unpaired replicators that lead to erasers can be removed. If that leaves one zero-delta port, the replicator becomes the wire it is equivalent to.
6.4 Why the algorithm specifies leftmost-outermost
Core interaction rules enjoy the local confluence property. Canonicalization rules can involve ports beyond a principal-to-principal pair, so they operate under an additional scheduling discipline. Leftmost-outermost first selects an outermost reducible pattern—one with no enclosing reducible pattern—then chooses the leftmost candidate in the term-like reading of the net. Here “sequential” means this priority rule chooses one next interaction. The paper uses that order for ΔA, ΔI, and ΔK so that cleanup happens early and merge opportunities are handled before later interactions.
07 Synthesis
What does this proposal actually promise?
The paper’s final claim is an algorithm for optimal parallel λ-reduction: translate a term to a canonical net, reduce with the core rules plus required canonicalizations and scheduling, then read a canonical net back as a term.
Erasure is controlled
Leftmost-outermost reduction avoids evaluating a subnet that will later be erased; the reachability sweep removes the leftover garbage.
Sharing stays interior
Replicators represent shared use directly, aiming to avoid duplicating necessary reductions merely because an expression has several consumers.
Independent pairs can run
The interaction core’s perfect confluence lets disjoint active pairs choose and apply their local rules independently.
7.1 The guarantee differs by subsystem
In ΔL, fan annihilation is the only interaction. The paper states that all proper nets are canonical, and that if n β-reductions normalize a λL term, n interactions normalize its ΔL encoding in any order. ΔA, ΔI, and ΔK add canonicalization rules for erasure and sharing structures.
| System | Extra concern | Paper’s prescribed response |
|---|---|---|
| ΔL | None beyond fan annihilation. | Any interaction order; perfect confluence. |
| ΔA | Discarded subnet garbage. | Leftmost-outermost annihilations + erasure canonicalization. |
| ΔI | Replicator trees and early copies. | Leftmost-outermost + unpaired merging / canonicalization. |
| ΔK | Both garbage and sharing context. | Leftmost-outermost + erasure, merge, and decay canonicalizations. |
7.2 A useful way to separate the claims
- Expressiveness: every term in the four λ fragments has a canonical net representation, with a stated bijection.
- Local behavior: the three-agent interaction core is an interaction system with the one-step diamond property.
- Whole-algorithm behavior: adding canonicalization and the global reduction discipline is claimed to give Church–Rosser confluence and optimality for the nonlinear systems. Church–Rosser confluence is the standard name for the broader agreement property: reduction paths that start from the same object can be continued to a common result.
This distinction matters. The third layer relies on erasure sweeps, replicator merging, decay, and leftmost-outermost scheduling in addition to the core interaction rules.
7.3 The broader proposition
The paper asks readers to see λ-calculus as a projection of Δ-Nets: λ-terms enforce a particular, restrictive form of sharing, while nets can express sharing relationships that syntax alone obscures. If the proposed reduction machinery holds up, that added freedom could matter for parallel language runtimes and machine architectures.
✓
One-sentence takeaway
Δ-Nets tries to make optimal parallel evaluation practical by packing each sharing boundary’s information into a variable-arity replicator, then combining local interactions with only the global discipline needed to avoid preventable work.
08 Keep nearby
A compact glossary, then the source.
Use these short definitions while reading the formal article. They are intentionally intuitive, and defer to the paper for exact notation and proofs.
λ-term
A program made from variables, abstractions, and applications. In λx.t, the abstraction binds parameter x in body t. In t u, t is the function and u is its argument.
β-redex / β-reduction
A β-redex is a function already applied to an argument, (λx.t)u. Its β-reduction substitutes u for the bound occurrences of x in t.
Normal form / normalizing
Normal form means no reducible pattern remains. A term or net is normalizing if some reduction sequence eventually reaches normal form; it need not do so in every system or every sequence.
Interaction system
A graph-rewriting system made of agent types and rules that apply only when two agents meet at their principal ports.
Agent / port
An agent is one small node in a net. Ports are its connection sockets. Each agent has one principal port and zero or more auxiliary ports.
Active pair
Two agents connected through their principal ports; exactly the local configuration that an interaction rule rewrites.
One-step diamond
If two different single interactions can begin at the same net, the results can meet after one more interaction each. Every edge of the “diamond” is exactly one step.
Perfect confluence
The paper’s name for the one-step diamond property of its interaction-system core. It means competing local steps agree immediately.
Church–Rosser confluence
The broader common-result property for reduction paths. It says divergent valid reductions can be joined again, not necessarily in one step.
Canonical Δ-Net
A net produced by the term-to-net translation, in the special representation expected by the translation back to a λ-term.
Canonicalization
A cleanup rewrite used to return a proper intermediate net to canonical, term-like form. It is not itself a core principal-port interaction.
Commutation
An interaction of distinct, non-eraser agents. Each travels through the other and may be copied according to the other’s arity.
Fan
The two-auxiliary-port structural agent. In a rooted net it can encode either application or abstraction, and fan annihilation expresses β-reduction.
Level / delta
In a canonical λ encoding, entering the argument of an application adds one level; entering its function or an abstraction body does not. A replicator port’s delta is its bound-variable occurrence level minus the replicator level.
Proper Δ-Net
Any net reachable from a canonical net through zero or more core Δ interactions; it can contain noncanonical intermediate shapes.
Replicator
The variable-arity agent used for sharing. It has a level and an integer delta associated with each auxiliary port.
Sharing scope
The region controlled by one duplication context. Older interaction-net approaches often marked scope boundaries with separate delimiter agents.
Leftmost-outermost
A priority order: choose a reducible pattern not nested inside another, then choose the leftmost such pattern in the term-like reading of the net.
Primary source
Daniel Augusto Rizzi Salvadori, “Δ-Nets: Interaction-Based System for Optimal Parallel λ-Reduction,” arXiv:2505.20314v4, 22 July 2026.
About this edition. It is an independently structured teaching summary based on the paper’s abstract and Sections 1–5. All diagrams and wording here are original explanatory material, not reproductions of the author’s figures.