BRICS RS-94-4 Klarlund & Schwartzbach: Graphs and Decidable Transductions based on Edge Constraints

BRICS

Basic Research in Computer Science

Graphs and Decidable Transductions based on Edge Constraints

Nils Klarlund Michael I. Schwartzbach

BRICS Report Series RS-94-4 ISSN 0909-0878 February 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

Graphs and Decidable Transductions based on Edge Constraints

(Extended Abstract)

Nils Klarlund^{∗} Michael I. Schwartzbach
BRICS^{†}

Department of Computer Science, University of Aarhus,

Ny Munkegade, DK-8000 Aarhus, Denmark

            {klarlund,mis}@daimi.aau.dk

Abstract

We give examples to show that not even c-edNCE, the most general known notion of context-free graph grammar, is suited for the specification of some common data structures.

To overcome this problem, we use monadic second-order logic and introduce edge constraints as a new means of specifying a large class of graph families. Our notion stems from a natural dichotomy found in programming practice between ordinary pointers forming spanning trees and auxiliary pointers cutting across.

Our main result is that for certain transformations of graphs definable in monadic second-order logic, the question of whether a graph family given by a specification A is mapped to a family given by a specification B is decidable. Thus a decidable Hoare logic arises.

1 Introduction

Graphs are complicated objects to describe. Thus various grammars and logics have emerged for their representation, see the chapter by Courcelle [1]. The monadic second-order logic of graphs (M2L-G) allows a very large class of graph families to be described. The first-order terms of the logic denote nodes. The second-order terms denote sets of nodes. Nodes and edges are related by built-in predicates. The M2L-G formalism is very well-suited for describing properties of some common data structures, see our earlier paper [5].

∗The author is supported by a fellowship from the Danish Research Council.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Some authors consider logics that comprise quantification over edges. For these logics, a fundamental result is that a family of graphs allows a decidable M2L if and only if the family is specified by a hyperedgereplacement grammar [2]. Such grammars constitute a natural generalization of context-free grammars for string languages.

An even larger class of context-free grammars is known as c-edNCE. The monadic logic of graph families thus given is undecidable, but certain other questions, such a non-emptiness of a specification, are decidable, see [4].

For programming purposes, we would like to describe common data structures found in the store such as trees and doubly-linked lists. Indeed, this is possible within the framework of decidable formalisms as e.g. hyperedge-replacement grammars. Many other graph shapes are not representable. But whatever specification formalism we choose, we should be able to represent trees with additional, unconstrained pointers—reflecting a situation where almost nothing is said about the store, as is the case with type systems of most imperative programming languages.

We show in this paper that not even c-edNCE grammars are able to define such families of graphs.

To reason about data structures, it is vital to model the execution of programs. Therefore, we must formulate ways of transforming graphs corresponding to statements in a programming language. For program correctness, we would use Hoare logic to show that the store transformations leave the graph specifications satisfied.

In this paper we consider restricted graph transformations, called transductions, which are based on the method of semantic interpretation [7] and studied in [3]. Given logical graph specifications A and B and a transduction, we address the problem of verifying what we call transductional correctness: for any graph satisfying A, any graph resulting from the transduction satisfies B. This informal definition omits the difficulty of having shared logical variables in A and B—a problem that is explicitly solved in this paper. Decidability of transductional correctness amounts to decidability of the corresponding Hoare logic.

Contributions of this paper

We devise a class of graph specifications

• that may model loosely restrained edges, and

• for which transductional correctness is decidable.

Our graphs consist of ordinary edges constituting an underlying spanning forest, called the backbone, and auxiliary edges cutting across the backbone.

These notions stem from a natural dichotomy found in programming practice between ordinary pointers forming spanning trees and auxiliary pointers cutting across as used for short-cuts (such as extra links pointing backward to previous elements) or for indexing into other data structures using unrestrained pointers.

Our graph specifications are based on combining the full M2L in form of a backbone formula for specifying ordinary edges together with a special M2L syntax, called edge constraints, for specifying auxiliary edges. The formulas in an edge constraint involve only the backbone to specify the sources and destinations of auxiliary edges. The resulting class of graph families thus definable is called EC. We show that the classes c-edNCE and EC are incomparable.

We next introduce a class of transductions. They are formulated in M2L and are similar to the ones considered in [3]. We use extra logical variables to model edges that are followed, deleted, or added during the transformation of the graph.

Our main result is that the transduction problem is decidable for EC. This result is based on a rather complicated encoding of the effects of the transduction within M2L on the backbone alone. The obstacle that we overcome is that it is impossible to directly represent all auxiliary edges in the logic of the backbone. The key idea is to distinguish between the bounded number of auxiliary edges that are explicitly manipulated by the transduction and the others, which are represented by a universal quantification in the logic.

Our other work

