Term Graph Representations for Cyclic Lambda-Terms∗
Clemens Grabmayer

Jan Rochel

Department of Philosophy
Utrecht University
The Netherlands
clemens@phil.uu.nl

Department of Computing Sciences
Utrecht University
The Netherlands
jan@rochel.info

We study various representations for cyclic λ -terms as higher-order or as first-order term graphs.
We focus on the relation between ‘λ -higher-order term graphs’ (λ -ho-term-graphs), which are firstorder term graphs endowed with a well-behaved scope function, and their representations as ‘λ -termgraphs’, which are plain first-order term graphs with scope-delimiter vertices that meet certain scoping requirements. Specifically we tackle the question: Which class of first-order term graphs admits a
faithful embedding of λ -ho-term-graphs in the sense that (i) the homomorphism-based sharing-order
on λ -ho-term-graphs is preserved and reflected, and (ii) the image of the embedding corresponds
closely to a natural class (of λ -term-graphs) that is closed under homomorphism?
We systematically examine whether a number of classes of λ -term-graphs have this property, and
we find a particular class of λ -term-graphs that satisfies this criterion. Term graphs of this class are
built from application, abstraction, variable, and scope-delimiter vertices, and have the characteristic
feature that the latter two kinds of vertices have back-links to the corresponding abstraction.
This result puts a handle on the concept of subterm sharing for higher-order term graphs, both
theoretically and algorithmically: We obtain an easily implementable method for obtaining the maximally shared form of λ -ho-term-graphs. Furthermore, we open up the possibility to pull back properties from first-order term graphs to λ -ho-term-graphs, properties such as the complete lattice structure
of bisimulation equivalence classes with respect to the sharing order.

1

Introduction

Cyclic lambda-terms typically represent infinite λ -terms. In this paper we study term graph representations of cyclic λ -terms and their respective notions of homomorphism, or functional bisimulation.
The context in which the results presented in this paper play a central role is our research on subterm sharing as present in terms of languages such as the λ -calculus with letrec [8, 1], with recursive
definitions [2], or languages with µ-recursion [3], and our interest in describing maximal sharing in such
settings. Specifically we want to obtain concepts and methods as follows:
• an efficient test for term equivalence with respect to α-renaming and unfolding;
• a notion of ‘maximal subterm sharing’ for terms in the respective language;
• the efficient computation of the maximally shared form of a term;
• a sharing (pre-)order on unfolding-equivalent terms.
Now our approach is to split the work into a part that concerns properties specific to concrete languages,
and into a part that deals with aspects that are common to most of the languages with constructs for
expressing subterm sharing. To this end we set out to find classes of term graphs that facilitate faithful
interpretations of terms in such languages as (higher-order, and eventually first-order) term graphs, and
that are ‘well-behaved’ in the sense that maximally shared term graphs do always exist. In this way the
∗
This work was started, and in part carried out, within the framework of the project NWO project Realising Optimal Sharing
(ROS), project number 612.000.935, under the direction of Vincent von Oostrom and Doaitse Swierstra.

R. Echahed and D. Plump (Eds.): 7th International Workshop on
Computing with Terms and Graphs
EPTCS 110, 2013, pp. 56–73, doi:10.4204/EPTCS.110.7

© C. Grabmayer & J. Rochel
This work is licensed under the
Creative Commons Attribution License.

C. Grabmayer & J. Rochel

57

task can be divided into two parts: an investigation of sharing for term graphs with higher-order features
(the aim of this paper), and a study of language-specific aspects of sharing (the aim of a further paper).
Here we study a variety of classes of term graphs for denoting cyclic λ -terms, term graphs with
higher-order features and their first-order ‘implementations’. All higher-order term graphs we consider
are built from three kinds of vertices, which symbolize applications, abstractions, and variable occurrences, respectively. They also carry features that describe notions of scope, which are subject to certain
conditions that guarantee the meaningfulness of the term graph (that a λ -term is denoted), and in some
cases are crucial to define binding. The first-order implementations do not have these additional features,
but they may contain scope-delimiter vertices.
In particular we study the following three kinds (of classes) of term graphs:
λ -Higher-order-term-graphs (Section 3) are extensions of first-order term graphs by adding a scope
function that assigns a set of vertices, its scope, to every abstraction vertex. There are two variants,
one with and one without an edge (a back-link) from each variable occurrence to its corresponding
abstraction vertex. The class with back-links is related to higher-order term graphs as defined by
Blom in [4], and in fact is an adaptation of that concept for the purpose of representing λ -terms.
Abstraction-prefix based λ -higher-order-term-graphs (Section 4) do not have a scope function but assign, to each vertex w, an abstraction prefix consisting of a word of abstraction vertices that includes those abstractions for which w is in their scope (it actually lists all abstractions for which w
is in their ‘extended scope’ [6]). Abstraction prefixes are aggregations of scope information that is
relevant for and locally available at individual vertices.
λ -Term-graphs with scope delimiters (Section 5) are plain first-order term graphs intended to represent
higher-order term graphs of the two sorts above, and in this way stand for λ -terms. Instead of
relying upon additional features for describing scopes, they use scope-delimiter vertices to signify
the end of scopes. Variable occurrences as well as scoping delimiters may or may not have backlinks to their corresponding abstraction vertices.
Each of these classes induces a notion of homomorphism (functional bisimulation) and bisimulation.
Homomorphisms increase sharing in term graphs, and in this way induce a sharing order. They preserve
the unfolding semantics of term graphs1 , and therefore are able to preserve λ -terms that are denoted by
term graphs in the unfolding semantics. Term graphs from the classes we consider always represent finite
or infinite λ -terms, and in this sense are not ‘meaningless’. But this is not shown here. Instead, we lean
on motivating examples, intuitions, and the concept of higher-order term graph from [4].
We establish a bijective correspondence between the former two classes, and a correspondence between the latter two classes that is ‘almost bijective’ (bijective up to sharing or unsharing of scope
delimiter vertices). All of these correspondences preserve and reflect the sharing order. Furthermore,
we systematically investigate which specific class of λ -term-graphs is closed under homomorphism and
renders the mentioned correspondences possible. We prove (in Section 6) that this can only hold for a
class in which both variable-occurrence and scope-delimiter vertices have back-links to corresponding
abstractions, and establish (in Section 7) that the subclass containing only λ -term-graphs with eager
application of scope-closure satisfies these properties. For this class the correspondences allow us:
• to transfer properties known for first-order term graphs, such as the existence of a maximally
shared form, from λ -term-graphs to the corresponding classes of higher-order λ -term-graphs;
• to implement maximal sharing for higher-order λ -term-graphs (with eager scope closure) via
bisimulation collapse of the corresponding first-order λ -term-graphs (see algorithm in Section 8).
We stress that this paper in its present form is only a report about work in progress, and, while a
number of proofs are included, predominantly has the character of an extended abstract.
1

While this is well-known for first-order term graphs, it can also be proved for the higher-order term graphs considered here.

58

2

Term Graph Representations for Cyclic Lambda-Terms

Preliminaries

By N we denote the natural numbers including zero. For words w over an alphabet A we denote the
length of w by ∣w∣. For a function f ∶ A → B we denote by dom( f ) the domain, and by im( f ) the image
of f ; and for A0 ⊆ A we denote by f ∣A0 the restriction of f to A0 .
Let Σ be a signature with arity function ar ∶ Σ → N. A term graph over Σ is a tuple ⟨V,lab,args,r⟩
where V is a set of vertices, lab ∶ V → Σ the (vertex) label function, args ∶ V → V ∗ the argument function
that maps every vertex v to the word args(v) consisting of the ar(lab(v)) successor vertices of v (hence
it holds ∣args(v)∣ = ar(lab(v))), r, the root is a vertex in V , and where every vertex is reachable from
the root (by a path that arises by repeatedly going from a vertex to one of its successors). (Note this
reachability condition, and mind the fact that term graphs may have infinitely many vertices.) By a
Σ-term-graph we mean a term graph over Σ. And by TG(Σ) we mean the class of all term graphs over Σ.
Let G be a term graph over signature Σ. As useful notation for picking out any vertex or the i-th
vertex from among the ordered successors of a vertex v in G we define the (not indexed) edge relation
↣ ⊆ V ×V , and for each i ∈ N the indexed edge relation ↣i ⊆ V ×V , between vertices by stipulating that:
w ↣i w′ ∶ ⇐⇒ ∃w0 ,...,wn ∈ V . args(w) = w0 ...wn ∧ w′ = wi
w ↣ w′ ∶ ⇐⇒ ∃i ∈ N. w ↣i w′

