Sharing Equality is Linear

Andrea Condoluci; Beniamino Accattoli; Claudio Sacerdoti Coen

arxiv: 1907.06101 · v1 · pith:SGP4HJRGnew · submitted 2019-07-13 · 💻 cs.LO

Sharing Equality is Linear

Andrea Condoluci , Beniamino Accattoli , Claudio Sacerdoti Coen This is my paper

Pith reviewed 2026-05-24 21:44 UTC · model grok-4.3

classification 💻 cs.LO

keywords lambda calculussharing equalitylinear timeDAG representationbisimulationalpha conversion

0 comments

The pith

Sharing equality of λ-terms with sharing can be decided in linear time.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a linear-time algorithm for deciding whether two shared representations denote α-convertible λ-terms. Earlier work achieved only polynomial time in the size of the shared terms. The approach represents the shared terms as directed acyclic graphs and reduces the equality question to checking bisimilarity on those graphs. If the reduction is correct, equality testing becomes feasible at the scale of the shared structure rather than the exponentially larger unshared terms.

Core claim

The paper shows that sharing equality reduces to DAG bisimulation in such a way that the decision procedure runs in time linear in the size of the input DAGs, yielding the first linear-time algorithm for the problem.

What carries the argument

Representation of shared λ-terms as directed acyclic graphs together with reduction of sharing equality to bisimulation on those graphs.

If this is right

Equality tests inside evaluators and proof checkers that use sharing become linear rather than polynomial in the size of the shared objects.
The cost of comparing two terms no longer grows with the size of their fully expanded unshared forms.
Implementations can safely use more aggressive sharing without paying an extra asymptotic price for equality checks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same linear bound may extend to other operations that traverse shared structure, such as substitution or reduction steps that respect sharing.
If the linear algorithm composes cleanly with existing sharing-based evaluators, the overall complexity of normalization in proof assistants could drop in practice.
The technique supplies a concrete target for verifying the correctness of equality primitives in systems that already rely on DAG representations.

Load-bearing premise

The reduction of sharing equality to DAG bisimulation preserves exact correspondence with α-conversion of the underlying unshared terms and incurs no hidden logarithmic or polynomial overhead.

What would settle it

An input pair of shared terms on which the algorithm either outputs the wrong answer relative to unshared α-conversion or requires superlinear time in the size of the shared representations.

Figures

Figures reproduced from arXiv: 1907.06101 by Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen.