In an accompanying paper [6], we outline a typing system for data structures and define a programming language. The typing information is expressed in a logic on the underlying recursive data types. The programming language provides assignment, dereference, allocation, deallocation, and limited forms of iterations based on regular walks. We show in [6] that the operational semantics is captured by transductions and that by the results in this paper the resulting Hoare logic on data structures is decidable.

In [5], we also used monadic second-order logic to reason about data structures as graphs, but we restricted ourselves to trees with auxiliary edges that are functionally determined by the backbone in terms of regular walks.

2 Rooted Graphs

A graph alphabet Λ consists of a finite set Λ^{V} of node labels (which include a special label spare) and a finite set Λ^{E} of edge labels. Usually, we denote a node label by v. There are two kinds of edge labels: ordinary and auxiliary. Usually, an ordinary edge label is denoted f and an auxiliary edge label is denoted a. An edge label that is either ordinary or auxiliary is denoted n.

A rooted graph G over Λ consists of a finite set G^{V} of labeled nodes; a finite set G^{E} of labeled edges; and a finite set of node variables x, called roots, denoting nodes in GṪhe label of node v ∈ G^{V} is denoted G^{L}(v). Nodes are either ordinary or spare according to their label. An edge from v to w labeled n is denoted (v, n, w). For each v and n, there is at most one such edge. Loops are allowed. The edges of G are divided into ordinary and auxiliary ones according to their label. The node denoted by root x is written x^{G}.

The set of all graphs over Λ is denoted GR(Λ). An edge set E is a set of edges such that (v, n, w) ∈ E and (v, n, u) ∈ E implies w = u.

We sometimes view G as consisting of \overline{G}, called the backbone, which is all of G except for the auxiliary edges, and \begin{matrix}= \\ G \end{matrix}, which is the edge set of auxiliary edges in G. Thus, G may be written as (\overline{G}, \begin{matrix}= \\ G \end{matrix}).

The spare nodes model free memory cells in programming language applications. They are essential to allow addition and deletion of nodes by transductions.

Figure 1 shows a sketch of a rooted graph. The ordinary edges are drawn as solid arrows, whereas the auxiliary edges are dashed; spare

[figure: a; v; f; f; f; f_{1}; f_{2}; f_{2}; f_{1}; f; a; a; x_{1}; x_{2}; x_{3}]

Figure 1: A rooted graph.

nodes are black; the roots are called x_{1}, x_{2}, and x_{3}.

3 The Logic M2L-BB

The key to specifying data structures is the Monadic Second-Order of Backbones, abbreviated M2L-BB. First-order terms range over nodes in the graph. Second-order terms range over sets of nodes.

Syntax

Assume a graph alphabet Λ. The logic of rooted graphs over Λ is denoted M2L-BB(Λ). Its syntax is as follows.

Address terms A denote nodes in the graph.

A ::= x root src source dst destination α, β, … first-order variable

The terms src and dst are special variables used in certain assertions. Address set terms Σ denote sets of nodes.

Σ ::= ∅ empty set Σ_{1} ∪ Σ_{2} set union Σ_{1} \ Σ_{2} set difference S, T, … second-order variable Formulas Φ denote true or false.

Φ ::= A_{1} = A_{2} equality

A ∈ Σ set membership Σ_{1} ⊆ Σ_{2} set inclusion

A_{1} \underrightarrow{f} A_{2} successor relation, where f ∈ Λ^{E} is ordinary v?A test for node label, where v ∈ Λ^{V} ¬Φ negation Φ_{1} ∧ Φ_{2} conjunction ∃^{0}α : Φ first-order quantification over all nodes ∃^{0}S : Φ second-order quantification over all nodes

Note that the syntax does not allow references to auxiliary edges. We also use unmarked quantifiers that range only over ordinary nodes. They can be viewed as abbreviations according to the following.

∃α : Φ ≡ ∃^{∘}α : ¬spare?α ∧ Φ
∃S : Φ ≡ ∃^{∘}S : (¬∃^{∘}α : α ∈ S ∧ spare?α) ∧ Φ

We also assume abbreviations ∀, ⇒, ∨, etc.

Semantics

M2L-BB is interpreted relative to a backbone \overline{G}. The interpretation of x is given by \overline{G} as x\overline{G}. The constants dst and src are used as variables. The semantics of variables is formulated below by substitution for values in \overline{G}^{V}. A value v is interpreted as itself, i.e. v\overline{G} = v. A non-variable address set term Σ is interpreted as follows.

\begin{aligned}∅\overline{G} & = ∅ \\ (Σ_{1} ∪ Σ_{2})\overline{G} & = Σ\overline{G} ; 1 ∪ Σ\overline{G} ; 2 \\ (Σ_{1}\Σ_{2})\overline{G} & = Σ\overline{G} ; 1\Σ\overline{G} ; 2 \end{aligned}

The semantics of formulas is as follows.