holds for all w,w′ ∈ V . We write w f↣i w′ if w ↣i w′ ∧ lab(w) = f holds for w,w′ ∈ V , i ∈ N, f ∈ Σ, to indicate
the label at the source of an edge. A path in G is a tuple of the form ⟨w0 ,k0 ,w1 ,k1 ,w2 ,...,wn−1 ,kn−1 ,wn ⟩
where w0 ,...,wn ∈ V and n,k0 ,k1 ,...,kn−1 ∈ N such that w0 ↣k0 w1 ↣k1 w2 ⋯ wn−1 ↣kn−1 wn holds; paths
will usually be denoted in the latter form, using indexed edge relations. An access path of a vertex w of
G is a path that starts at the root of G, ends in w, and does not visit any vertex twice. Note that every
vertex w has at least one access path: since every vertex in a term graph is reachable from the root, there
is a path π from r to w; then an access path of w can be obtained from π by repeatedly cutting out cycles,
that is, parts of the path between different visits to one and the same vertex.
In the sequel, let G1 = ⟨V1 ,lab1 ,args1 ,r1 ⟩, G2 = ⟨V2 ,lab2 ,args2 ,r2 ⟩ be term graphs over signature Σ.
A homomorphism, also called a functional bisimulation, from G1 to G2 is a morphism from the
structure ⟨V1 ,lab1 ,args1 ,r1 ⟩ to the structure ⟨V2 ,lab2 ,args2 ,r2 ⟩, that is, a function h ∶ V1 → V2 such that,
for all v ∈ V1 it holds:
lab1 (v) = lab2 (h(v))
h̄(args1 (v)) = args2 (h(v))
h(r1 ) = r2

(labels)
(arguments)
(roots)

⎫
⎪
⎪
⎪
⎪
⎬
⎪
⎪
⎪
⎪
⎭

(1)

where h̄ is the homomorphic extension of h to words over V1 , that is, to the function h̄ ∶ V1∗ → V2∗ ,
v1 ...vn ↦ h(v1 )...h(vn ). In this case we write G1 →h G2 , or G2 ←h G1 . And we write G1 → G2 , or
for that matter G2 ← G1 , if there is a homomorphism (a functional bisimulation) from G1 to G2 .
Let f ∈ Σ. We write G1 →f G2 or G2 ←f G1 if there is a homomorphism h between G1 and G2 with
the property that for all w1 ,w2 ∈ V1 with w1 ≠ w2 it holds that h(w1 ) = h(w2 ) ⇒ lab1 (w1 ) = lab1 (w2 ) = f,
that is, if h only ‘shares’, or ‘identifies’, vertices when they have label f. If h is such a homomorphism,
we also write G1 →fh G2 or G2 ←fh G1 .
A bisimulation between G1 and G2 is a term graph G = ⟨R,lab,args,r⟩ over Σ with R ⊆ V1 ×V2 and
r = ⟨r1 , r2 ⟩ such that G1 ←π1 G →π2 G2 where π1 and π2 are projection functions, defined, for i ∈ {1,2},
by πi ∶ V1 ×V2 → Vi , ⟨v1 , v2 ⟩ ↦ vi . In this case we write G1 ↔R G2 . And we write G1 ↔ G2 if there is a
bisimulation between G1 and G2 .

C. Grabmayer & J. Rochel

59

Alternatively, bisimulations for term graphs can be defined directly as relations on the vertex sets,
obtaining the same notion of bisimilarity. In this formulation, a bisimulation between G1 and G2 is a
relation R ⊆ V1 ×V2 such that the following conditions hold, for all ⟨v, v′ ⟩ ∈ R:
⟨r1 , r2 ⟩ ∈ R

lab1 (v) = lab2 (v′ )
′

(roots)
(labels)

∗

⟨args1 (v), args2 (v )⟩ ∈ R

(arguments)

where R∗ ∶= {⟨v1 ⋯vk , v′1 ⋯v′k ⟩ ∣ v1 ,...,vk ∈ V1 , v′1 ,...,v′k ∈ V2 for k ∈ N such that⟨vi , v′i ⟩ ∈ R for all 1 ≤ i ≤ k}.
Bisimulation is an equivalence relation on the class TG(Σ) of term graphs over a signature Σ. The
homomorphism (functional bisimulation) relation → is a pre-order on term graphs over a given signature
Σ, and it induces a partial order on isomorphism equivalence classes of term graphs over Σ. We will refer
to → as the sharing pre-order, and will speak of it as sharing order, dropping the ‘pre’. The bisimulation
equivalence class [[G]∼ ]↔ ∶= {[G′ ]∼ ∣ G′ ↔ G} of the isomorphism equivalence class [G]∼ of a term
graph G is ordered by homomorphism → such that ⟨[[G]∼ ]↔, →⟩ is a complete lattice [3, 10].Note that,
different from e.g. [10], we use the order relation → in the same direction as ≤: if G1 → G2 , then G2 is
greater or equal to G1 in the ordering → (indicating that sharing is typically increased from G1 to G2 ).
Let K ⊆ TG(Σ) be a subclass of the term graphs over Σ, for a signature Σ. We say that K is closed
under homorphism (closed under bisimulation) if G → G′ (resp. G ↔ G′ ) for G,G′ ∈ TG(Σ) with G ∈ K
implies G′ ∈ K. Note these concepts are invariant under considering other signatures Σ′ with K ⊆ TG(Σ′ ).

3

λ -higher-order-Term-Graphs

By Σλ we designate the signature {@,λ } with ar(@) = 2, and ar(λ ) = 1. By Σλi , for i ∈ {0,1}, we denote
the extension Σλ ∪ {0} of Σλ where ar(0) = i. The classes of term graphs over Σλ0 and Σλ1 are denoted by
T0 and T1 , respectively.
Let G = ⟨V,lab,args,r⟩ be a term graph over a signature extending Σλ or Σλi , for i ∈ {0,1}. By V(λ )
we designate the set of abstraction vertices of G, that is, the subset of V consisting of all vertices with
label λ ; more formally, V(λ ) ∶= {v ∈ V ∣ lab(v) = λ }. Analogously, the sets V(@) and V(0) of application
vertices and variable vertices of G are defined as the sets consisting of all vertices in V with label @ or
label 0, respectively. Whether the variable vertices have an outgoing edge depends on the value of i. The
intention is to consider two variants of term graphs, one with and one without variable back-links to their
corresponding abstraction.
A ‘λ -higher-order-term-graph’ consists of a Σλi -term-graph together with a scope function that maps
abstraction vertices to their scopes (‘extended scopes’ in [6]), which are subsets of the set of vertices.
Definition 1 (λ -ho-term-graph) Let i ∈ {0,1}. A λ -ho-term-graph (short for λ -higher-order-termgraph) over Σλi , is a five-tuple G = ⟨V,lab,args,r,Sc⟩ where GG = ⟨V,lab,args,r⟩ is a Σλi -term-graph,
called the term graph underlying G, and Sc ∶ V(λ ) → ℘(V ) is the scope function of G (which maps an
abstraction vertex v to a set of vertices called its scope) that together with GG fulfills the following conditions: For all k ∈ {0,1}, all vertices w,w0 ,w1 ∈ V , and all abstraction vertices v,v0 ,v1 ∈ V(λ ) it holds:
⇒ r ∉ Sc− (v)
−

⇒ v ∈ Sc(v)

(root)
−

v1 ∈ Sc (v0 ) ⇒ Sc(v1 ) ⊆ Sc (v0 )
−

w ↣k wk ∧ wk ∈ Sc (v) ⇒ w ∈ Sc(v)

(self)
(nest)
(closed)

60

Term Graph Representations for Cyclic Lambda-Terms

G0 :

λ

λ

@

@

λ

λ

@

@

0

G1 :

@
0

λ

λ

@

@

0
λ

@
0

0

λ
0

Figure 1: G0 and G1 are λ -ho-term-graphs in Hiλ whereby the dotted back-link edges are present for
i = 1, but absent for i = 0. The underlying term graphs of G0 and G1 are identical but their scope functions
(signified by the shaded areas) differ. While in G0 scopes are chosen as small as possible, which we refer
to as ‘eager scope closure’, in G1 some scopes are closed only later in the graph.
w ∈ V(0) ⇒ ∃v0 ∈ V(λ ). w ∈ Sc− (v0 )
w ∈ V(0) ∧ w ↣0 w0

⎧
w0 ∈ V(λ ) ∧
⎪
⎪
⎪
⇒ ⎨ ∧ ∀v ∈ V(λ ).
⎪
⎪
⎪
(w ∈ Sc(v) ⇔ w0 ∈ Sc(v))
⎩