**Figure 1.** Figure 1: a) λ-term as a λ-tree, without sharing; b) λ-graph with sharing (same term of a); c) λ-graph breaking domination. terms in the technical parts, since much more elegant and short proofs can be obtained by avoiding to reason explicitly on bound names and α-equivalence. Terms as graphs, informally. Graphically, λ-terms can be seen as syntax trees—please have a look at the example in [PITH_FULL_IMAGE:figures/… view at source ↗

**Figure 2.** Figure 2: Examples of sharing equivalences and queries. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 3.** Figure 3: Sharing equivalence rules on a λ-graph of equivalence between nodes (sharing equivalence, eorem 4.2) whose intended meaning is that two related nodes have the same readback. is notion shall rest on various requirements; the rst one is that only homogeneous nodes can be related: Definition 4.1 (Homogeneous nodes [27]). Let n,m be nodes of a λ-graph G. We say that n and m are homogeneous if they are both … view at source ↗

**Figure 3.** Figure 3: Notation A.3. We denote by B a generic bisimulation. A.2 Propagation ⇓ Definition A.4 (Propagated Relation). We call propagated a relation that is closed under the rules of [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗

read the original abstract

The $\lambda$-calculus is a handy formalism to specify the evaluation of higher-order programs. It is not very handy, however, when one interprets the specification as an execution mechanism, because terms can grow exponentially with the number of $\beta$-steps. This is why implementations of functional languages and proof assistants always rely on some form of sharing of subterms. These frameworks however do not only evaluate $\lambda$-terms, they also have to compare them for equality. In presence of sharing, one is actually interested in the equality---or more precisely $\alpha$-conversion---of the underlying unshared $\lambda$-terms. The literature contains algorithms for such a sharing equality, that are polynomial in the sizes of the shared terms. This paper improves the bounds in the literature by presenting the first linear time algorithm. As others before us, we are inspired by Paterson and Wegman's algorithm for first-order unification, itself based on representing terms with sharing as DAGs, and sharing equality as bisimulation of DAGs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper claims the first linear-time algorithm for alpha-equality under sharing by reducing it to DAG bisimulation, but the abstract gives no details on binder handling or the linearity proof.

read the letter

The core claim here is a linear-time algorithm for sharing equality, meaning alpha-conversion of the unshared lambda-terms when the representation uses sharing to keep size small. It improves on prior polynomial-time methods by adapting Paterson-Wegman DAG bisimulation to lambda-DAGs. That is the actual new piece: the asymptotic bound, presented as the first such result. The paper does a reasonable job framing the practical setting, where functional implementations and proof assistants need to compare terms without expanding shared subterms, and it correctly points to the exponential blowup problem that sharing solves. The citation pattern to earlier polynomial algorithms is straightforward and shows the authors know the baseline. The soft spot is exactly the one the stress-test flags. The abstract says nothing about how binders and variable nodes are encoded in the DAG or what the bisimulation rules look like for alpha-renaming. Without those, it is impossible to check whether the reduction is sound and complete for unshared lambda-terms or whether the claimed O(n) bound survives the representation details. If the full paper supplies explicit rules, a complexity argument without hidden logarithmic factors, and a proof that bisimilarity matches alpha-equivalence, the concern disappears; otherwise the central claim rests on an unshown adaptation. This is the kind of paper that belongs in a reading group focused on term representations and implementation algorithms. Readers working on efficient equality checks inside proof assistants or compilers would get direct value from the bound improvement. It deserves a serious referee because the problem is well-motivated, the approach is grounded in existing work, and the claimed result is falsifiable once the details are written out.

Referee Report

1 major / 0 minor

Summary. The paper claims to present the first linear-time algorithm for sharing equality (α-equivalence of the underlying unshared λ-terms) by modeling shared terms as DAGs and reducing the problem to DAG bisimulation via an adaptation of the Paterson-Wegman first-order unification algorithm.

Significance. If the central claim holds, the result would improve upon the existing polynomial-time algorithms in the literature for equality checking under sharing, which is relevant for implementations of functional languages and proof assistants that rely on shared representations to avoid exponential term growth.

major comments (1)

[Abstract] Abstract: the claim that a linear-time algorithm exists is stated, but the text supplies no proof sketch, complexity analysis, pseudocode, or description of the bisimulation rules for binders; this prevents verification that the reduction correctly captures α-conversion of unshared λ-terms and that the O(n) bound holds without hidden logarithmic or polynomial factors from the representation or hash tables.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the comments. We address the major comment below.

read point-by-point responses

Referee: [Abstract] Abstract: the claim that a linear-time algorithm exists is stated, but the text supplies no proof sketch, complexity analysis, pseudocode, or description of the bisimulation rules for binders; this prevents verification that the reduction correctly captures α-conversion of unshared λ-terms and that the O(n) bound holds without hidden logarithmic or polynomial factors from the representation or hash tables.

Authors: Abstracts are concise summaries by design and do not contain proof sketches, pseudocode or detailed analyses; the full manuscript supplies these. The body adapts the Paterson-Wegman algorithm to DAG bisimulation, with explicit rules for binders that correctly reduce sharing equality to α-equivalence of the underlying unshared terms. The algorithm is given in pseudocode, the representation is standard pointer-based DAGs without hash tables, and the complexity section proves an O(n) bound with no hidden logarithmic or polynomial factors. revision: no

Circularity Check

0 steps flagged

No significant circularity; adaptation of external algorithm

full rationale

The paper adapts the Paterson-Wegman DAG bisimulation algorithm (an external, prior result) to λ-DAGs for α-equality under sharing. The abstract explicitly positions the contribution as an improvement on existing polynomial bounds via this inspiration, with no self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations that reduce the linear-time claim to the paper's own inputs. The derivation chain remains self-contained against the cited external benchmark.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the correctness of the DAG-bisimulation reduction and on the linear-time complexity of the adapted Paterson-Wegman procedure; these are treated as background assumptions rather than derived inside the paper.

axioms (2)

domain assumption Sharing equality of λ-terms is equivalent to bisimulation of their DAG representations.
Invoked when the abstract equates the two problems.
domain assumption Paterson and Wegman's unification algorithm decides DAG bisimulation in linear time.
The paper states it is inspired by this algorithm and claims the same complexity.

pith-pipeline@v0.9.0 · 5703 in / 1178 out tokens · 22912 ms · 2026-05-24T21:44:49.392433+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

[1]

Beniamino Acca/t_toli. 2018. Proof Nets and the Linear Substitution Calculus. In /T_heoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings. 37–61. h/t_tps://doi. org/10.1007/978-3-030-02508-3 3

work page doi:10.1007/978-3-030-02508-3 2018
[2]

Beniamino Acca/t_toli and Bruno Barras. 2017. Environments and the complexity of abstract machines. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017. 4–16. h/t_tps://doi.org/10.1145/3131851.3131855

work page doi:10.1145/3131851.3131855 2017
[3]

Beniamino Acca/t_toli and Claudio Sacerdoti Coen. 2015. On the Relative Use- fulness of Fireballs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015 . 141–155. h/t_tps://doi.org/10. 1109/LICS.2015.23

work page 2015
[4]

Beniamino Acca/t_toli and Giulio Guerrieri. 2017. Implementing Open Call-by- Value. In Fundamentals of So/f_tware Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers. 1–19. h/t_tps: //doi.org/10.1007/978-3-319-68972-2 1

work page doi:10.1007/978-3-319-68972-2 2017
[5]

Beniamino Acca/t_toli and Ugo Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA’12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan. 22–37. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2012.22

work page doi:10.4230/lipics.rta.2012.22 2012
[6]

Beniamino Acca/t_toli and Ugo Dal Lago. 2014. Beta reduction is invariant, indeed. In Joint Meeting of the Twenty-/T_hird EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014 . 8:1–8:10. h/t_tps://doi.org/10.1145/2603088.2603105

work page doi:10.1145/2603088.2603105 2014
[7]

John Allen. 1978. Anatomy of LISP. McGraw-Hill, Inc., New York, NY, USA

work page 1978
[8]

Lauridsen, and Mikkel /T_horup

Stephen Alstrup, Dov Harel, Peter W. Lauridsen, and Mikkel /T_horup. 1999. Dominators in Linear Time. SIAM J. Comput. 28, 6 (1999), 2117–2132. h/t_tps: //doi.org/10.1137/S0097539797317263

work page doi:10.1137/s0097539797317263 1999
[9]

Ariola and Jan Willem Klop

Zena M. Ariola and Jan Willem Klop. 1996. Equational Term Graph Rewriting. Fundam. Inform. 26, 3/4 (1996), 207–240. h/t_tps://doi.org/10.3233/FI-1996-263401

work page doi:10.3233/fi-1996-263401 1996
[10]

Blelloch and John Greiner

Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. 226–237. h/t_tps://doi.org/10.1145/224164.224210

work page doi:10.1145/224164.224210 1995
[11]

Stefanus Cornelis Christoﬀel Blom. 2001. Term Graph Rewriting. Syntax and semantics. Ph.D. Dissertation. Vrije Universiteit Amsterdam

work page 2001
[12]

Robert S Boyer and Jay S Moore. 1972. /T_he sharing of structure in theorem- proving programs. Machine intelligence 7 (1972), 101–116

work page 1972
[13]

Buchsbaum, Haim Kaplan, Anne Rogers, and Jeﬀery R

Adam L. Buchsbaum, Haim Kaplan, Anne Rogers, and Jeﬀery R. Westbrook. 1998. A New, Simpler Linear-Time Dominators Algorithm. ACM Trans. Program. Lang. Syst. 20, 6 (1998), 1265–1296. h/t_tps://doi.org/10.1145/295656.295663

work page doi:10.1145/295656.295663 1998
[14]

Christophe Calv`es. 2013. Unifying Nominal Uni/f_ication. In24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, /T_he Netherlands. 143–157. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2013. 143

work page doi:10.4230/lipics.rta.2013 2013
[15]

Christophe Calv`es and Maribel Fern´andez. 2010. /T_he First-Order Nominal Link. In Logic-Based Program Synthesis and Transformation - 20th International Sympo- sium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers. 234–248. h/t_tps://doi.org/10.1007/978-3-642-20551-4 15

work page doi:10.1007/978-3-642-20551-4 2010
[16]

Christophe Calv`es and Maribel Fern´andez. 2010. Matching and alpha-equivalence check for nominal terms. J. Comput. Syst. Sci. 76, 5 (2010), 283–301. h/t_tps: //doi.org/10.1016/j.jcss.2009.10.003

work page doi:10.1016/j.jcss.2009.10.003 2010
[17]

Arthur Chargu´eraud. 2012. /T_he Locally Nameless Representation. J. Autom. Reasoning 49, 3 (2012), 363–408. h/t_tps://doi.org/10.1007/s10817-011-9225-2

work page doi:10.1007/s10817-011-9225-2 2012
[18]

Andrei P. Ershov. 1958. On Programming of Arithmetic Operations. Commun. ACM 1, 8 (1958), 3–9. h/t_tps://doi.org/10.1145/368892.368907

work page doi:10.1145/368892.368907 1958
[19]

Harold N. Gabow. 1990. Data Structures for Weighted Matching and Nearest Common Ancestors with Linking. In Proceedings of the First Annual ACM-SIAM Symposium on Discrete Algorithms, 22-24 January 1990, San Francisco, California, USA. 434–443. h/t_tp://dl.acm.org/citation.cfm?id=320176.320229

work page arXiv 1990
[20]

1974.Monocopy and associative algorithms in extended Lisp

Eiichi Goto. 1974.Monocopy and associative algorithms in extended Lisp. Technical report TR 74–03. University of Tokyo

work page 1974
[21]

Clemens Grabmayer and Jan Rochel. 2014. Maximal sharing in the Lambda calculus with letrec. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. 67–80. h/t_tps://doi.org/10.1145/2628136.2628148

work page doi:10.1145/2628136.2628148 2014
[22]

Hopcro/f_t and R

J. Hopcro/f_t and R. Karp. 1971.A Linear Algorithm for Testing Equivalence of Finite Automata. Technical Report 0. Dept. of Computer Science, Cornell U

work page 1971
[23]

John Lamping. 1990. An Algorithm for Optimal Lambda Calculus Reduction. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990 . 16–30. h/t_tps://doi.org/10.1145/96709.96711

work page doi:10.1145/96709.96711 1990
[24]

Jordi Levy and Mateu Villaret. 2010. An Eﬃcient Nominal Uni/f_ication Algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Sco/t_tland, UK . 209–226. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2010.209

work page doi:10.4230/lipics.rta.2010.209 2010
[25]

Alberto Martelli and Ugo Montanari. 1977. /T_heorem Proving with Structure Sharing and Eﬃcient Uni/f_ication. InProceedings of the 5th International Joint Conference on Arti/f_icial Intelligence. Cambridge, MA, USA, August 22-25, 1977. 543. h/t_tp://ijcai.org/Proceedings/77-1/Papers/096.pdf

work page 1977
[26]

Alberto Martelli and Ugo Montanari. 1982. An Eﬃcient Uni/f_ication Algorithm. ACM Trans. Program. Lang. Syst. 4, 2 (1982), 258–282. h/t_tps://doi.org/10.1145/ 357162.357169

work page arXiv 1982
[27]

Paterson and M.N

M.S. Paterson and M.N. Wegman. 1978. Linear uni/f_ication.J. Comput. System Sci. 16, 2 (1978), 158 – 167. h/t_tps://doi.org/10.1016/0022-0000(78)90043-0

work page doi:10.1016/0022-0000(78)90043-0 1978
[28]

Zhenyu Qian. 1993. Linear Uni/f_ication of Higher-Order Pa/t_terns. In TAP- SOFT’93: /T_heory and Practice of So/f_tware Development, International Joint Con- ference CAAP/FASE, Orsay, France, April 13-17, 1993, Proceedings . 391–405. h/t_tps://doi.org/10.1007/3-540-56610-478

work page doi:10.1007/3-540-56610-478 1993
[29]

Laurent Regnier. 1992. Lambda-calcul et r´eseaux. PhD thesis. Univ. Paris VII

work page 1992
[30]

Manfred Schmidt-Schauß, Conrad Rau, and David Sabel. 2013. Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, /T_he Netherlands. 255–270. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2013.255

work page doi:10.4230/lipics.rta.2013.255 2013
[31]

Pi/t_ts, and Murdoch Gabbay

Christian Urban, Andrew M. Pi/t_ts, and Murdoch Gabbay. 2003. Nominal Uni/f_i- caiton. In Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G¨odel Colloquium, KGC 2003, Vi- enna, Austria, August 25-30, 2003, Proceedings. 513–527. h/t_tps://doi.org/10.1007/ 978-3-540-45220-1 41

work page 2003
[32]

Wadsworth

C.P. Wadsworth. 1971. Semantics and Pragmatics of the Lambda-calculus. Uni- versity of Oxford. h/t_tps://books.google.it/books?id=kl1QIQAACAAJ Conference’17, July 2017, Washington, DC, USA Condoluci, Acca/t_toli and Sacerdoti Coen A RELATIONS ON GRAPHS In this section we are going to introduce several kinds of binary relations on nodes of theλ-graph. Some...

work page 1971
[33]

Clearly m τ ′· m′ 1 and m τ ′· m′

work page
[34]

n τ m crosses p

□ Given a relation R, we de/f_ine its propagationR⇓ as the smallest propagated relation containing R: D/e.sc/f.sc/i.sc/n.sc/i.sc/t.sc/i.sc/o.sc/n.sc A.7 (P/r.sc/o.sc/p.sc/a.sc/g.sc/a.sc/t.sc/i.sc/o.sc/n.scR⇓). Let R be a binary relation over the nodes of aλ-graph G. /T_he propagationR⇓ of R is obtained by closing R under the rules of Figure 3. P/r.sc/o.sc...

work page 2017

[1] [1]

Beniamino Acca/t_toli. 2018. Proof Nets and the Linear Substitution Calculus. In /T_heoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings. 37–61. h/t_tps://doi. org/10.1007/978-3-030-02508-3 3

work page doi:10.1007/978-3-030-02508-3 2018

[2] [2]

Beniamino Acca/t_toli and Bruno Barras. 2017. Environments and the complexity of abstract machines. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017. 4–16. h/t_tps://doi.org/10.1145/3131851.3131855

work page doi:10.1145/3131851.3131855 2017

[3] [3]

Beniamino Acca/t_toli and Claudio Sacerdoti Coen. 2015. On the Relative Use- fulness of Fireballs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015 . 141–155. h/t_tps://doi.org/10. 1109/LICS.2015.23

work page 2015

[4] [4]

Beniamino Acca/t_toli and Giulio Guerrieri. 2017. Implementing Open Call-by- Value. In Fundamentals of So/f_tware Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers. 1–19. h/t_tps: //doi.org/10.1007/978-3-319-68972-2 1

work page doi:10.1007/978-3-319-68972-2 2017

[5] [5]

Beniamino Acca/t_toli and Ugo Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA’12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan. 22–37. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2012.22

work page doi:10.4230/lipics.rta.2012.22 2012

[6] [6]

Beniamino Acca/t_toli and Ugo Dal Lago. 2014. Beta reduction is invariant, indeed. In Joint Meeting of the Twenty-/T_hird EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014 . 8:1–8:10. h/t_tps://doi.org/10.1145/2603088.2603105

work page doi:10.1145/2603088.2603105 2014

[7] [7]

John Allen. 1978. Anatomy of LISP. McGraw-Hill, Inc., New York, NY, USA

work page 1978

[8] [8]

Lauridsen, and Mikkel /T_horup

Stephen Alstrup, Dov Harel, Peter W. Lauridsen, and Mikkel /T_horup. 1999. Dominators in Linear Time. SIAM J. Comput. 28, 6 (1999), 2117–2132. h/t_tps: //doi.org/10.1137/S0097539797317263

work page doi:10.1137/s0097539797317263 1999

[9] [9]

Ariola and Jan Willem Klop

Zena M. Ariola and Jan Willem Klop. 1996. Equational Term Graph Rewriting. Fundam. Inform. 26, 3/4 (1996), 207–240. h/t_tps://doi.org/10.3233/FI-1996-263401

work page doi:10.3233/fi-1996-263401 1996

[10] [10]

Blelloch and John Greiner

Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. 226–237. h/t_tps://doi.org/10.1145/224164.224210

work page doi:10.1145/224164.224210 1995

[11] [11]

Stefanus Cornelis Christoﬀel Blom. 2001. Term Graph Rewriting. Syntax and semantics. Ph.D. Dissertation. Vrije Universiteit Amsterdam

work page 2001

[12] [12]

Robert S Boyer and Jay S Moore. 1972. /T_he sharing of structure in theorem- proving programs. Machine intelligence 7 (1972), 101–116

work page 1972

[13] [13]

Buchsbaum, Haim Kaplan, Anne Rogers, and Jeﬀery R

Adam L. Buchsbaum, Haim Kaplan, Anne Rogers, and Jeﬀery R. Westbrook. 1998. A New, Simpler Linear-Time Dominators Algorithm. ACM Trans. Program. Lang. Syst. 20, 6 (1998), 1265–1296. h/t_tps://doi.org/10.1145/295656.295663

work page doi:10.1145/295656.295663 1998

[14] [14]

Christophe Calv`es. 2013. Unifying Nominal Uni/f_ication. In24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, /T_he Netherlands. 143–157. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2013. 143

work page doi:10.4230/lipics.rta.2013 2013

[15] [15]

Christophe Calv`es and Maribel Fern´andez. 2010. /T_he First-Order Nominal Link. In Logic-Based Program Synthesis and Transformation - 20th International Sympo- sium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers. 234–248. h/t_tps://doi.org/10.1007/978-3-642-20551-4 15

work page doi:10.1007/978-3-642-20551-4 2010

[16] [16]

Christophe Calv`es and Maribel Fern´andez. 2010. Matching and alpha-equivalence check for nominal terms. J. Comput. Syst. Sci. 76, 5 (2010), 283–301. h/t_tps: //doi.org/10.1016/j.jcss.2009.10.003

work page doi:10.1016/j.jcss.2009.10.003 2010

[17] [17]

Arthur Chargu´eraud. 2012. /T_he Locally Nameless Representation. J. Autom. Reasoning 49, 3 (2012), 363–408. h/t_tps://doi.org/10.1007/s10817-011-9225-2

work page doi:10.1007/s10817-011-9225-2 2012

[18] [18]

Andrei P. Ershov. 1958. On Programming of Arithmetic Operations. Commun. ACM 1, 8 (1958), 3–9. h/t_tps://doi.org/10.1145/368892.368907

work page doi:10.1145/368892.368907 1958

[19] [19]

Harold N. Gabow. 1990. Data Structures for Weighted Matching and Nearest Common Ancestors with Linking. In Proceedings of the First Annual ACM-SIAM Symposium on Discrete Algorithms, 22-24 January 1990, San Francisco, California, USA. 434–443. h/t_tp://dl.acm.org/citation.cfm?id=320176.320229

work page arXiv 1990

[20] [20]

1974.Monocopy and associative algorithms in extended Lisp

Eiichi Goto. 1974.Monocopy and associative algorithms in extended Lisp. Technical report TR 74–03. University of Tokyo

work page 1974

[21] [21]

Clemens Grabmayer and Jan Rochel. 2014. Maximal sharing in the Lambda calculus with letrec. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. 67–80. h/t_tps://doi.org/10.1145/2628136.2628148

work page doi:10.1145/2628136.2628148 2014

[22] [22]

Hopcro/f_t and R

J. Hopcro/f_t and R. Karp. 1971.A Linear Algorithm for Testing Equivalence of Finite Automata. Technical Report 0. Dept. of Computer Science, Cornell U

work page 1971

[23] [23]

John Lamping. 1990. An Algorithm for Optimal Lambda Calculus Reduction. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990 . 16–30. h/t_tps://doi.org/10.1145/96709.96711

work page doi:10.1145/96709.96711 1990

[24] [24]

Jordi Levy and Mateu Villaret. 2010. An Eﬃcient Nominal Uni/f_ication Algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Sco/t_tland, UK . 209–226. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2010.209

work page doi:10.4230/lipics.rta.2010.209 2010

[25] [25]

Alberto Martelli and Ugo Montanari. 1977. /T_heorem Proving with Structure Sharing and Eﬃcient Uni/f_ication. InProceedings of the 5th International Joint Conference on Arti/f_icial Intelligence. Cambridge, MA, USA, August 22-25, 1977. 543. h/t_tp://ijcai.org/Proceedings/77-1/Papers/096.pdf

work page 1977

[26] [26]

Alberto Martelli and Ugo Montanari. 1982. An Eﬃcient Uni/f_ication Algorithm. ACM Trans. Program. Lang. Syst. 4, 2 (1982), 258–282. h/t_tps://doi.org/10.1145/ 357162.357169

work page arXiv 1982

[27] [27]

Paterson and M.N

M.S. Paterson and M.N. Wegman. 1978. Linear uni/f_ication.J. Comput. System Sci. 16, 2 (1978), 158 – 167. h/t_tps://doi.org/10.1016/0022-0000(78)90043-0

work page doi:10.1016/0022-0000(78)90043-0 1978

[28] [28]

Zhenyu Qian. 1993. Linear Uni/f_ication of Higher-Order Pa/t_terns. In TAP- SOFT’93: /T_heory and Practice of So/f_tware Development, International Joint Con- ference CAAP/FASE, Orsay, France, April 13-17, 1993, Proceedings . 391–405. h/t_tps://doi.org/10.1007/3-540-56610-478

work page doi:10.1007/3-540-56610-478 1993

[29] [29]

Laurent Regnier. 1992. Lambda-calcul et r´eseaux. PhD thesis. Univ. Paris VII

work page 1992

[30] [30]

Manfred Schmidt-Schauß, Conrad Rau, and David Sabel. 2013. Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, /T_he Netherlands. 255–270. h/t_tps://doi.org/10.4230/LIPIcs.RTA.2013.255

work page doi:10.4230/lipics.rta.2013.255 2013

[31] [31]

Pi/t_ts, and Murdoch Gabbay

Christian Urban, Andrew M. Pi/t_ts, and Murdoch Gabbay. 2003. Nominal Uni/f_i- caiton. In Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G¨odel Colloquium, KGC 2003, Vi- enna, Austria, August 25-30, 2003, Proceedings. 513–527. h/t_tps://doi.org/10.1007/ 978-3-540-45220-1 41

work page 2003

[32] [32]

Wadsworth

C.P. Wadsworth. 1971. Semantics and Pragmatics of the Lambda-calculus. Uni- versity of Oxford. h/t_tps://books.google.it/books?id=kl1QIQAACAAJ Conference’17, July 2017, Washington, DC, USA Condoluci, Acca/t_toli and Sacerdoti Coen A RELATIONS ON GRAPHS In this section we are going to introduce several kinds of binary relations on nodes of theλ-graph. Some...

work page 1971

[33] [33]

Clearly m τ ′· m′ 1 and m τ ′· m′

work page

[34] [34]

n τ m crosses p

□ Given a relation R, we de/f_ine its propagationR⇓ as the smallest propagated relation containing R: D/e.sc/f.sc/i.sc/n.sc/i.sc/t.sc/i.sc/o.sc/n.sc A.7 (P/r.sc/o.sc/p.sc/a.sc/g.sc/a.sc/t.sc/i.sc/o.sc/n.scR⇓). Let R be a binary relation over the nodes of aλ-graph G. /T_he propagationR⇓ of R is obtained by closing R under the rules of Figure 3. P/r.sc/o.sc...

work page 2017