\overline{G} ⊨ A_{1} = A_{2} if A\overline{G} ; 1 = A\overline{G} ; 2
\overline{G} ⊨ A ∈ Σ if A\overline{G} ∈ Σ\overline{G}
\overline{G} ⊨ Σ_{1} ⊆ Σ_{2} if Σ\overline{G} ; 1 ⊆ Σ\overline{G} ; 2
\overline{G} ⊨ A_{1} \underrightarrow{f} A_{2} if (A\overline{G} ; 1, f, A\overline{G} ; 2) ∈ \overline{G}^{E}
\overline{G} ⊨ v?A  if \overline{G}^{L}(A\overline{G}) = v
\overline{G} ⊨ ¬Φ  if not \overline{G} ⊨ Φ
\overline{G} ⊨ Φ_{1} ∧ Φ_{2} if \overline{G} ⊨ Φ_{1} and \overline{G} ⊨ Φ_{2}
\overline{G} ⊨ ∃^{∘}α : Φ if there is v ∈ \overline{G}^{V} such that \overline{G} ⊨ Φ(α ↦ v)
\overline{G} ⊨ ∃^{∘}S : Φ if there is V ⊆ \overline{G}^{V} such that \overline{G} ⊨ Φ(S ↦ V),

If Φ has free variables 𝔉 and \underline{𝔉} is an interpretation of these variables in \overline{G}^{V}, then

\overline{G}, \underline{𝔉} ⊨ Φ if \overline{G} ⊨ Φ(𝔉 ↦ \underline{𝔉}).

If \overline{G} ⊨ Φ holds for all \overline{G}, then we say that Φ is valid and we write ⊨ Φ. A graph G is tree-formed if

• all edges are between ordinary nodes; and

• the graph induced by ordinary nodes and ordinary edges is a directed forest such that each root is the value of some root variable.

Note that the graph depicted in Figure 1 is tree-formed.

Lemma 1 There is a formula Φ such that G is tree-formed if and only if G ⊨ Φ.

Proof Among other conditions, acyclicity and reachability can be encoded in M2L-BB. □

We say that Φ is tree-valid and we write ⊩ Φ if \overline{G} ⊨ Φ holds for all tree-formed \overline{G}.

Theorem 1 Validity is undecidable, but tree-validity is decidable.

Proof The first result follows from the undecidability of the first-order logic of finite graphs. The second result follows from the decidability of the monadic second-order logic of finite trees. □

Edge Constraints and Assertions

Constraints on auxiliary edges cannot just be formulas, since the logic refers only to ordinary edges. Instead, an edge constraint is of the form [σ \underrightarrow{a} δ], where σ is a formula involving src as a free variable, and δ is a formula with free variables src and dst. The edge constraint is valid for a given graph if whenever σ is valid with a node v in place of src, then there is an a-edge (which is unique by definition of a rooted graph) from v to some node w and δ is valid with v and w in place of src and dst. Note that the edge constraint does not describe any a-edges outside where σ holds.

Formally, let [σ \underrightarrow{a} δ] be an edge constraint with free variables 𝔉. We say that G and \underline{𝔉} satisfy [σ \underrightarrow{a} δ], and we write G, \underline{𝔉} ⊨ [σ \underrightarrow{a} δ] if:

for all v ∈ G^{V}, G, \underline{𝔉} ⊨ σ(src ↦ v) implies

for some (v, a, w) ∈ \begin{matrix}= \\ G \end{matrix}, G, \underline{𝔉} ⊨ δ(src ↦ v, dst ↦ w).

An assertion A = Φ[σ_{1} \underrightarrow{a_{1}} δ_{1}] … [σ_{n} \underrightarrow{a_{n}} δ_{n}] consists of a formula Φ, called the backbone formula, and a number of edge constraints [σ_{i} \underrightarrow{a_{i}} δ_{i}]. These components are connected through free variables, which are implictly existentially quantified.

Let 𝔉 be a list containing the free variables and let \underline{𝔉} be a value assignment to these variables. An assertion A is satisfied in G with \underline{𝔉}, and we write G, \underline{𝔉} ⊨ A, if \overline{G}, \underline{𝔉} ⊨ Φ and for all i, G, \underline{𝔉} ⊨ [σ_{i} \underrightarrow{a_{i}} δ_{i}].

An assertion A specifies the language of graphs

\{G | G is tree-formed and for some \underline{𝔉}, G, \underline{𝔉} ⊨ A\}

The class of such graph languages is called EC.

Example

Consider the common data structure, shown in Figure 2, of linked lists with a head node that points both to the first element of the list and to some designated element. The f- and n-edges are ordinary; the s-edge is auxiliary. The corresponding backbone formula contains these clauses.

H?x The head node has label H

∃α : x \underrightarrow{f} α and an outgoing f-edge;

[figure: H; x; L; L; L; L; s; f; n; n; n]

Figure 2: A list structure