(scope)0
(scope)1

where Sc− (v) ∶= Sc(v) ∖ {v}. Note that if i = 0, then (scope)1 is trivially true and hence superfluous, and
if i = 1, then (scope)0 is redundant, because it follows from (scope)1 in this case. For w ∈ V and v ∈ V(λ )
we say that v is a binder for w if w ∈ Sc(v), and we designate by bds(w) the set of binders of w.
The classes of λ -ho-term-graphs over Σλ0 and Σλ1 will be denoted by H0λ and H1λ .
See Fig. 1 for two different λ -ho-term-graphs over Σλi both of which represent the same term in the
λ -calculus with letrec, namely letrec f = λ x.(λ y.y (x g)) (λ z.g f ), g = λ u.u in f .
The following lemma states some basic properties of the scope function in λ -ho-term-graphs. Most
importantly, scopes in λ -ho-term-graphs are properly nested, in analogy with scopes in finite λ -terms.
Lemma 2 Let i ∈ {0,1}, and let G = ⟨V,lab,args,r,Sc⟩ be a λ -ho-term-graph over Σλi . Then the following
statements hold for all w ∈ V and v,v1 ,v2 ∈ V(λ ):
(i) If w ∈ Sc(v), then v is visited on every access path of w, and all vertices on access paths of w after v
are in Sc− (v). Hence (since GG is a term graph, every vertex has an access path) bds(w) is finite.
(ii) If Sc(v1 ) ∩ Sc(v2 ) ≠ ∅ for v1 ≠ v2 , then Sc(v1 ) ⊆ Sc− (v2 ) or Sc(v2 ) ⊆ Sc− (v1 ). As a consequence,
if Sc(v1 ) ∩ Sc(v2 ) ≠ ∅, then Sc(v1 ) ⫋ Sc(v2 ) or Sc(v1 ) = Sc(v2 ) or Sc(v2 ) ⫋ Sc(v1 ).
(iii) If bds(w) ≠ ∅, then bds(w) = {v0 ,...,vn } for v0 ,...,vn ∈ V(λ ) and Sc(vn ) ⫋ Sc(vn−1 )... ⫋ Sc(v0 ).
Proof. Let i ∈ {0,1}, and let G = ⟨V,lab,args,r,Sc⟩ be a λ -ho-term-graph over Σλi .
For showing (i), let w ∈ V and v ∈ V(λ ) be such that w ∈ Sc(v). Suppose that π ∶ r = w0 ↣k0 w1 ↣k1
w2 ⋯ ↣kn−1 wn = w is an access path of w. If w = v, then nothing remains to be shown. Otherwise wn =
w ∈ Sc− (v), and, if n > 0, then by (closed) it follows that wn−1 ∈ Sc(v). This argument can be repeated
to find subsequently smaller i with wi ∈ Sc(v) and wi+1 ,...,wn ∈ Sc− (v). We can proceed as long as

C. Grabmayer & J. Rochel

61

wi ∈ Sc− (v). But since, due to (root), w0 = r ∉ Sc− (v), eventually we must encounter an i0 such that such
that wi0 +1 ,...,wn ∈ Sc− (v) and wi0 ∈ Sc(v) ∖ Sc− (v). This implies wi0 = v, showing that v is visited on π.
For showing (ii), let w ∈ V and v1 ,v2 ∈ V(λ ), v1 ≠ v2 be such that w ∈ Sc(v1 ) ∩ Sc(v2 ). Let π be an
access path of w. Then it follows by (i) that both v1 and v2 are visited on π, and that, depending on
whether v1 or v2 is visited first on π, either v2 ∈ Sc− (v1 ) or v1 ∈ Sc− (v2 ). Then due to (nest) it follows that
either Sc(v2 ) ⊆ Sc− (v1 ) holds or Sc(v1 ) ⊆ Sc− (v2 ).
Finally, statement (iii) is an easy consequence of statement (ii).
◻
Remark 3 The notion of λ -ho-term-graph is an adaptation of the notion of ‘higher-order term graph’
by Blom [4, Def. 3.2.2] for the purpose of representing finite or infinite λ -terms or cyclic λ -terms, that
is, terms in the λ -calculus with letrec. In particular, λ -ho-term-graphs over Σλ1 correspond closely to
higher-order term graphs over signature Σλ . But they differ in the following respects:
Abstractions: Higher-order term graphs in [4] are graph representations of finite or infinite terms in Combinatory
Reduction Systems (CRSs). They typically contain abstraction vertices with label ◻ that represent CRS-abstractions. In contrast, λ -ho-term-graphs have abstraction vertices with label λ that denote λ -abstractions.
Signature: Whereas higher-order term graphs in [4] are based on an arbitrary CRS-signature, λ -ho-term-graphs
over Σλ1 only contain the application symbol @ and the variable-occurrence symbol 0 in addition to the
abstraction symbol λ .
Variable back-links and variable occurrence vertices: In the formalization of higher-order term graphs in [4] there
are no explicit vertices that represent variable occurrences. Instead, variable occurrences are represented by
back-link edges to abstraction vertices. Actually, in the formalization chosen in [4, Def. 3.2.1], a back-link
edge does not directly target the abstraction vertex v it refers to, but ends at a special variant vertex v̄ of v.
(Every such variant abstraction vertex v̄ could be looked upon as a variable vertex that is shared by all edges
that represent occurrences of the variable bound by the abstraction vertex v.)
In λ -ho-term-graphs over Σλ1 a variable occurrence is represented by a variable-occurrence vertex that as
outgoing edge has a back-link to the abstraction vertex that binds the occurrence.
conditions on the scope function: While the conditions (root), (self), (nest), and (closed) on the scope function in
higher-order term graphs in [4, Def. 3.2.2] correspond directly to the respective conditions in Def. 1, the
difference between the condition (scope) there and (scope)1 in Def. 1 reflects the difference described in the
previous item.
free variables: Whereas the higher-order term graphs in [4] cater for the presence of free variables, free variables
have been excluded from the basic format of λ -ho-term-graphs.

Definition 4 (homomorphism, bisimulation) Let i ∈ {0,1}. Let G1 and G2 be λ -ho-term-graphs over
Σλi with Gk = ⟨Vk ,labk ,argsk ,rk ,Sck ⟩ for k ∈ {1,2}.
A homomorphism, also called a functional bisimulation, from G1 to G2 is a morphism from the structure ⟨V1 ,lab1 ,args1 ,r1 ,Sc1 ⟩ to the structure ⟨V2 ,lab2 ,args2 ,r2 ,Sc2 ⟩, that is, a function h ∶ V1 → V2 such
that, for all v ∈ V1 the conditions (labels), (arguments), and (roots) in in (1) are satisfied, and additionally,
for all v ∈ V1(λ ):
(2)
h̄¯ (Sc1 (v)) = Sc2 (h(v))
(scope functions)
where h̄¯ is the homomorphic extension of h to sets over V1 , that is, to the function h̄ ∶ ℘(V1 ) → ℘(V2 ),
A ↦ {h(a) ∣ a ∈ A}. If there exists a homomorphism (a functional bisimulation) h from G1 to G2 , then we
write G1 →h G2 or G2 ←h G1 , or, dropping h as subscript, G1 → G2 or G2 ← G1 .
A bisimulation between G1 and G2 is a term graph G = ⟨R,lab,args,r,Sc⟩ over Σ with R ⊆ V1 ×V2 and
r = ⟨r1 , r2 ⟩ such that G1 ←π1 G →π2 G2 where π1 and π2 are projection functions, defined, for i ∈ {1,2}, by
πi ∶ V1 ×V2 → Vi , ⟨v1 , v2 ⟩ ↦ vi . If there exists a bisimulation R between G1 and G2 , then we write G1 ↔R G2 ,
or just G1 ↔ G2 .

62

Term Graph Representations for Cyclic Lambda-Terms

()

()

G0′ :

λv0

λv0

@(v0 )

@(v0 )

λv10

(v )

λv3

()

@(v0 v1 )

@()

(v )

λv30

(v )

@(v0 v1 )

@(v0 )

0(v0 v1 ) @(v0 v1 )

0(v0 v1 ) @(v0 )
0(v0 )

G1′ :

λv10

()

λv2
0(v2 )

0(v0 )

()

λv2
0(v2 )

Figure 2: The λ -ap-ho-term-graphs corresponding to the λ -ho-term-graphs in Fig 1. The subscripts of
abstraction vertices indicate their names. The super-scripts of vertices indicate their abstraction-prefixes.
A precise formulation of this correspondence is given in Example 11.

