Co-Induction and Term Graphs

For the sake of clarity, we will use curried notation for function application. \(f(x)\) will frequently be written as \(f\ x\) and \(f\ x\ y\) or \(f(x)(y)\) will mean \((f(x))(y)\). Occasionally, this could lead to ambiguity, e.g., when we wish to represent \(x\ y\) as the concatenation of \(x\) and \(y\). In such cases, ambiguity will be resolved by clarification of the specific use.

The Colon symbol \((:)\) will be used interchangeably with \(\in\) to denote membership: \(x:A\) is identical to \(x\in A\).

\(\N\) denotes the set of natural numbers. \(\N_1\) denotes the set of positive natural numbers. An index is a positive natural number. Let \(m:\N\) denote a natural number. \(\N_1(m)\) denotes the subset of \(\N_1\) consisting of indices less than or equal to \(m\). Note that \(\N_1(0)\) is empty.

If \(f:A\pfn B\) is a partial function from \(A\) to \(B\), then \(A\) and \(B\) are called the domain and the codomain of \(f\) and denoted \(\id{dom}\ f\) and \(\id{cod}\ f\), respectively. The domain of definition of \(f\), written \(\id{dod}\ f\) is the set \({x\in A\ |\ \exists y\in B. y=f\ x}\). The range of \(f\), denoted \(\id{rng}\ f\) is the set of all \(y\in B\) such that there is an \(x\in A\) such that \(f\ x=y\).

A signature \(\Sigma\) is a finite set of constructor symbols along with an arity function \(\alpha:\Sigma\rightarrow \N\). We write \(\Sigma^{(n)}\) to denote the set of all constructors that have arity \(n\). A constructor is said to be nullary if its arity is zero.

The set of \(T_{\sf ind}(\Sigma)\) of inductive terms over a signature \(\Sigma\) is defined using the following rule \[ \frac{\tau_1:T_{\sf ind}(\Sigma)\quad \ldots \quad \tau_n:T_{\sf ind}(\Sigma)} {f(\tau_1, \ldots, \tau_n)\ : T_{\sf ind}(\Sigma)} \quad f:\Sigma^{(n)}\qquad CONS \]

Recall that a rule tells us how to derive new judgements from old. A rule consists of a consequent and antecedent parts:

1. A consequent which is the concluding judgement (written below the line).
2. A set of antecedent judgements (written above the line).

In addition, a rule may have side conditions, which are written immediately to the right of the rule. A rule also has a name, for reference, which is written left most to the rule.

Exercise: Identify all the pieces of the rule above.

If each of the antecedent judgements is derivable, and the side conditions hold, then the consequent judgement is derivable using the given rule.

The structure \(f(\tau_1, \ldots, \tau_n)\) is a more traditional syntax for the list \((f, \tau_1, \ldots, \tau_n)\). We will continue to use the former notation in our narrative, but switch to the latter (sans commas!) when implementing terms in Racket.

The inductive terms \(\tau_1, \ldots \tau_n\) are called immediate subterms of \(f(\tau_1, \ldots, \tau_n)\). The transitive closure of the immediate subterm relation is the proper subterm relation.

It is not possible to have an inductive term \(\tau\) such that \(\tau\) is a proper subterm of itself. (Exercise: prove it).

Let \(\N_1\) denote the set of positive integers. A term graph over a signture \(\Sigma\) is a tuple \(\pair{V, h, \xto{}{}}\) where