∀β, β′ : β \underrightarrow{f} β′ ⇒ β = x no other node has an outgoing f-edge; ∀β : ¬β =x ⇒ L?β all other nodes have label L; ∀β, β′ : β \underrightarrow{n} β′ ⇒ β ≠ x the head node has no outgoing n-edge; L?γ and there is a designated L-node...

Note that we quantify only over ordinary nodes. There is only a single edge constraint.

[H?src \underrightarrow{s} γ =dst] that is the destination of the s-edge.

Here the free variable γ connects the backbone formula and the edge constraint. In conjunction with the general requirement of tree-formedness, this assertion describes backbones that are lists with a head node. Note that the assertion does not eliminate extraneous s-edges from nodes other than the one marked H. In a programming language application these are avoided through elementary type-checking of the transductions that build graphs [6].

4 Relations to Other Formalisms

It is interesting to compare the expressive power of this graph specification formalism with those of other proposals. In particular we show in this section that the set of trees with unrestrained auxiliary edges is not representable as a context-free graph grammar.

We look at the most general class known of context-free graphs languages: c-edNCE, which stands for “confluent edge and node labeled, directed graphs given by Neighborhood Controlled Embedding.” The grammars that define such languages are complicated. Instead we shall use a result by Engelfriet that these languages are exactly the images of trees under functions definable in monadic second-order logic [4]. The following definition is from [4] (but changed as to allow loops in graphs):

Let Λ_{1} and Λ_{2} be alphabets. An M2L-definable function f : GR(Λ_{1}) → GR(Λ_{2}) is given by the following formulas in M2L-BB(Λ_{1}):

• a closed formula ϕ_{dom}, called the domain formula;

• for every v ∈ Λ_{2}^{V}, a formula ϕv, called a node formula, with one free variable src; and

• for every n ∈ Λ_{2}^{E}, a formula ϕn, called an edge formula, with two free variables src and dst.

The domain of f is {G ∈ GR(Λ_{1}) | G ⊨ ϕ_{dom}}. For every G ∈ dom(f), the graph G′ = f(G) ∈ GR(Λ_{2}) is given by

G′^{V} = {v ∈ G^{V} | there is exactly one v ∈ Λ_{1}^{V}such that G ⊨ ϕv(src ↦ v)}
G′^{E} = {(v, n, w) | v, w ∈ G^{V}and G ⊨ ϕn(src ↦ v, dst ↦ w)}.

(For simplicity, we ignore roots in this section.)

Theorem 2 [4] A language of graphs is c-edNCE if and only if it is the image of an M2L-definable function f : GR(Λ_{1}) → GR(Λ_{2}) applied to the set of directed trees over Λ_{1}.

Such a language is then said to be f-definable.

Theorem 3 [4] It is decidable whether a function f defines a finite language of graphs.

Lemma 2 [4] The class of M2L-definable functions is closed under composition.

Now fix Λ_{T}^{V} = {v}, Λ_{T}^{E} = {f_{1}, f_{2}, a}. A tree with equi-level edges is a graph G over Λ_{T} such that G restricted to f-edges is a directed tree and such that (v, a, w) ∈ G^{E} if and only if w is the left-most node to the right of v at the same level as v, as shown in Figure 3.

Lemma 3 The set of trees over Λ_{T} with equi-level edges is not c-edNCE.