4

Abstraction-prefix based λ -h.o.-term-graphs

By an ‘abstraction-prefix based λ -higher-order-term-graph’ we will mean a term-graph over Σλi for
i ∈ {0,1} that is endowed with a correct abstraction prefix function that maps abstraction vertices v to
words of vertices that represent the sequence of abstractions that have v in their scope. The conceptual
difference between the abstraction-prefix function and the scope function is that the former makes the
most essential scoping information locally available. It explicitly states all ‘extended scopes’ (induced
by the transitive closure of the in-scope relation, see [6]) in which a node resides in the order of their
nesting. This approach leads to simpler correctness conditions.
Definition 5 (correct abstraction-prefix function for Σλi -term-graphs) Let G = ⟨V,lab,args,r⟩ be, for
an i ∈ {0,1}, a Σλi -term-graph.
A function P ∶ V → V ∗ from vertices of G to words of vertices is called an abstraction-prefix function
for G. Such a function is called correct if for all w,w0 ,w1 ∈ V and k ∈ {0,1}:
⇒ P(r) = ε

(root)

w ∈ V(λ ) ∧ w ↣0 w0 ⇒ P(w0 ) ≤ P(w)w

(λ )

w ∈ V(@) ∧ w ↣k wk ⇒ P(wk ) ≤ P(w)

(@)

w ∈ V(0) ⇒ P(w) ≠ ε
w ∈ V(0) ∧ w ↣0 w0 ⇒ w0 ∈ V(λ ) ∧ P(w0 )w0 = P(w)

(0)0
(0)1

Note that analogously as in Def. 1, if i = 0, then (0)1 is trivially true and hence superfluous, and if i = 1,
then (0)0 is redundant, because it follows from (0)1 in this case.
We say that G admits a correct abstraction-prefix function if such a function exists for G.
Definition 6 (λ -ap-ho-term-graph) Let i ∈ {0,1}. A λ -ap-ho-term-graph (short for abstraction-prefix
based λ -higher-order-term-graph) over signature Σλi is a five-tuple G = ⟨V,lab,args,r,P⟩ where GG =
⟨V,lab,args,r⟩ is a Σλi -term-graph, called the term graph underlying G, and P is a correct abstractionprefix function for GG . The classes of λ -ap-ho-term-graphs over Σλi will be denoted by Hi(λ ) .
See Fig. 2 for two examples, which correspond, as we will see, to the λ -ho-term-graphs in Fig. 1.
The following lemma states some basic properties of the scope function in λ -ap-ho-term-graphs.

C. Grabmayer & J. Rochel

63

Lemma 7 Let i ∈ {0,1} and let G = ⟨V,lab,args,r,P⟩ be a λ -ap-ho-term-graph over Σλi . Then the following statements hold:
(i) Suppose that, for some v,w ∈ V , v occurs in P(w). Then v ∈ V(λ ), occurs in P(w) only once, and
every access path of w passes through v, but does not end there, and thus w ≠ v. Furthermore it
holds: P(v)v ≤ P(w). In particular, if P(w) = pv, then P(v) = p.
(ii) Vertices in abstraction prefixes are abstraction vertices, and hence P is of the form P ∶ V → (V(λ ))∗ .
(iii) For all v ∈ V(λ ) it holds: v ∉ P(v).
(iv) While access paths might end in vertices in V(0), they only pass through vertices in V(λ ) ∪V(@).
Proof. Let i ∈ {0,1} and let G = ⟨V,lab,args,r,P⟩ be a λ -ap-ho-term-graph over Σλi .
For showing (i), let v,w ∈ V be such that v occurs in P(w). Suppose further that π is an access path
of w. Note that when walking through π the abstraction prefix starts out empty (due to (root)), and is
expanded only in steps from vertices v′ ∈ V(λ ) (due to (λ ), (@), and (0)1 ) in which just v′ is added to the
prefix on the right (due to (λ )). Since v occurs in P(w), it follows that v ∈ V(λ ), that v must be visited on
π, and that π continues after the visit to v. That π is an access path also entails that v is not visited again
on π, hence that w ≠ v and that v occurs only once in P(w), and that P(v)v, the abstraction prefix of the
successor vertex of v on π, is a prefix of the abstraction prefix of every vertex that is visited on π after v.
Statements (ii) and (iii) follow directly from statement (i).
For showing (iv), consider an access path π ∶ r = w0 ↣ ⋯ ↣ wn that leads to a vertex wn ∈ V(0). If
i = 0, then there is no path that extends π properly beyond wn . So suppose i = 1, and let wn+1 ∈ V be such
that wn ↣0 wn+1 . Then (0)1 implies that P(wn ) = P(wn+1 )wn+1 , from which it follows by (i) that wn+1 is
visited already on π. Hence π does not extend to a longer path that is again an access path.
◻
Definition 8 (homomorphism, bisimulation) Let i ∈ {0,1}. Let G1 and G2 be λ -ap-ho-term-graphs over
Σλi with Gk = ⟨Vk ,labk ,argsk ,rk ,Pk ⟩ for k ∈ {1,2}.
A homomorphism, also called a functional bisimulation, from G1 to G2 is a morphism from the
structure ⟨V1 ,lab1 ,args1 ,r1 ,P1 ⟩ to the structure ⟨V2 ,lab2 ,args2 ,r2 ,P2 ⟩, that is, a function h ∶ V1 → V2 such
that, for all v ∈ V1 the conditions (labels), (arguments), and (roots) in in (1) are satisfied, and additionally,
for all v ∈ V1 :
h̄(P1 (v)) = P2 (h(v))
(abstraction-prefix functions)
(3)
where h̄ is the homomorphic extension of h to words over V1 . In this case we write G1 →h G2 , or G2 ←h G1 .
And we write G1 → G2 , or for that matter G2 ← G1 , if there is a homomorphism (a functional bisimulation)
from G1 to G2 .
A bisimulation between G1 and G2 is a term graph G = ⟨R,lab,args,r,Sc⟩ over Σ with R ⊆ V1 ×V2 and
r = ⟨r1 , r2 ⟩ such that G1 ←π1 G →π2 G2 where π1 and π2 are projection functions, defined, for i ∈ {1,2}, by
πi ∶ V1 ×V2 → Vi , ⟨v1 , v2 ⟩ ↦ vi . If there exists a homomorphism (a functional bisimulation) h from G1 to
G2 , then we write G1 →h G2 or G2 ←h G1 , or, dropping h as subscript, G1 → G2 or G2 ← G1 .
The following proposition defines mappings between λ -ho-term-graphs and λ -ap-ho-term-graphs
by which we establish a bijective correspondence between the two classes. For both directions the
underlying λ -term-graph remains unchanged. Ai derives an abstraction-prefix function P from a scope
function by assigning to each vertex a word of its binders in the correct nesting order. Bi defines its scope
function Sc by assigning to each λ -vertex v the set of vertices that have v in their prefix (along with v
since a vertex never has itself in its abstraction prefix).

64

Term Graph Representations for Cyclic Lambda-Terms

Proposition 9 For each i ∈ {0,1}, the mappings Ai and Bi are well-defined between the class of λ -hoterm-graphs over Σλi and the class of λ -ap-ho-term-graphs over Σλi :
Ai ∶ Hiλ → Hi(λ ) , G = ⟨V,lab,args,r,Sc⟩ ↦ Ai (G) ∶= ⟨V,lab,args,r,P⟩

⎫
⎪
⎪
⎪
⎪
∗
where P ∶ V → V , w ↦ v0 ⋯ vn if bds(w) ∖ {w} = {v0 ,...,vn } and⎬
⎪
⎪
⎪
Sc(vn ) ⫋ Sc(vn−1 )... ⫋ Sc(v0 ) ⎪
⎭
⎫
⎪
Bi ∶ Hi(λ ) → Hiλ , G = ⟨V,lab,args,r,P⟩ ↦ Ai (G) ∶= ⟨V,lab,args,r,Sc⟩
⎪
⎬
where Sc ∶ V(λ ) → ℘(V ), v ↦ {w ∈ V ∣ v occurs in P(w)} ∪ {v} ⎪
⎪
⎭

(4)

(5)

Theorem 10 (correspondence of λ -ho-term-graphs with λ -ap-ho-term-graphs) For each i ∈ {0,1}
it holds that the mappings Ai in (4) and Bi in (5) are each other’s inverse; thus they define a bijective
correspondence between the class of λ -ho-term-graphs over Σλi and the class of λ -ap-ho-term-graphs
over Σλi . Furthermore, they preserve and reflect the sharing orders on Hiλ and on Hi(λ ) :
(∀G1 ,G2 ∈ Hiλ )