1. \(V\) is a (countable) set of vertices.
2. \(h\) is the head function mapping \(V\) to \(\Sigma\).
3. \(\xto{}{} \subseteq V\times \N_1\times V\) is a transition relation. We write \((v, i, v')\) as \(v\xto{i}{}v'\). We say that \(i\) takes \(v\) to \(v'\).
4. If \(h(v)\in \Sigma^{(n)}\), then \(v\) has exactly \(n\) out-edges. For each \(i\), \(1\leq i \leq n\), there is exactly one out-edge labeled \(i\).

Assume a term graph \(G\) with vertices \(v\) and \(v'\). Let \(p\) denote an index sequence. \(v\xto{p}{G}{v'}\) means that there is a path from \(v\) to \(v'\) whose label is \(p\). We say that \(p\) takes \(v\) to \(v'\). Another way of saying this is that \(v'\) is reachable from \(v\) via \(p\).

The path relation may be defined inductively.

It is not hard to see that since \(G\) is a term graph, \(v\xto{p}{G}r\) is in fact a function: if \(v\xto{p}{G}s\), then \(r=s\). (Exercise: prove this.)

If \(v\) is a vertex in a term graph \(G\), then \(\id{pos}_G\ v\) denotes the set of positions for \(v\), i.e., the set of all index sequences \(p\) such that \(v\xto{p}{G}v'\) for some vertex \(v'\) in \(G\). \(\id{dest}_G\ v\) maps a position in \(\id{pos}_G\ v\) to the unique vertex that is reachable from \(v\) via \(p\). We drop the subscript \(G\) when it is clear from the context.

If \(h(v)=f\) and \(f\in \Sigma^{(n)}\) and \(v\xto{i}{G}v_i\), for each \(i:1\leq i\leq n\), then we denote this by the relation

\[v \eqn f(v_1, \ldots, v_n)\]

to indicate that (a) \(\id{h}(v)=f\), (b) \(f\in \Sigma^{(n)}\), and (c) for each \(i\) \(1\leq i\leq n\), \(v\xto{i}{G}v_i\).

The above looks like an equation if we interpret the vertices as variables. In particular, the relation element is a `flat term equation', `flat' because the constructor is applied to other vertices. A term graph may be completely specified by a system of such `flat term equations' with one equation for each vertex in the term graph.

A solution to an inductive term graph over \(\Sigma\) is a map \(\sigma\) from \(V_G\) to inductive terms over \(\Sigma\) that `solves' the flat system of equations: i.e., for each `flat equation' \(v \eqn f(v_i, \ldots, v_n)\) in \(G\):

\[\sigma\ v = f(\sigma\ v_1, \ldots, \sigma\ v_n)\]

The inductive term graph \(G\) and its representation as a system of equations is shown below:

Proof: left as an exercise.

So far, we have seen inductive terms and term graphs. We have seen that each vertex of an inductive term graph may be interpreted as a inductive term.

But what about terms graphs that are not inductive? For such graphs, the notion of solution based on inductive terms we have defined so far no longer holds:

Consider for example the equation representing the cyclic term graph \(G\) below.

Let \(\sigma = \set{t\mapsto \tau}\) where \(\tau\) is an inductive term. Suppose \(\sigma\) is a solution of \(G\). Then, we should have

Clearly \(\tau\) does not exist, as this violates the well-foundedness property of inductive terms. Therefore, for cyclic term graphs can not have solutions that consist only of inductive terms. But can they have solutions that are not inductive `terms'? This begs the question of what is a `term', after all?

We wish to associate a term with each vertex in a term graph but we are grappling with the question of what is a term. One way to answer to this question is to consider what we can observe at the vertex and how we can `interact' with it. The observation related to a vertex is simply its head. A `unit' interaction consists of supplying an index (between 1 and the arity of the vertex's head) to the vertex and getting back another vertex (the child).

Notice that we can overload the equation to mean the following:

1. An observation that the head of \(v\) is \(f\) and
2. \(n\) unit interactions with \(v\) that respectively yield the vertices \(v_1, \ldots, v_n\).

is literally the relation \(v \eqn f(v_1, \ldots, v_n)\).

A position space is any set of index sequences \(P\) that that is prefix closed: if \(q\in P\) then every prefix \(p\) of \(q\) is also in \(P\).

If \(B_1\ldots B_n\) are behaviours and \(f\in \Sigma^{(n)}\), then we write \(f(B_1\ldots, B_n)\) to denote the behaviour \((\Union_{i=1}^n\ i\ B_i) \union \set{[\ ]\mapsto f}\).

Now, we are ready to formally define a term:

Defn [(Co-Inductive) Term] Given a signature \(\Sigma\) a term over \(\Sigma\) is a behaviour over \(\Sigma\).

Notice that in the definition of term, we have dispensed with the notion of vertices or term graphs. The notion of a term exists independent of a term graph, but may be generated via interactions with a vertex in a term graph.

(Co-Inductive) terms are behaviours over a signature. A term is inductive if its domain of definition is a finite position space.

Exercise: Verify that the definition of inductive terms via derivation using the CONS rule matches the above characterization.

Let \(t\) and \(t_i\) be two terms. \(t_i\) is an immediate subterm of \(t\) if there exists an \(f\in \Sigma\) and terms \(t_1, \ldots, t_n\) such that

1. \(t = f(t_1,\ldots, t_n)\) and
2. \(t'=t_i\) for some \(i\), \(1\leq i\leq n\).

The reflexive transitive closure of the immediate subterm relation is called the subterm relation. A term is rational if the set of all its subterms is finite.

One way of capturing the sum total of interactions and observations at a vertex is to list (a) the set of all valid interaction sequences (positions), and (b) and the observation of the head of the destination vertex at the end of each path. We call this the observable behaviour, or just behaviour of a vertex.

Formally, let \(G\) be a term graph over a signature \(\Sigma\). The observable behaviour of a vertex \(v\) in \(G\), written \(\id{obs}_G\ v\), is a map from the position space \(\id{pos}_G\ v\) to \(\Sigma\) and is defined as

\[\id{obs}_G\ v\ p \ida h(\id{dest}_G\ v\ p)\]

The following inductive definition is an alternative way to define the observable behaviour function:

(Exercise: show that the two alternative definitions are equivalent.)

\(\id{obs}_G\) is called the observable behaviour map of term graph \(G\). The range of \(\id{obs}_G\), denoted \({\cal B}_G\) is called the set of observable behaviours in \(G\).

Let us revisit the term graph \(G\) of Example 6.2, For the vertex \(t_1\), its position space is the set \(\set{[\ ], [1], [2], [1\ 1]}\). Its observable behaviour, \(\id{obs}(t_1)\), is the map

The set of observable behaviours of \(G\) is the collection of observable behaviours of each of its vertices.

A solution to a term graph is function \(\sigma\) that maps each vertex \(v\) in \(G\) to a behaviour such that if \[v \eqn f(v_1\ldots, v_n)\]

then

\[\sigma\ v = f(\sigma\ v_1, \ldots, \sigma\ v_n)\]

The solution set of a term graph is the range of the solution.

If \(G\) is a term graph, then the observable behaviour map \(\id{obs}_G\) is the unique solution of \(G\).

Given a term graph \(G\), each vertex of \(G\) may be mapped to its `meaning': a co-inductive term which is obtained via the solution of the flat system of term equations.

Exercise: Show that a term is inductive iff it is in the solution set of a finite and acyclic term graph.

Exercise: Show that if the term graph \(G\) is finite and acyclic, then the solution set of \(G\) consists of only inductive terms.

Exercise: Give an example to show that the converse is not true. It is possible to have a solution set consisting of only inductive terms for a graph that is not finite.

Exercise: Show that a term is rational iff it is in the solution set of a finite term graph.

Finite and acyclic (respectively finite) have solution sets consisting of terms that are inductive and rational respectively. The relationships between the term graphs and the terms in the solution sets of those term graphs is summarised below:

\[\text{Inductive}\subseteq \text{Rational}\subseteq \text{Co-inductive}\]

One might be tempted to think of co-inductive terms as `limits' of inductive terms. If we try to do that, we run into the following difficulty. Consider a non-empty signature \(\Sigma\) consisting only of a unary constructor \({\sf g}\). The set of inductive terms, viz., \(T_{\sf ind}(\Sigma)\) is empty, while the set of co-inductive terms is not. So, there are no inductive terms available to approximate the co-inductive term \(t={\sf g}(t)\).

Seeing terms as functions from a position space to constructors is only one way of interpreting terms. Another way, which we have been using so far inductive terms, is continue to see terms as tuples. To accommodate co-inductive terms as tuples we will need confront the possibility that tuples — and ultimately sets — could be circular, i.e., they contain themselves. There is a a variant of set theory that entertains this possibility (the theory of non-well-founded sets, or `hypersets'). This theory has its own formulation of the Solution Lemma: every flat system of equations has a unique solution, which maps vertices to tuples. We will not make a detour into non-well-founded set theory. Instead, we will rely on functional programming to do model circular objects in yet another way.

We need to be careful, for, otherwise we could be trapped in a hopelessly circular argument: Consider the term graph with two vertices:

We want to show that both the vertices \(t_1\) and \(t_2\) refer to the same infinite term \({\sf g}({\sf g}(...))\). Now, if were to reason using the `DOWN' rule, we end up with something like this:

\(t_1\) are \(t_2\) are the same, because their heads are the same (both are \({\sf g}\)) and their immediate subterms, viz \(t_2\) and \(t_1\) are the same.

This is clearly a circular argument. The objects of our reasoning may be circular, but circular reasoning is mathematically unacceptable: A proof can not assume what it is trying to prove. Trying the `UP' rule instead doesn't help either. A different approach is needed, and this is where the notion of bisimulation comes in.

The intuitive idea behind bisimulation is that we `decree' that two terms are equal, and challenge anyone to show us where we are wrong. This kind of reasoning may seem untenable, but it's not without value or use. Imagine a court scene in which a defendant charged with murder claims that he was away with his friend in Mumbai on the night of a crime that took place in Delhi. His alibi provides an argument consistent with the defendant's claim. Should the defendant be pronounced guilty? In the absence of any contradictory evidence challenging or repudiating the claims of the defendant, a jury will be unable to prosecute the defendant and the defendant will be acquitted.

Reasoning with bisimuation is similar: first we propose an `equality' (bisimulation) relation. Then, we try to verify that this relation is consistent with the equality flowing down between subterms.

Let \(T\) be a \(\Sigma\)-term graph with vertex set \(V\). A relation \(R\subseteq V\times V\) is a bisimulation if for each pair \((v,v')\in R\), the following is true:

1. \(\id{h}(v)=\id{h}(v')\): Their heads are the same, and
2. for each \(i\), \(1\leq i \leq \alpha(\id{h}(v))\), if \(v\xto{i}{}v_i\) and \(v'\xto{i}{}v'_i\), then \((v_i, v'_i) \in R\).

We say two vertices \(v\) and \(v'\) in the $Σ$-term graph are bisimilar iff there is a bisimulation relation \(R\) such that \((v,v')\in R\).

Therefore, we work with bisimilarity as the notion of observational equivalence between vertices. One way of thinking about this (and it will be generalised in later classes) is that vertices are like `states': black boxes that allow only specific observations about them and interactions that take you to other vertices. Vertices that are bisimilar have the same observations. In addition, identical interactions with them take us to states that are themselves bisimilar.

Let \(G\) be a term graph and let \(t\) be a term vertex and let \(t_p\) be the subterm vertex of \(t\) at position \(p\). Let \(s\) be another term vertex. If we think of \(t\) as the root of a a (possibly infinite) tree, then the replacement of the subterm of \(t\) at position \(p\) by term \(s\), denoted \(\id{replace}(t,p,s)\) results in a new term graph. Everything works out nicely when the terms are inductive or infinite. But, when dealing with circular term graphs, `unrolling' the circular term graph is necessary when performing replacement.

Here are some examples. For replacement involving term trees, we dispense with writing down elaborate term graphs and rely on the tree (expression) notation:

What happens when (sub)terms are shared? Consider

What is the result of \(\id{replace}(t_1, [1\ 1], t_4)\)? Is it \({\sf f(g(b), a)}\) or \({\sf f(g(b), b)}\)? The correct answer is \({\sf f(g(b), a)}\) because we may think of position \([1\ 1]\) as a pointer which is now pointing to \(t_4\). The pointer \([2]\) is unchanged.

Let \(t\) be a term and let \(p\) be a position in \(t\). Let \(t'\) be a subterm of \(t\) at position \(p\). This means that

1. \(p\in \id{pos}_G(t)\).
2. If \(q\in \id{pos}_G(t')\), then \(pq\in \id{pos}_G(t)\) and \(t(pq) = t'(q)\).

Let \(s\) be a term. \(\id{replace}(t, p, s)\) results in the following term \(r\):

We define \(r\) via pattern matching positions:

Exercise: Verify that the result of a replacement is indeed a term.

We define inductive terms as lists whose first element is a symbol. For simplicity we will altogether avoid arity checking. Every time we call list a brand new vertex is created in the term graph.

(check-true (term? (list 'a)))
(check-true (term? (list 'g '(a))))
(check-true (term? '(f (g (a)) (a))))

To define co-inductive terms, we need a co-inductive version of list: colist.

(check-true (term? (list 'g '(a))))
(check-true (term? (colist 'g '(a))))
(check-true (term? (rec t (colist 'g t))))
(check-true (term? (list 'g (rec t (colist 'g t)))))

colist is defined by extending Racket's syntax. colist is a lazy constructor. It does not evaluate its arguments, and thereby allows delaying their evaluation. This is a crucial tool to construct co-inductive terms. We have already seen a cousin scons of colist which was used to construct streams.

(define-syntax colist
  (syntax-rules ()
    [(colist sym terms ...) 
     (lambda () (list sym terms ...))]))

A term is either one built inductively (using list) or built co-inductively (using colist):

;;; term? :: any/c -> boolean?
(define term? (or/c procedure? list?))

The head of a term returns the constructor:

(check-equal? (hd (g (a))) 'g)
(check-equal? (hd (rec t (colist 'g t))) 'g)

If the term is a list, that's easy: the head is just the car of the list. If the term is built using colist, then we will need to first unroll the procedure representing the term to get a list. Then we take the car of that list.

;;; unroll :: term? -> term?
(define (unroll t)
  (if (procedure? t) (t) t))

;;; hd :: term? -> symbol?
(define (hd t)
  (car (unroll t)))

An index is a positive integer.

;;; posint? :: any/c -> boolean?
(define posint? (and/c integer? (>=/c 1)))
(define index? posint?)

Now that we have the head, let's try to locate the children of a term. Analogous to Racket's list-ref, we define term-ref ,which returns the i=th element of the (list representing) the term. =term-ref indexes into a term and returns the immediate subterm at that index. If the index is greater than the arity of the term's head, Racket throws an error.

;;; term-ref :: term? posint? -> term?
(define (term-ref t i)
  (list-ref (unroll t) i))

(check-equal? (term-ref (list 'f '(a) '(b)) 1) '(a))
(check-equal? (term-ref (list 'f '(a) '(b)) 2) '(b))
(check-exn exn:fail? (lambda () (term-ref (list 'f (a) '(b)) 3))) ; index type checking 

A position is a sequence of indices.

;;; pos? :: any/c -> boolean?
(define pos? (listof index?))
(check-true (pos? '()))
(check-true (pos? '(1 3 2)))
(check-false (pos? '(0 1)))

Given a position pos in a term t we want to find the subterm at that position.

(check-equal? (subterm '(f (a) (a)) '())
              '(f (a) (a)))

(check-equal?  (subterm '(f (a) (b)) '(2))
              '(b))

(letrec ([t (colist 'g t)])
  (check-equal?  (subterm  t '(1 1))
                 t))


(letrec ([t (colist 'f t '(a))])
  (check-equal? (subterm t '(1 1 2))
                '(a))
  (check-equal? (subterm t '(1 1 1))
                t))

If the position is empty, then the answer is t. Otherwise, we take the first index from pos, say i, and search inside the i=th child t_i of t.

;;; subterm :: term? pos? -> term?
(define (subterm t pos)
  (letrec ([loop (lambda (t pos)
                   (cond [(null? pos) t]
                         [else (let* ([i (first pos)]
                                      [t_i (term-ref t (first pos))])
                                 (loop t_i (rest pos)))]))])
    (loop t pos)))

Before defining replacement in terms, we consider a simpler situation: replacing an element at a particular index in a list with another element. We call this operation replace-flat. (replace-flat ls i val) takes a list ls, an index i within the boundaries of ls and a value val and return a new list whose value at position i is val, but all other positions, it is the same as that of ls.

(check-equal? (replace-flat '(f a b) 1 'c) '(f c b))
(check-exn exn:fail? (lambda ()  (replace-flat '(f a b) 0 'c)))

Now we come to replace. In the first test below, the subterm (a) in the term (g (a)) occurs at position [1] and is replaced (b).

(check-equal?  (replace '(g (a)) '[1] '(b))
               ;; replace '(a) with '(b)
               '(g (b)))

In the test below, the subterm (a) occurs at position [1 1] in the top level expression and is again replaced by (b).

(check-equal?  (replace '(f (g (a)) (b)) '[1 1] '(b))
               ;; replace (a) with (b)
               '(f (g (b)) (b)))

In the test below, a coterm t is constructed as shown below in Figure 5 on the . We wish to replace the subterm at position [1 1 2] in t with (b). That involves unrolling t a few times before (b) can be grafted at the position [1 1 2]. The result is shown in Figure 6.

(letrec ([t (colist 'f t '(a))])
  (let ([r (replace t '[1 1 2] '(b))])
    (check-equal?  (subterm r '[1 1 2]) '(b))
    (check-eq? (subterm r '[1 1 1]) t))) ; this last test should get you thinking!

Exercise: Write systems of flat equations that precisely mimic the term graphs according to the Racket implementation. Then, draw diagrams of other possible term graphs that represent the replacement.

Exercise: Implement the function bisimilar?.

Ana Bove 2018

Notes on Inductive Sets and Induction.

Kozen and Silva, 2016. Practical Co-Induction

Math. Structures in Computer Science. pp 1–21. 10.1017/S0960129515000493.

Bahr 2012

Infinitary Term Graph Rewriting is Simple Sound and Complete. Rewriting Techniques and Applications. 2012

Co-inductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

Endrullis et al. Logical Methods in Computer Science. Vol 14(1:3) 2018 pp. 1–44. http://www.lmcs-online.org

• Wikipedia page on Knaster-Tarski Theorem
• Online Notes.
• Cornell CS 6110 S 17 Lec 7 Notes

Moss, Lawrence S. 2018

Non-wellfounded Set Theory, The Stanford Encyclopedia of Philosophy (Summer 2018 Edition), Edward N. Zalta (ed.),

Akman and Pakkan, 1996

Nonstandard set theories and information management. A readable discussion of Set Theory with the Anti-foundation axiom and its application to relational database theory (Sec 3.2).