Proof Suppose for a contradiction that the set is c-edNCE by means of an M2L-definable function f. Then there would be a uniform way of obtaining an M2L-definable function f_{i} whose graph language represents all finite sequences of configurations that TM (Turing Machine) i may produce with an empty input tape. In fact we may choose Λ^{V} = {0, 1, #}

[figure: a; f_{1}; f_{2}; f_{1}; f_{2}; f_{1}; f_{2}; f_{1}; f_{2}; a; a; a]

Figure 3: A tree with equi-level edges.

and construct f′_{i} such that it maps trees with equi-level edges into trees whose Λ^{V} labels at level k encode the configuration of TM i after the k’th step (details are omitted). By Lemma 2, the set of graphs representing finite configuration sequences is then definable by a function f_{i} = f′_{i} ∘ f. But then the Halting Problem would be decidable by Theorem 3, which is a contradiction. □

Lemma 4 The set of trees over Λ_{T} with unrestrained a-edges is not c-edNCE.

Proof If it was we could use Lemmas 2 and 3 to show that also the set of trees with equi-level edges is c-edNCE. (We would construct a domain formula checking, among other things, that whenever (v, a, w) and (v′, a, w′) are edges and v′ is a child of v, then w′ is a child of w.) □

Theorem 4 c-edNCE and EC are incomparable.

Proof EC ⊈ c-edNCE: The set of trees with unrestrained a-edges is certainly EC, but not c-edNCE by Lemma 4.

c-edNCE ⊈ EC: The set of cyclic graphs over singleton node and edge alphabets is c-edNCE, but not EC (in fact, since the edge label determines whether an edge is ordinary or auxiliary, only list-like structures and certain degenerate structures can be described with singleton edge alphabets). □

5 Transductions

We are interested in graph transformations that model pointer manipulations in programs. These can be specified through a transduction, which is defined to be of the form T =< L, E, ρ >. The component L is a list of labeled entries. An entry t defines one or two first-order variables, called transduction variables, according to its label as follows.

• add-n: this indicates the creation of an n-edge between two nodes denoted by first-order terms src(t) and dst(t); an existing n-edge from the source is deleted.

• del-n: this indicates the deletion of the n-edge whose origin is denoted by the first-order term src(t).

• foll-a: this indicates the existence of an a-edge which has been followed between two cells denoted by first-order terms src(t) and dst(t); this makes for an explicit representation of auxiliary edges that are followed and, therefore, known to exist in the original graph.

• v: this indicates that a node denoted by the first-order logical variable src(t) is marked with label v (which may be spare); if an ordinary node is marked spare, then its outgoing and incoming edges are deleted.

The component E is an environment, which maps root variables to address terms denoting their values. The component ρ is a formula which must hold in order for the free variables in L and E to denote a transformation. The formula ρ may contain other transduction variables than those defined by L. Together they are designated μ⃗.

The formula ρ must ensure that the entries are consistent with each other. Thus if a graph G and a value assignment \underline{μ⃗} are such that G, \underline{μ⃗} ⊨ ρ, then some examples of technical relationsships that most hold are:

• given any v and a, there are at most one foll-a entry t such that G, \underline{μ⃗} ⊨ src(t) = v; and

• given any (v, a, w) that is marked by a del-a entry before any add-a entry, there is a foll-a entry, which makes explicit the assumption that (v, a, w) is an edge in G.

6 Predicate Transformers

Each transduction T determines a predicate transformer Tr_{T}. A formula Φ is translated into Tr_{T} Φ according to the following rules.

Tr_{T} (x)  = T .E(x)
Tr_{T} (α)  = α
Tr_{T} (A_{1} = A_{2}) = Tr_{T} (A_{1}) = Tr_{T} (A_{2})

Tr_{T} (α \underrightarrow{f} β) = \{ \begin{matrix}β = dst(t) & if t is an add-f entry in T .L, α = src(t), t is the last such en- try, and no later spare entry t′ is such that src(t′) ∈ \{α, β\} and no later del-f entry t′ is such that src(t′) = α \\ false & if there is a spare en- try  t with src(t) ∈ \{α, β\} or there is a del-f entry t with src(t) = α, and no later add-f entry t′ is such that src(t′) = α\} \\ α \underrightarrow{f} β & otherwise \end{matrix}

Tr_{T} (v?α)  = \{ \begin{matrix}true & if there is an v-entry t in T .L such that src(t) = α and no later v′-entry t′ is such that src(t′) = α \\ v?α & otherwise \end{matrix}
Tr_{T} (A ∈ Σ) = Tr_{T} (A) ∈ Σ
Tr_{T} (Σ_{1} ⊆ Σ_{2}) = Σ_{1} ⊆ Σ_{2}
Tr_{T} (¬Φ)  = ¬Tr_{T} Φ
Tr_{T} (Φ_{1} ∧ Φ_{2}) = Tr_{T} (Φ_{1}) ∧ Tr_{L}(Φ_{2})
Tr_{T} (∃^{∘}α : Φ) = ∃^{∘}α : Tr_{T} Φ
Tr_{T} (∃^{∘}S : Φ) = ∃^{∘}S : Tr_{T} Φ

The transformed backbone, denoted BB_{T} (\overline{G}, \underline{μ⃗}), according to T on \overline{G} with transduction values \underline{μ⃗} is the graph \overline{G}′ defined as follows.

• \overline{G}^{′V} = \overline{G}^{V};

• (v, f, w) ∈ \overline{G}^{′E} iff \overline{G}, \underline{μ⃗} ⊨ Tr_{T} (v \underrightarrow{f} w);

• \overline{G}^{′L}(v) = v iff \overline{G}, \underline{μ⃗} ⊨ Tr_{T} (v?v); and

• x^{\overline{G}′} is the node v such that \overline{G}, \underline{μ⃗} ⊨ v = Tr_{T} (T .E(x)).

Lemma 5 (Faithfulness) Let \overline{G}′ = BB_{T} (\overline{G}, \underline{μ⃗}) and let \underline{𝔉} be a value assignment to the free variables of Φ. Then,

\overline{G}′, \underline{𝔉} ⊨ Φ

if and only if

\overline{G}, \underline{𝔉}, \underline{μ⃗} ⊨ Tr_{T} Φ

Proof (Sketch) By a straightforward structural induction. □

We say that \overline{G}, μ⃗, and T determine a transformation. In addition to the transformed backbone, the transformation also determines:

• Foll_{T} -a(\overline{G}, \underline{μ⃗}), the set of a-edges in the old graph G that were followed;

• Del_{T} -a(\overline{G}, \underline{μ⃗}), the set of a-edges in the old graph G that were both followed and deleted; and

• Add_{T} -a(\overline{G}, \underline{μ⃗}), the set of a-edges in the new graph G′ that were added.

To specify Foll_{T} -a(\overline{G}, \underline{μ⃗}), we define a predicate Foll_{T} -a with free variables src and dst expressing that an a-edge from src to dst was followed. Informally,

Foll_{T} -a ≡ “for some foll-a entry in T .L, src = src(t) and dst = dst(t),”

which can be encoded as a formula. Now,

Foll_{T} -a(\overline{G}, \underline{μ⃗}) = \{(v, a, w) | \overline{G}, \underline{μ⃗}, src ↦ v, dst ↦ w ⊨ Foll_{T} -a\}.

Similarly, we define the two other sets by defining predicates Del_{T} -a and Add_{T} -a:

Del_{T} -a ≡ “Foll_{T} -a and there is some spare entry with src = src(t) or dst = src(t), or some del-a or add-a entry t with src = src(t).”

Add_{T} -a ≡ “if there is an add-a entry t such that src(t) = src and dst(t) = dst, and no later entries delete this edge.”

Lemma 6 Del_{T} -a(\overline{G}, \underline{μ⃗}) ⊆ Foll_{T} -a(\overline{G}, \underline{μ⃗}) if G, \underline{μ⃗} ⊨ ρ.

Proof By the definitions and imposed technical relationships. □

The transformation relation induced by T is:

G ⟶_{T} G′

if and only if

for some \underline{μ⃗} :

\overline{G}, \underline{μ⃗} ⊧ T .ρ,

Foll-a_{T} (\overline{G}, \underline{μ⃗}) ⊆ \begin{matrix}= \\ G \end{matrix},

\overline{G}′ = BB_{T} (\overline{G}, \underline{μ⃗}), and

\begin{matrix}= \\ G \end{matrix}′ = (\begin{matrix}= \\ G \end{matrix}\Del-a_{T} (\overline{G}, \underline{μ⃗})) ∪ Add-a_{T} (\overline{G}, \underline{μ⃗})

Example (continued)

Consider the linked list with a designated element from Section 4. A common transduction on such structures is the insertion of an new element just before the head. This is realized by the following transduction.

L: L(μ′).del-f(x, μ).add-f(x, μ′).add-n(μ′, μ)

E: x ↦ x

ρ: x \underrightarrow{f} μ ∧ spare?μ′

Notice how this closely mimics the code that one would write in a conventional programming language. The expressive power of transductions goes beyond mere straight-line code, since regular control structures can be encoded in formulas [5].

7 Transductional Correctness

Let 𝔄 be the free variables in the assertion A and let 𝔅 be the free variables in the assertion B that are not already free in A. The problem of transductional correctness is:

Given assertions A, B, and a transduction T . Does it hold for all G, G′, and \underline{𝔄} that if G is tree-formed and satisfies A with \underline{𝔄}, and if G ⟶_{T} G′, then G′ is tree-formed and satisfies B for some \underline{𝔅}?

Since tree-formedness by Lemma 1 can be encoded as a backbone formula, we can without loss of generality rephrase the question as follows. We say that the triple A{T }B is tree-valid, and write ⊩ A{T }B, if:

for all tree-formed G, all G′ , and all \underline{𝔄}, G, \underline{𝔄} ⊨ A and G ⟶_{T} G′ implies there is \underline{𝔅} such that G′, \underline{𝔅} ⊨ B

Note that triple tree-validity concerns only transformations of tree-formed graphs.

Our main result is to demonstrate that tree triple validity can be encoded in M2L-BB. For simplicity we assume in what follows that an assertion now contains only one edge constraint, and that A = Φ[σ \underrightarrow{a} δ] and B = Φ′[σ′ \underrightarrow{a} δ′]. Then we say that triple A\{T \}B is provable and write ⊢ A{T }B if

⊩ ∀^{∘}𝔄 : ∀^{∘}μ⃗ :

(Φ ∧ ρ ∧ ∀^{∘}src∃^{∘}dst : (σ ⇒ (δ ∧ (¬Foll_{T} ⇒ (∀^{∘}dst : ¬Foll_{T}))))

⇒ ∃^{∘}𝔅 : (Tr_{T} Φ′

∧ ∀^{∘}src : Tr_{T} σ′ ⇒
((∃^{∘}dst : Add_{T} ∧ Tr_{T} δ′)
∨(∃^{∘}dst : Foll_{T} ∧ ¬Del_{T} ∧ Tr_{T} δ′)

∨(σ ∧ ∀^{∘}dst : ¬Add_{T} ∧ ¬Foll_{T} ∧ (δ ⇒ Tr_{T} δ′))))

8 Soundness, Completeness, and Decidability

Theorem 5 (Soundness) ⊢ A{T }B implies ⊩ A{T }B.

Proof Assume ⊢ A{T }B. (1) Fix a tree-formed G, a G′, and a value assignment \underline{𝔄} to the free variables 𝔄 of A such that G, \underline{𝔄} ⊨ A, and (2) G ⟶_{T} G′. (3) To establish ⊩ A\{T \}B, we only need to find a value assignment \underline{𝔅} to the remaining free variables 𝔅 such that G′, \underline{𝔄}, \underline{𝔅} ⊨ B. (4) Now by (3) and the definition of transductions, there is a value assignment \underline{μ⃗} to the transduction variables μ⃗ of T such that \overline{G}, \underline{μ⃗} ⊧ T .ρ (5)

Foll_{T} (\overline{S}, \underline{μ⃗}) ⊆ \begin{matrix}= \\ G \end{matrix}, (6)

\overline{G}′ = BB_{T} (\overline{G}, \underline{μ⃗}), and (7)

\begin{matrix}= \\ G \end{matrix}′ = (\begin{matrix}= \\ G \end{matrix}\Del_{T} (\overline{G}, \underline{μ⃗})) ∪ Add_{T} (\overline{G}, \underline{μ⃗}) (8)

In order to apply (1), we would like to show that

\overline{G}, \underline{𝔄}, \underline{μ⃗} ⊨ Φ ∧ ρ
∧ ∀^{∘}src∃^{∘}dst : σ ⇒ (δ ∧ (¬Foll_{T} ⇒ (∀^{∘}dst : ¬Foll_{T})))

(9)

holds. Now by (2), we have \overline{G}, \underline{𝔄} ⊨ Φ and \overline{G}, \underline{𝔄} ⊨ [σ →^{a} δ]. Thus it is sufficient to find for each v such that \overline{G}, \underline{𝔄}, src ↦ v ⊨ σ some w satisfying \overline{G}, \underline{𝔄}, src ↦ v, dst ↦ w ⊨ δ ∧ (¬Foll_{T} ⇒ (∀^{∘}dst : ¬Foll_{T})) (10) The w we choose is the one such that (v, a, w) ∈ \begin{matrix}= \\ G \end{matrix}. This w exists by virtue of (2) and the definition of edge constraint satisfaction. Moreover, \overline{G}, \underline{𝔄}, src ↦ v, dst ↦ w ⊨ δ. Thus in order to establish (10), it suffices to suppose that \overline{G}, \underline{𝔄}, src ↦ v, dst ↦ w ⊨ ¬Foll_{T} (11) and to prove that no u exists such that \overline{G}, \underline{𝔄}, src ↦ v, dst ↦ u ⊨ Foll_{T} . (12)

For a contradiction, assume that some u does satisfy (12). Then (v, a, u) ∈ Foll_{T} (\overline{G}, \underline{μ⃗}). But by (5), Foll_{T} (\overline{G}, \underline{μ⃗}) ⊆ \begin{matrix}= \\ G \end{matrix}, and thus u = w, which contradicts our supposition (11). It follows that (9) holds, and by (1) we then obtain a \underline{𝔅} such that

\overline{G}, \underline{𝔄}, \underline{𝔅}, \underline{μ⃗} ⊨ Tr_{T} Φ′ ∧ ∀^{∘}src : Tr_{T} σ′)
⇒ ((∃^{∘}dst : Add_{T} ∧ Tr_{T} δ′) ∨(∃^{∘}dst : Foll_{T} ∧ ¬Del_{T} ∧ Tr_{T} δ′) ∨(σ ∧ ∀^{∘}dst : ¬Add_{T} ∧ ¬Foll_{T} ∧ (δ ⇒ Tr_{T} δ′)))

(13)

holds. From (13) and Lemma 5 (Faithfulness), it follows that

\overline{G}, \underline{𝔄}, \underline{𝔅} ⊨ Φ′ (14)

We thus only need to show that also the edge constraint [σ′ \underrightarrow{a} δ′] holds. To do this, we consider v ∈ \begin{matrix}= \\ G \end{matrix}′ such that

\overline{G}, \underline{𝔄}, \underline{𝔅}, src ↦ v ⊨ σ′. (15)

We must then prove that there is w such that (v, a, w) ∈ \begin{matrix}= \\ G \end{matrix}′ and

\overline{G}, \underline{𝔄}, \underline{𝔅}, src ↦ v, dst ↦ w ⊨ δ′. (16)

Now by (15) and Lemma 5 (Faithfulness), we have

\overline{G}, \underline{𝔄}, \underline{𝔅}, \underline{μ⃗}, src ↦ v ⊨ Tr_{T} σ′. (17)

Discharging the hypothesis in (13) by means of (17) gives us three cases:

\overline{G}, \underline{𝔄}, \underline{𝔅}, \underline{μ⃗}, src ↦ v ⊨ ∃^{∘}dst : Add_{T} ∧ Tr_{T} δ′ (18)

\overline{G}, \underline{𝔄}, \underline{𝔅}, \underline{μ⃗}, src ↦ v ⊨ ∃^{∘}dst : Foll_{T} ∧ ¬Del_{T} ∧ Tr_{T} δ′ (19)

\overline{G}, \underline{𝔄}, \underline{𝔅}, \underline{μ⃗}, src ↦ v ⊨ σ ∧ ∀^{∘}dst : ¬Add_{T} ∧¬Foll_{T} ∧ (δ ⇒ Tr_{T} δ′)) (20)

In case (18) there is a w such that

\overline{G}, \underline{𝔄}, \underline{𝔅}, \underline{μ⃗}, src ↦ v, dst ↦ w ⊨ Add_{T} ∧ Tr_{T} δ′ (21)

By (8), (v, a, w) ∈ \begin{matrix}= \\ G \end{matrix}′, and by Lemma 5 (Faithfulness) (16) holds. Case (19) is handled by a similar argument. Finally, in Case (20) we have by Lemma 5 (Faithfulness) that \overline{G}, \underline{𝔄}, \underline{𝔅}, src ↦ v ⊨ σ and \overline{G}, \underline{𝔄}, \underline{𝔅}, src ↦ v, dst ↦ w ⊨ ¬Add_{T} ∧ ¬Foll_{T} ∧ (δ ⇒ Tr_{T} δ′), where w is the node such that (v, a, w) ∈ \begin{matrix}= \\ G \end{matrix} (this node exists by virtue of (2)). By (8), (20), and Lemma 6, we infer that (v, a, w) ∈ \begin{matrix}= \\ G \end{matrix}′ and by (2) that \overline{G}, \underline{𝔄}, \underline{𝔅}, src ↦ v, dst ↦ w ⊨ Tr_{T} δ. Thus \overline{G}, \underline{𝔄}, \underline{𝔅}, src ↦ v, dst ↦ w ⊨ Tr_{T} δ′ holds, whence (16) holds by Lemma 5 (Faithfulness). □

Theorem 6 (Completeness) ⊩ A{T }B implies ⊢ A{T }B.

Proof Proof can be found in full paper.

□

Theorem 7 Transductional correctness is decidable for EC.

Proof By Theorems 1, 5, and 6. □

References

[1] B. Courcelle. Graph rewriting: an algebraic and logic approach. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 193–242. Elsevier Science Publishers, 1990.

[2] B. Courcelle. The monadic second-order logic of graphs I. Recognizable sets of finite graphs. Information and computation, 85:12–75, 1990.

[3] B. Courcelle. Monadic second-order definable graph transductions. In J.C. Raoult, editor, CAAP ’92, Colloquium on Trees in Algebra and Programming, LNCS 581, pages 124–144. Springer Verlag, 1992.

[4] J. Engelfriet. A characterizarion of context-free NCE graph languages by monadic second-order logic on trees. In H. Ehrig, H.J. Kreowski, and G. Rozenberg, editors, Graph grammars and their applications to computer science, 4th International Workshop, LNCS 532, pages 311–327. Springer Verlag, 1990.

[5] N. Klarlund and M. Schwartzbach. Graph types. In Proc. 20th Symp. on Princ. of Prog. Lang., pages 196–205. ACM, 1993.

[6] N. Klarlund and M. Schwartzbach. Invariants as data types. Unpublished, 1993.

[7] M. Rabin. A simple method for undecidability proofs and some applications. In Logic, Methodology and Philosophy of Science II, pages 58–68. North-Holland, 1965.

Recent Publications in the BRICS Report Series

RS-94-1 Glynn Winskel. Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk. February 1994, 8 pp.

RS-94-2 Alexander E. Andreev. Complexity of Nondeterministic Functions. February 1994, 47 pp.

RS-94-3 Uffe H. Engberg and Glynn Winskel. Linear Logic on Petri Nets. February 1994, 54 pp.

RS-94-4 Nils Klarlund and Michael I. Schwartzbach. Graphs and Decidable Transductions based on Edge Constraints. February 1994, 19 pp. Appears in: Trees in Algebra and Programming CAAP ’94 (ed. S. Tison), LNCS 787, 1994.

RS-94-5 Peter D. Mosses. Uni�ed Algebras and Abstract Syntax. March 1994, 21 pp. To appear in: Recent Trends in Data Type Speci�cation (ed. F. Orejas), LNCS 785, 1994.

RS-94-6 Mogens Nielsen and Christian Clausen. Bisimulations, Games and Logic. April 1994, 37 pp. Full version of paper to appear in: New Results and Trends in Computer Science, LNCS, 1994.