(∀G1 ,G2 ∈ Hi(λ ) )

G1 → G2 ⇐⇒ Ai (G1 ) → Ai (G1 )
Bi (G1 ) → Bi (G1 ) ⇐⇒ G1 → G2

Example 11 The λ -ho-term-graphs in Fig. 1 correspond to the λ -ap-ho-term-graphs in Fig. 2 via the
Ai (G1 ) = G1′ .
Bi (G0 ) = G0′ ,
Ai (G1 ) = G1′ ,
mappings Ai and Bi as follows:
Ai (G0 ) = G0′ ,
For λ -ho-term-graphs over the signature Σλ0 (that is, without variable back-links) essential binding
information is lost when looking only at the underlying term graph, to the extent that λ -terms cannot
be unambiguously represented anymore. For instance the λ -ho-term-graphs that represent the λ -terms
λ xy.x y and λ xy.x x have the same underlying term graph. The same holds for λ -ap-ho-term-graphs.
This is not the case for λ -ho-term-graphs (λ -ap-ho-term-graphs) over Σλ1 , because the abstraction
vertex to which a variable-occurrence vertex belongs is uniquely identified by the back-link. This is the
reason why the following notion is only defined for the signature Σλ1 .
Definition 12 (λ -term-graph over Σλ1 ) A term graph G over Σλ1 is called a λ -term-graph over Σλ1 if G
admits a correct abstraction-prefix function. By T1(λ ) we denote the class of λ -term-graphs over Σλ1 .
In the rest of this section we examine, and then dismiss, a naive approach to implementing functional
bisimulation on λ -ho-term-graphs or λ -ap-ho-term-graphs, which is to apply the homomorphism on the
underlying term graph, hoping that this application would simply extend to the λ -ho-term-graph (λ -apho-term-graph) without further ado. We demonstrate that this approach fails, concluding that a faithful
first-order implementation of functional bisimulation must not be negligent of the scoping information.
Definition 13 (scope- and abstraction-prefix-forgetful mappings) Let i ∈ {0,1}. The scope-forgetful
mapping ScFiλ and the abstraction-prefix-forgetful mapping PF1(λ ) map λ -ho-term-graphs in Ti(λ ) , and
respectively, λ -ho-term-graphs in Ti(λ ) to their underlying term graphs:
ScFiλ ∶ Hiλ → Ti , ⟨V,lab,args,r,Sc⟩ ↦ ⟨V,lab,args,r⟩
PFi(λ ) ∶ Hi(λ ) → Ti , ⟨V,lab,args,r,P⟩ ↦ ⟨V,lab,args,r⟩
Definition 14 Let G be a λ -ho-term-graph over Σλi for i ∈ {0,1} with underlying term graph ScFiλ (G).
And suppose that ScFiλ (G) →h G′ holds for a term graph G′ over Σλi and a functional bisimulation h. We
say that h extends to a functional bisimulation on G if G′ can be endowed with a scope function to obtain
a λ -ho-term-graph G ′ with ScFiλ (G ′ ) = G′ and such that it holds G →h G ′ .

C. Grabmayer & J. Rochel

65

We say that a class K of λ -ho-term-graphs is closed under functional bisimulations on the underlying
term graphs if for every G ∈ K and for every homomorphism h on the term graph underlying G that
witnesses ScFiλ (G) →h G′ for a term graph G′ there exists G ′ ∈ K with ScFiλ (G ′ ) = G′ such that G →h G ′
holds, that is, h is also a homorphism between G and G ′ .
These notions are also extended, by analogous stipulations, to λ -ap-ho-term-graphs over Σλi for
i ∈ {0,1} and their underlying term graphs.
Proposition 15 Neither the class H1λ of λ -ho-term-graphs nor the class H1(λ ) of λ -ap-ho-term-graphs
is closed under functional bisimulations on the underlying term graphs.
Proof. In view of Thm. 10 it suffices to show the statement for H1λ . We show that not every functional
bisimulation on the term graph underlying a λ -ho-term-graph over Σλ1 extends to a functional bisimulation on the higher-order term graphs. Consider the following term graphs G0 and G1 over Σλ1 (at first,
please ignore the scope shading):
λ

λ

@
λ

G1 :

@

G0 :

@

0

0

@
0

@
@
0

0

0

There is an obvious homomorphism h that witnesses G1 →h G0 . Both of these term graphs extend to
λ -ho-term-graphs by suitable scope functions (one possibility per term graph is indicated by the scope
shadings above; G1 actually admits two possibilities). However, h does not extend to any of the λ -hoterm-graphs G1 and G0 that extend G1 and G0 , respectively.
◻
The next proposition is merely a reformulation of Prop. 15.
Proposition 16 The scope-forgetful mapping ScF1λ on H1λ and the abstraction-prefix-forgetful mapping
PF1(λ ) on H1(λ ) preserve, but do not reflect, the sharing orders on these classes. In particular:
(∀G1 ,G2 ∈ H1(λ ) )

(∃G1 ,G2 ∈ H1(λ ) )

G1 → G2 Ô⇒ PF1(λ ) (G1 ) → PF1(λ ) (G2 )
G1 →
/ G2 ∧ PF1(λ ) (G1 ) → PF1(λ ) (G2 )

As a consequence of this proposition it is not possible to faithfully implement functional bisimulation
on λ -ho-term-graphs and λ -ap-ho-term-graphs by only considering the underlying term graphs, and in
doing so neglecting2 the scoping information from the scope function, or respectively, from the abstraction prefix function. In order to yet be able to implement functional bisimulation of λ -ho-term-graphs
and λ -ap-ho-term-graphs in a first-order setting, in the next section we introduce a class of first-order
term graphs that accounts for scoping by means of scope delimiter vertices.

5

λ -Term-Graphs with Scope Delimiters

For all i ∈ {0,1} and j ∈ {1,2} we define the extensions Σλi, j ∶= Σλ ∪ {0,S} of the signature Σλ where
ar(0) = i and ar(S) = j , and we denote the class of term graphs over signature Σλi, j by Ti, j .
2
In the case of Σλ1 implicit information about possible scopes is being kept, due to the presence of back-links from variable
occurrence vertices to abstraction vertices. But this is not enough for reflecting the sharing order under the forgetful mappings.

66

Term Graph Representations for Cyclic Lambda-Terms

Let G be a term graph with vertex set V over a signature extending Σλi, j for i ∈ {0,1} and j ∈ {1,2}.
We denote by V(S) the subset of V consisting of all vertices with label S, which are called the delimiter
vertices of G. Delimiter vertices signify the end of an ‘extended scope’ [6]. They are analogous to
occurrences of function symbols S in representations of λ -terms in a nameless de-Bruijn index [5] form
in which Dedekind numerals based on 0 and the successor function symbol S are used (this form is due
to Hendriks and van Oostrom, see also [9], and is related to their end-of-scope symbol λ [7]).
Analogously as for the classes Hiλ and Hi(λ ) , the index i will determine whether in correctly formed
λ -term-graphs (defined below) variable vertices have back-links to the corresponding abstraction. Here
additionally scope-delimiter vertices have such back-links (if j = 2) or not (if j = 1).
Definition 17 (correct abstraction-prefix function for Σλi, j -term-graphs) Let G = ⟨V,lab,args,r⟩ be a
Σλi, j -term-graph for an i ∈ {0,1} and an j ∈ {1,2}.
A function P ∶ V → V ∗ from vertices of G to words of vertices is called an abstraction-prefix function
for G. Such a function is called correct if for all w,w0 ,w1 ∈ V and k ∈ {0,1} it holds:
⇒ P(r) = ε

(root)

w ∈ V(λ ) ∧ w ↣0 w0 ⇒ P(w0 ) = P(w)w

(λ )

w ∈ V(@) ∧ w ↣k wk ⇒ P(wk ) = P(w)

(@)

w ∈ V(0)

⇒ P(w) ≠ ε

(0)0

w ∈ V(0) ∧ w ↣0 w0 ⇒ w0 ∈ V(λ ) ∧ P(w0 )w0 = P(w)

(0)1

w ∈ V(S) ∧ w ↣0 w0 ⇒ P(w0 )v = P(w) for some v ∈ V

(S)1

w ∈ V(S) ∧ w ↣1 w1 ⇒ w1 ∈ V(λ ) ∧ P(w1 )w1 = P(w)

(S)2

Note that analogously as in Def. 1 and in Def. 6, if i = 0, then (0)1 is trivially true and hence superfluous,
and if i = 1, then (0)0 is redundant, because it follows from (0)1 in this case. Additionally, if j = 1, then
(S)2 is trivially true and therefore superfluous.
Definition 18 (λ -term-graph over Σλi, j ) Let i ∈ {0,1} and j ∈ {1,2}. A λ -term-graph (with scope-delimiters) over Σλi, j is a Σλi, j -term-graph that admits a correct abstraction-prefix function. The class of
λ -term-graphs over Σλi, j is denoted by Ti,(λj ).
See Fig. 3 for examples, that, as we will see, correspond to the ho-term-graphs in Fig. 1 and in Fig. 2.
Lemma 19 Let i ∈ {0,1} and j ∈ {1,2}, and let G = ⟨V,lab,args,r⟩ be a λ -term-graph over Σλi, j . Then
the statements (i)–(iii) in Lemma 7 hold, and additionally:
(iv) Access paths may end in vertices in V(0), but only pass through vertices in V(λ ) ∪V(@) ∪V(S),
and depart from vertices in V(S) only via indexed edges S↣0 .
(v) There exists precisely one correct abstraction-prefix function on G.
Proof. That also here statements (i)–(iii) in Lemma 7 hold, and that statement (iv) holds, can be shown
analogously as in the proof of the respective items of Lemma 7. For (v) it suffices to observe that if P is
a correct abstraction-prefix function for G, then, for all w ∈ V , the value P(w) of P at w can be computed
by choosing an arbitrary access path π from r to w and using the conditions (λ ), (@), and (S)0 to
determine in a stepwise manner the values of P at the vertices that are visited on π. Hereby note that in
every transition along an edge on π the length of the abstraction prefix only changes by at most 1.
◻
Now we define a precise relationship between λ -term-graphs and λ -ap-ho-term-graphs via translation mappings between these classes:

C. Grabmayer & J. Rochel

G0 :

67

λ

λ

@

@

λ

S

@

λ

0

0

S

S

@

@

G1 :

S

λ

λ

@

S

0

@

@

S

S

0

S

S

λ

λ

0

0

S

Figure 3: The λ -term-graphs corresponding to the λ -ap-ho-term-graphs from Fig 2 and the λ -ho-termgraphs from Fig 1. A precise formulation of this correspondence is given in Example 23.
The mapping Gi, j (see Prop. 20) produces a λ -term-graph for any given λ -ap-ho-term-graph by adding
to the original set of vertices a number of delimiter vertices at the appropriate places. That is, at
every position where the abstraction prefix decreases by n elements, n S-vertices are inserted. In
the image, the original abstraction prefix is retained as part of the vertices. This can be considered
intermittent information used for the purpose of defining the edges of the image.
The mapping Gi, j (see Prop. 21) back to λ -ap-ho-term-graphs is simpler because it only has to erase the
S-vertices, and add the correct abstraction prefix that exists for the λ -term-graph to be translated.
Proposition 20 Let i ∈ {0,1} and j ∈ {1,2}. The mapping Gi, j defined below is well-defined between the
class of λ -term-graphs over Σλi, j and the class of λ -ap-ho-term-graphs over Σλi :
Gi, j ∶ Hi(λ ) → Ti,(λj ), G = ⟨V,lab,args,r,P⟩ ↦ Gi, j (G) ∶= ⟨V ′ ,lab′ ,args′ ,r′ ⟩
where:
V ′ ∶= {⟨w, P(w)⟩ ∣ w ∈ V } ∪ {⟨w,k,w′ , p⟩ ∣ w,w′ ∈ V, w ↣k w′ ,
r′ ∶= ⟨r, ε⟩

V(w) = λ ∧ P(w′ ) < p ≤ P(w)w
}
∨ V(w) = @ ∧ P(w′ ) < p ≤ P(w)

lab′ ∶ V ′ → Σλi, j , ⟨w, P(w)⟩ ↦ lab′ (⟨w, P(w)⟩) ∶= lab(w)
⟨w,k,w′ , p⟩ ↦ lab′ (w,k,w′ , p) ∶= S

and args′ ∶ V ′ → (V ′ )∗ is defined such that for the induced indexed successor relation ↣′(⋅) it holds:
w ↣k wk ∧ #del(w, k) = 0 Ô⇒ ⟨w, P(w)⟩ ↣′k ⟨wk , P(wk )⟩
w ↣0 w0 ∧ #del(w, 0) > 0 ∧ lab(w) = λ ∧ P(w) = P(w0 )v p
Ô⇒ ⟨w, P(w)⟩ ↣′0 ⟨w,0,w0 ,P(w)w⟩ ∧ ⟨w,0,w0 ,P(w0 )v⟩ ↣′0 ⟨w0 , P(w0 )⟩
w ↣k wk ∧ #del(w, k) > 0 ∧ lab(w) = @ ∧ P(w) = P(wk )v p
Ô⇒ ⟨w, P(w)⟩ ↣′k ⟨w,k,wk ,P(w)⟩ ∧ ⟨w,k,wk ,P(wk )v⟩ ↣′0 ⟨wk , P(wk )⟩

w ↣k wk ∧ #del(w, k) > 0 ∧ ⟨w,k,wk , pv⟩, ⟨w,k,wk , p⟩ ∈ V ′ Ô⇒ ⟨w,k,wk , pv⟩ ↣′0 ⟨w,k,wk , p⟩

w ↣k wk ∧ #del(w, k) > 0 ∧ ⟨w,k,wk , pv⟩ ∈ V ′ ∧ j = 2 Ô⇒ ⟨w,k,wk , pv⟩ ↣′1 ⟨wk , P(wk )⟩

68

Term Graph Representations for Cyclic Lambda-Terms

for all w,w0 ,w1 ,v ∈ V , k ∈ {0,1}, p ∈ V ∗ , and where the function #del is defined as:
⎧
⎪
∣P(w)∣ − ∣P(w′ )∣
if w ∈ V(@) ∧ w ↣k w′
⎪
⎪
⎪
′
#del(w, k) ∶= ⎨∣P(w)∣ + 1 − ∣P(w )∣ if w ∈ V(λ ) ∧ w ↣k w′
⎪
⎪
⎪
otherwise
⎪
⎩0
Proposition 21 Let i ∈ {0,1} and j ∈ {1,2}. The mapping Gi, j defined below is well-defined between the
class of λ -term-graphs over Σλi, j and the class of λ -ap-ho-term-graphs over Σλi :
Gi, j ∶ Ti,(λj ) → Hi(λ ) , G = ⟨V,lab,args,r⟩ ↦ Gi, j (G) ∶= ⟨V ′ ,lab′ ,args′ ,r′ ,P′ ⟩

where V ′ ∶= V(λ ) ∪V(@) ∪V(0), lab′ ∶= lab∣V ′ , r′ ∶= r,
args′ ∶ V ′ → (V ′ )∗ so that for the induced indexed succ. relation ↣′(⋅) :

v0 ↣′k v1 ∶⇔ v0 ↣k ⋅ (S↣0 )∗ v1 (for all v0 ,v1 ∈ V ′ , k ∈ {0,1})
P ∶= P∣V ′ for the correct abstraction-prefix function P for G.
′

Theorem 22 (correspondence between λ -ap-ho-term-graphs with λ -term-graphs) Let i ∈ {0,1} and
j ∈ {1,2}. The mappings Gi, j from Prop. 21 and Gi, j from Prop. 20 define a correspondence between the
classes of λ -term-graphs over Σλi, j and of λ -ap-ho-term-graphs over Σλi with the following properties:
(i) Gi, j ○ Gi, j = idHi(λ ) .

(ii) For all G ∈ Ti,(λj ) : (Gi, j ○ Gi, j )(G) →S G.
(iii) Gi, j and Gi, j preserve and reflect the sharing orders on Hi(λ ) and on Ti,(λj ):
(∀G1 ,G2 ∈ Hi(λ ) )

G1 → G2 ⇐⇒ Gi, j (G1 ) → Gi, j (G2 )

(∀G1 ,G2 ∈ Ti,(λj )) Gi, j (G1 ) → Gi, j (G2 ) ⇐⇒ G1 → G2

Example 23 The λ -ap-ho-term-graphs in Fig. 2 correspond to the λ -ap-ho-term-graphs in Fig. 3 via the
mappings Gi, j and Gi, j as follows:
Gi, j (G0 ) = G′0 , Gi, j (G1 ) = G′1 , Gi, j (G0 ) = G0′ , Gi, j (G1 ) = G1′ .
Remark 24 The correspondence in Theorem 22 is not a bijection since Gi, j is not injective. This can be
seen for the following graphs (here with i = 0 and j = 1) where we have G0,1 (G) = G = G0,1 (G′ ):
λ
@

G: λ

λ
S
0

λ

()

λv1

G:

@(v1 )
(v )

(v )

λv21 λv31
0(v1)

@

′

G: λ

λ

S

S

0

0

Obviously λ -ap-ho-term-graphs are not capable of reproducing the different degrees of S-sharing.

6

Not closed under bisimulation and functional bisimulation

In this section we collect all negative results concerning closedness under bisimulation and functional
bisimulation for the classes of λ -term-graphs as introduced in the previous section.

C. Grabmayer & J. Rochel

69

Proposition 25 None of the classes T1(λ ) and Ti,(λj ), for i ∈ {0,1} and j ∈ {1,2}, of λ -term-graphs are
closed under bisimulation.
This proposition is an immediate consequence of the next one, which can be viewed as a refinement,
because it formulates non-closedness of classes of λ -term-graphs under specializations of bisimulation,
namely for functional bisimulation (under which some classes are not closed), and for converse functional bisimulation (under which none of the classes considered here is closed).
Proposition 26 The following statements hold:
(i) None of the classes T0 ,(λj ) for j ∈ {1,2} of λ -term-graphs are closed under functional bisimulation
→, or under converse functional bisimulation ← .
(ii) None of the classes T1(λ ) and T1 ,(λj ) for j ∈ {1,2} of λ -term-graphs are closed under converse
functional bisimulation.
)
(iii) The class T1 ,1(λ
1 of λ -term-graphs is not closed under functional bisimulation.
)
(iv) The class T1 ,2(λ
2 of λ -term-graphs is not closed under functional bisimulation.
Proof.

For showing (i), let ∆ be one of the signatures Σλ0, j . Consider the following term graphs over ∆:
@

@

G2 :

λ

λ

0

0

G1 :

λ

@

G0 :

λ

λ
0

0

Note that G2 represents the syntax tree of the nameless de-Bruijn-index notation (λ 0) (λ 0) for the
λ -term (λ x.x) (λ x.x). Then it holds: G2 → G1 → G0 . But while G2 and G0 admit correct abstractionprefix functions over ∆ (nestedness of the implicitly defined scopes, here shaded), and consequently are
λ -term-graphs over ∆, this is not the case for G1 (overlapping scopes). Hence the class of λ -term-graphs
over ∆ is closed neither under functional bisimulation nor under converse functional bisimulation.
For showing (ii), let ∆ be one of the signatures Σλ1 and Σλ1, j . Consider the term graphs over ∆:
@

G′1 :

λ

G′0 :

λ

0

G′1

G′0 .

@
λ
0

G′0

→
Then it holds:
But while
admits a correct abstraction-prefix function, and therefore is
a λ -term-graph, over ∆, this is not the case for G′1 (due to overlapping scopes). Hence the class of
λ -term-graphs over ∆ is not closed under converse functional bisimulation.
For showing (iii), consider the following term graphs over Σλ1,1 :
λ

G′′1 :

λ

@

G′′0 :

@

λ

λ

λ

λ

S

S

S

0

0

0

70

Term Graph Representations for Cyclic Lambda-Terms

Then it holds that G′′1 → G′′0 . However, while G′′1 admits a correct abstraction-prefix function, and hence
is a λ -term-graph over Σλ1,1 , this is not the case for G′′0 (due to overlapping scopes). Therefore the class
of λ -term-graphs over Σλ1,1 is not closed under functional bisimulation.
For showing (iv), consider the following term graphs over Σλ1,2 :
@

@

G′′′
1

G′′′
0 :

@
0

λ

λ

0

0

G′′′
0 .

λ

λ

λ

λ

G′′′
1 :

@
0

λ
0

G′′′
1

→
Then it holds that
However, while
admits a correct abstraction-prefix function, and
hence is a λ -term-graph over Σλ1,2 , this is not the case for G′′′
0 (overlapping scopes). Therefore the class
λ
of λ -term-graphs over Σ1,2 is not closed under functional bisimulation. The scopes defined implicitly by
these graphs are larger than necessary: they do not exhibit ‘eager scope closure’, see Section 7.
◻
As an easy consequence of Prop. 25, and of Prop. 26, (i) and (ii), together with the examples used in
the proof, we obtain the following two propositions.
Proposition 27 Let i ∈ {0,1}. None of the classes Hiλ of λ -ho-term-graphs, or Hi(λ ) of λ -ap-ho-termgraphs are closed under bisimulations on the underlying term graphs.
Proposition 28 The following statements hold:
(i) Neither the class H0λ nor the class H0(λ ) is closed under functional bisimulations, or under converse functional bisimulations, on the underlying term graphs.
(ii) Neither the class H1λ of λ -ho-term-graphs nor the class H1(λ ) of λ -ap-ho-term-graphs is closed
under converse functional bisimulations on underlying term graphs.
Note that Prop. 28, (i) is a strengthening of the statement of Prop. 15 earlier.

7

Closed under functional bisimulation

The negative results gathered in the last section might seem to show our enterprise in a quite poor state:
For the classes of λ -term-graphs we introduced, Prop. 26 only leaves open the possibility that the class
T1(λ ) is closed under functional bisimulation. Actually, T1(λ ) is closed (we do not prove this here), but
that does not help us any further, because the correspondences in Thm. 22 do not apply to this class,
and worse still, Prop. 16 rules out simple correspondences for T1(λ ) . So in this case we are left without
the satisfying correspondences to λ -ho-term-graphs and λ -ap-ho-term-graphs that yet exist for the other
classes of λ -term-graphs, but which in their turn are not closed under functional bisimulation.
(λ )
But in this section we establish that the class T1,2
is very useful after all: its restriction to term
graphs with eager application of scope closure is in fact closed under functional bisimulation.
(λ )
The reason for the non-closedness of T1,2
under functional bisimulation consists in the fact that
λ
λ -term-graphs over Σ1,2 do not necessarily exhibit ‘eager scope closure’: for example in the term graph
G′′′
1 from the proof of Prop. 26, (iv), the scopes of the two topmost abstractions are not closed on the
paths to variable occurrences belonging to the bottommost abstractions. For the following variation G̃1

C. Grabmayer & J. Rochel

71

of G1 with eager scope closure the problem disappears:

@

G̃1 :
0

@

λ

λ

@

S
S

λ

λ

0

G̃0 :

λ

λ

@

S

0

S
λ

0

0

Its bisimulation collapse G̃0 has again a correct abstraction-prefix function and hence is a λ -term-graph.
Definition 29 (eager-scope, and fully back-linked, λ -term-graphs) Let G = ⟨V,lab,args,r⟩ be a λ -termgraph over Σλ1, j for j ∈ {1,2} with abstraction-prefix function P ∶ V → V ∗ . We call G an eager-scope
λ -term-graph (over Σλ1, j ) if it holds:
∀w,v ∈ V . ∀p ∈ V ∗. P(w) = pv ⇒ ∃n ∈ N∃w1 ,...,wn−1 ∈ V .
w ↣ w1 ↣ ... ↣ wn−1 ↣0 v
∧ wn−1 ∈ V(0) ∧ ∀1 ≤ i ≤ n − 1. P(w) ≤ P(wi ) ,
that is, if for every vertex w in G with a non-empty abstraction-prefix P(w) that ends with v there exists
a path from w to v in G via vertices with abstraction-prefixes that extend P(w) and finally a variableoccurrence vertex before reaching v. By eag Ti,(λj ) we denote the subclass of Ti,(λj ) consisting of all eagerscope-λ -term-graphs. And we say that G is fully back-linked if it holds:
∀w,v ∈ V1 . ∀p ∈ V1∗. P(w) = pv ⇒ w ↣∗ v ,

(6)

that is, if for all vertices w of G1 , the last vertex v in the abstraction-prefix of w is reachable from v. Note
that eager-scope implies fully back-linkedness for λ -term-graphs.
(λ )
Lemma 30 Let G be a fully back-linked λ -term-graph in T1,2
with vertex set V , and let P be its ab′
λ
straction-prefix function. Let G be a term graph over Σ1,2 (thus in T1,2 ) such that G →h G′ . Then it holds:

∀v1 ,v2 ∈ V . h(v1 ) = h(v2 ) ⇒ h̄(P(v1 )) = h̄(P(v2 ))

(7)

where h̄ is the homomorphic extension of h to words over V .
Proof (Idea). Let G1 , G2 be as assumed in the lemma, and let h be a homomorphism that witnesses
G1 →h G2 . We will use the following distance parameter for vertices of G1 : Let, for all w ∈ V1 , dλ ,P (w)
be either 0 if P(w) is empty, or otherwise the minimum length of a path in G1 from w to the last vertex
in the abstraction-prefix P(w). Thus due to (6), dλ ,P (w) ∈ N for all vertices w of G1 . Now (7) can be
proved by induction on max{dλ ,P (v1 ),dλ ,P (v2 )} with a subinduction on max{∣P(v1 )∣,∣P(v2 )∣}.
◻
This lemma is the crucial stepping stone for the proof of the following theorem.
Theorem 31 (preservation of λ -term-graphs over Σλ1,2 under homomorphism) Let G and G′ be term
(λ )
graphs over Σλ1,2 such that G is a λ -term-graph in T1,2
, and G →h G′ holds for a homomorphism h.
(λ )
If G is fully back-linked, then also G′ is a λ -term-graph in T1,2
, which is fully back-linked. If, in
′
addition, G is an eager-scope λ -term-graph, then so is G .

72

Term Graph Representations for Cyclic Lambda-Terms

(λ )
Corollary 32 The subclass eag T1,2
of the class T1,2 that consists of all eager-scope λ -term-graphs in
(λ )
T1,2 is closed under functional bisimulation.

Since the counterexample in the proof of Prop. 26, (iii) used eager-scope λ -term-graphs, it rules out
(λ )
(λ )
(λ )
a statement analogous to Cor. 32 for the class T1,1
. Such a statement for T0,1
and T0,2
is ruled out
similarly, with respect to an appropriate definition of ‘eager-scope’ for λ -term-graphs over Σλ0,1 and Σλ0,2 .
Corollary 33 Let h be a functional bisimulation from an eager-scope λ -term-graph G over Σλ1,2 to a term
graph G′ over Σλ1,2 (h witnesses G →h G′ ). Then G′ is an eager-scope λ -term-graph as well, and h extends
to a functional bisimulation from G1,2 (G) to G1,2 (G′ ) (thus h also witnesses G1,2 (G) →h G1,2 (G′ )).

8

Conclusion

We first defined higher-order term graph representations for cyclic λ -terms:
• λ -ho-term-graphs in Hiλ , an adaptation of Blom’s ‘higher-order term graphs’ [4], which possess a
scope function that maps every abstraction vertex v to the set of vertices that are in the scope of v.
• λ -ap-ho-term-graphs in Hi(λ ) , which instead of a scope function carry an abstraction-prefix function that assigns to every vertex w information about the scoping structure relevant for w. Abstraction prefixes are closely related to the notion of ‘generated subterms’ for λ -terms [6]. The
correctness conditions here are simpler and more intuitive than for λ -ho-term-graphs.
These classes are defined for i ∈ {0,1}, according to whether variable occurrences have back-links to
abstractions (for i = 1) or not (for i = 0). Our main statements about these classes are:
• a bijective correspondence between Hiλ and Hi(λ ) via mappings Ai and Bi that preserve and reflect
the sharing order (Thm. 10);
• the naive approach to implementing homomorphisms on theses classes (ignoring all scoping information and using only the underlying first-order term graphs) fails (Prop. 16).
The latter was the motivation to consider first-order term graph implementations with scope delimiters:
• λ -term-graphs in Ti,(λj ) (with i ∈ {0,1} and j = 2 or j = 1 for scope delimiter vertices with or without
back-links, respectively), which are first-order term graphs without a higher-order concept, but for
which correctness conditions are formulated via the existence of an abstraction-prefix function.
The most important results linking these classes with λ -ap-ho-term-graphs are:
• an ‘almost bijective’ correspondence between the classes Hi(λ ) and Ti,(λj ) via mappings Gi, j and
Gi, j that preserve and reflect the sharing order (Thm. 22);
(λ )
(λ )
• the subclass eag T1,2
of eager-scope λ -term-graphs in T1,2
is closed under homomorphism (Cor. 32).
The correspondences together with the closedness result allow us to derive methods to handle homomorphisms between eager higher-order term graphs in H1λ and H1(λ ) in a straightforward manner by
(λ )
implementing them via homomorphisms between first-order term graphs in T1,2
.
eag

H1λ

A1

B1

eag

H1(λ )

G1,2
eag

G1,2
(λ )
T1,2

G0

h

G0′
B1

A1
G1

h

G1′
G1,2

G1,2
G

h′

G′

(λ )
For example, the property that a unique maximally shared form exists for λ -term-graphs in T1,2
(which

C. Grabmayer & J. Rochel

73

can be computed as the bisimulation collapse that is guaranteed to exist for first-order term graphs) can
now be transferred to eager-scope λ -ap-ho-term-graphs and λ -ho-term-graphs via the correspondence
(λ )
mappings (see the diagram above). For this to hold it is crucial that eag T1,2
is closed under homomorphism, and that the correspondence mappings preserve and reflect the sharing order. The maximally
shared form maxeag Hλ (G) of an eager λ -ho-term-graph G can furthermore be computed as:
1

maxeag Hλ (G) = (B1 ○ G1,2 ○ maxeag T1,2
(λ ) ○ G1,2 ○ A1 )(G).
1

(λ )
where maxeag T1,2
to its bisimulation collapse. For obtaining maxeag T1,2
(λ ) maps every λ -term-graph in T1,2
(λ )
fast algorithms for computing the bisimulation collapse of first-order term graphs can be utilized.
While we have explained this result here only for term graphs with eager scope-closure, the approach
can be generalized to non-eager-scope term graphs. To this end scope delimiters have to be placed also
underneath variable vertices. Then variable occurrences do not implicitly close all open extended scopes,
but every extended scope that is open at some position must be closed explicitly by scope delimiters on
all (maximal) paths from that position. The resulting graphs are fully back-linked, and then Thm. 31
guarantees that the arising class of λ -term-graphs is again closed under homomorphism.
For our original intent of getting a grip on maximal subterm sharing in the λ -calculus with letrec or
µ, however, only eager scope-closure is practically relevant, since it facilitates a higher degree of sharing.
Ultimately we expect that these results allow us to develop solid formalizations and methods for
subterm sharing in higher order languages with sharing constructs.

Acknowledgement. We want to thank the reviewers for their helpful comments, and for pointing out
a number of inaccurate details in the submission that we have remedied for obtaining this version.

References
[1] Zena M. Ariola & Stefan Blom (1997): Cyclic Lambda Calculi. In Martin Abadi & Takayasu Ito, editors:
Proceedings of TACS’97, Sendai, Japan, September 23–26, 1997. LNCS 1281, Springer Berlin / Heidelberg,
pp. 77–106, doi:10.1007/BFb0014548.
[2] Zena M. Ariola & Jan Willem Klop (1994): Cyclic Lambda Graph Rewriting. In: Proceedings of the Symposium on Logic in Computer Science (LICS) 1994. pp. 416 –425, doi:10.1109/LICS.1994.316066.
[3] Zena M. Ariola & Jan Willem Klop (1996): Equational Term Graph Rewriting. Fundamenta Informaticae
26(3), pp. 207–240, doi:10.3233/FI-1996-263401.
[4] Stefan Blom (2001): Term Graph Rewriting, Syntax and Semantics. Ph.D. thesis, Vrije Universiteit Amsterdam.
[5] N. G. de Bruijn (1972): Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula
Manipulation, with Application to the Church-Rosser Theorem. Indagationes Mathematicae 34, pp. 381–392,
doi:10.1016/1385-7258(72)90034-0.
[6] Clemens Grabmayer & Jan Rochel (2012): Expressibility in the Lambda-Calculus with Letrec. Technical
Report arXiv:1208.2383, http://arxiv.org. http://arxiv.org/abs/1208.2383.
[7] Dimitri Hendriks & Vincent van Oostrom (2003): λ. In F. Baader, editor: Proceedings CADE-19. Lecture
Notes in Artificial Intelligence 2741, Springer–Verlag, pp. 136–150.
[8] Simon Peyton Jones (1987): The Implementation of Functional Programming Languages. Prentice-Hall, Inc.
[9] Vincent van Oostrom, Kees-Jan van de Looij & Marijn Zwitserlood (2004): Lambdascope. Extended Abstract
for the Workshop on Algebra and Logic on Programming Systems (ALPS), Kyoto, April 10th 2004. http:
//www.phil.uu.nl/~oostrom/publication/pdf/lambdascope.pdf.
[10] Terese (2003): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55, Cambridge
University Press.

