We study a variant of the Ackermann encoding NA(x) := Py2x 2NA(y) of the hereditarily nite sets by the natural numbers, applicable to the larger collection HF1=2 of the hereditarily nite hypersets. The proposed variation is obtained by simply placing a `minus' sign before each exponent in the de nition of NA, resulting in the expression RA(x) := Py2x 2 RA(y). By a careful analysis, we prove that the encoding RA is well-de ned over the whole collection HF1=2, as it allows one to univocally assign a real-valued code to each hyperset in it. We also address some preliminary cases of the injectivity problem for RA.
In 1937, W. Ackermann proposed the following recursive encoding of hereditarily nite sets by natural numbers:
NA(x) :=
X 2NA(y): y2x (1) The encoding NA is simple, elegant, and highly expressive for a number of reasons. On the one hand, it builds a strong bridge between two foundational mathematical structures: (hereditarily nite) sets and (natural) numbers. On the other hand, it enables the representation of the characteristic function of hereditarily nite sets in terms of the usual notation for natural numbers as sequences of binary digits. That is: y belongs to x if and only if the NA(y)-th digit in the binary expansion of NA(x) is equal to 1. As one would expect, the string of 0's and 1's representing NA(x) is nothing but (a representation of) the characteristic function of x.
proposed in [Pol13] and discussed in [DOPT15] and [OPT17], applicable to a larger collection of sets. The proposed variation is obtained by simply placing a minus sign before each exponent in (1), resulting in the expression: RA(x) := As opposed to the encoding NA, the range of RA is not contained in the set N of the natural numbers, but it extends to the set R of real numbers. In addition, the domain of RA can be expanded so as to include also the non-well-founded hereditarily nite sets, namely, the sets de ned by ( nite) systems of equations of the following form with bisimilarity as equality criterion (see [Acz88] and [BM96], where the term hyperset is also used). For instance, the special case of the single set equation & = f&g, resulting into the equation (in real numbers) x = 2 x, is illustrated in Section 3 and provides the code of the unique (under bisimilarity) hyperset = f g.3
our intuition of the very basic properties of the collections of natural numbers N and of hereditarily nite sets HF|called HF0 in [BM96]), the de nition of RA, instead, is not inductive when extended to non-well-founded sets, and thus it requires a more careful analysis, as it must be proved that it univocally (and possibly injectively) associates (real) numbers to sets.
The injectivity of RA on the collection of well-founded and non-well-founded hereditarily nite sets|henceforth, to be referred to as HF1=2, see [BM96]|was conjectured in [Pol13] and is still an open problem. Here we prove that, given any nite collection ~1; : : : ; ~n of pairwise distinct sets in HF1=2 satisfying a system of set-theoretic equations of the form (2) in n unknowns, one can univocally determine real numbers RA(~1); : : : ; RA(~n) satisfying the following system of equations:
associates a unique (real) number to each hereditarily nite hyperset in HF1=2. This extends to HF1=2 the rst of the properties that the encoding NA enjoys with respect to HF. Should RA also enjoy the injectivity property, the proposed adaptation of NA would be completely satis ying, and RA could be coherently dubbed an encoding for HF1=2.
In the course of our proof, we shall also present a procedure that drives us to the real numbers RA(~1); : : : ; RA(~n) mentioned above by way of successive approximations. In the well-founded case, our procedure will converge in a nite number of steps, whereas in nitely many steps will be required for convergence in the non-well-founded case. In the last section of the paper, we shall also brie y hint at the injectivity problem for RA. 3 Notice that the solution to the equation x = e x is the so-called omega constant, introduced by Lambert in [Lam58] and studied also by Euler in [Eul83].
Let N be the set of natural numbers and let P( ) denote the powerset operator.
all hereditarily nite sets, where nite sets). HF := Sn2N HFn is the collection of (
HF0 := ;;
HFn+1 := P(HFn); for n 2 N:
NA(h) :=
X 2NA(h0); for h 2 HF: h02h
NA(hi) = i, for i 2 N. Using the iterated-singleton notation
fxg0 := x fxgn+1 := fxgn ; for n 2 N, we plainly have: In addition, for j 2 N we have: h0 = ;; h1 = f;g; h2 = f;g2; h3 = ff;g; ;g; h4 = f;g3; etc. h0 2 hj i
j is odd, h2j = fhjg and h2j 1 = fh0; h1; : : : ; hj 1g : (3) (4) i hj The map NA induces a total ordering among the elements of HF (that we shall call Ackermann ordering) such that, for h; h0 2 HF: h h0
NA(h) < NA(h0) : Thus, hi is the i-th element of HF in the Ackermann ordering and, for i; j 2 N, we plainly have: hi i i < j:
Proposition 1. For hi; hj 2 HF, the following equivalence holds: hi hj i hi 6= hj and max(hi hj) 2 hj ; where is the symmetric di erence operator A B := (A n B) [ (B n A).
It is also useful to de ne the following map low : N ! N which, for i 2 N, computes the smallest code j of a set hj not present in hi (or, equivalently, the position of the lowest bit set to 0 in the binary expansion of i):
low(i) := minfj j hj 2= hig :
Lemma 1. For i 2 N, we have: (i) low(i) = 0 i
i is even, (ii) hlow(i) 2= hi, (iii) fh0; : : : ; hlow(i) 1g hi, (iv) hi+1 = hi n fh0; : : : ; hlow(i) 1g [ fhlow(i)g.
iom of regularity, which forbids both membership cycles and in nite descending chains of memberships. In the hypersets realm of our interest, based on the FortiHonsell axiomatization [FH83] as popularized by P. Aczel [Acz88], the axiom of regularity is replaced by the anti-foundation axiom (AFA). Roughly speaking, AFA states that every conceivable hyperset, described in terms of a graph speci cation modelling its internal membership structure, actually exists and is univocally determined, regardless of the presence of cycles or in nite descending paths in its graph speci cation. To be slightly more precise, a graph speci cation (or membership graph) is a directed graph with a distinguished node (point ), where nodes are intended to represent hypersets, edges model membership relationships among the node/hypersets, and the distinguished node denotes the hyperset of interest among all the hypersets represented by the nodes of the graph. However, extensionality needs to be strengthened so as structurally indistinguishable pointed graphs are always realized by the same hyperset. More speci cally, we say that two pointed graphs G = (V; E; p) and G0 = (V 0; E0; p0), where p 2 V and p0 2 V 0 are the `points' of G and G0, respectively, are structurally indistinguishable if the points p and p0 are bisimilar, namely, if there exists a relation R over V V 0 such that the following three properties hold, for all v 2 V and v0 2 V 0: (B1) (8w 2 V )(9w0 2 V 0) (v R v0 ^ (v; w) 2 E) ! ((v0; w0) 2 E0 ^ w R w0) ; (B2) (8w0 2 V 0)(9w 2 V ) (v R v0 ^ (v0; w0) 2 E0) ! ((v; w) 2 E ^ w R w0) ; (B3) p R p0.
bisimulation over V
V 0.
as a nite pointed graph: these are the hereditarily nite hypersets in HF1=2.
Given a ( nite) pointed graph G = (V; E; p) whose nodes are all reachable from its point p, the collection of hypersets represented by all its nodes form the transitive closure of f~g, denoted trCl (f~g), where ~ is the hyperset corresponding to the point p.
RA(x) :=
Consider the following map RA obtained from NA by simply placing a minus sign before each exponent in (1): (5) (6) RA(;) = 0;
1 RA(f;g3) = p ; 2
RA(f;g) = 1;
1 RA(f;g4) = 2 p2 ;
RA(f;g2) = RA(f;g5) = 2 2 p12 ; It is easy to see that the equation (6) has a unique solution in R, since the functions x and 2 x are, respectively, strictly increasing and strictly decreasing, so that the function x 2 x is strictly increasing. In addition, we have: x 2 xjx= 21 = 21 Thus, the solution of (6) over R, namely, the code of the hyperset de ned by the set equation x = fxg, satis es 12 < < 1. Furthermore, much by the same argument used by the Pythagoreans to prove the irrationality of p2, it can easily be shown that is irrational. In fact, is transcendental. This follows from the Gelfond-Schneider theorem (see [Gel34]), which states that every real number of the form ab is transcendental, provided that a and b are algebraic numbers such that 0 6= a 6= 1, and b is irrational.4 Indeed, if were algebraic, so would be and therefore, by the Gelfond-Schneider theorem, 2 = would be transcendental, contradicting the assumed algebraicity of . Thus, must be transcendental after all. As is easy to check, the RA-code 2 1=p2 of f;g4 is transcendental as well.
a consequence of the results to be proved in Section 4, we shall see that (5) allows one to associate univocally a code to each non-well-founded hereditarily nite set as well, thus showing that RA is also well-de ned over the whole collection HF1=2 of hereditarily nite hypersets. 4 We recall that the Gelfond-Schneider theorem, obtained independently in 1934 by A. O. Gelfond and Th. Schneider, solves completely the seventh in a well-celebrated list of twenty-three problems posed by David Hilbert at the International Congress of Mathematicians held in Paris, 1900 (see [Hil02]).
Remark 1 For every singleton fh0g 2 HF, de nition (5) gives RA(fh0g) = 2 RA(h0). Thus, for every h 2 HF, we have
RA(h) = n n X 2 RA(h0) = X RA (fh0g) : h02h h02h
Once we prove that RA is well-de ned over HF1=2, equation (7) can be immediately generalized to HF1=2 as well.
Proposition 2. For any n 2 N, there exists an i 2 N such that RA(hi) > n. Proof. Notice that for any odd natural number j, we have ; 2 hj . Thus, by (7), we have RA(hj ) > R(f;g) = 1, RA(fhj g) = 2 RA(hj) 6 2 1 = 12 , and RA(ffhj gg) = 2 RA(fhjg) > 2 1=2 > 12 .
Let k = 4n and consider the hereditarily nite set h := fhk0 g : k0 6 k .
k RA(h) = X k0=0
RA (ffhk0 gg) > k X k0=0 k0 is odd 1 k RA (ffhk0 gg) > 2 2 = n : 4
The fully general case corresponds to considering systems of set-theoretic equations such as the ones introduced by the following de nition (see also [Acz88]). De nition 3 (Set systems). A set system S (&1; : : : ; &n) in the set unknowns &1; : : : ; &n is a collection of set-theoretic equations of the form: with mi > 0 for i 2 f1; : : : ; ng, and where each unknown &i;u, for i 2 f1; : : : ; ng and u 2 f1; : : : ; mig, occurs among the unknowns &1; : : : ; &n.5
The index map IS of S (&1; : : : ; &n) is the map
n IS : [ fhi; vi j 1 6 v 6 mig ! f1; : : : ; ng
i=1 such that IS (i; v) is the index of the unknown &i;v in the list &1; : : : ; &n, for i 2 f1; : : : ; ng and v 2 f1; : : : ; mig, namely, &IS (i;v) &i;v. 5 When mi = 0, the expression f&i;1; : : : ; &i;mi g reduces to the empty set fg. (7) (8)
A set system S (&1; : : : ; &n) is normal if there exist n pairwise distinct (i.e., non bisimilar) hypersets ~1; : : : ; ~n 2 HF1=2 such that the assignment &i 7! ~i satis es all the set equations of S (&1; : : : ; &n).
Observe that, by the anti-foundation axiom, the assignment &i 7! ~i satisfying the equations of a given normal set system S (&1; : : : ; &n) is plainly unique.
scripts, to denote a generic (possibly well-founded) hyperset in HF1=2.
ciate a system of equations in R, called code system, as follows.
De nition 4 (Code systems). Let S (&1; : : : ; &n) be a normal set system of the form . .
. 8> &1 = f&1;1; : : : ; &1;m1 g > < with index map IS . The code system associated with S (&1; : : : ; &n) is the following system C (x1; : : : ; xn) of equations in the real unknowns x1; : : : ; xn: where xi;u is a shorthand for xIS (i;u), for i 2 f1; : : : ; ng and u 2 f1; : : : ; mig.
Normal set systems characterise all possible elements of HF1=2 and we shall see that the corresponding code systems characterise their RA-codes. In fact, we shall prove that every code system admits a unique solution which can be computed as the limit of suitable sequences of real numbers. Terms in such sequences approximate the nal solution alternatively from above and from below. In case of non-well-founded sets, such approximating sequences are in nite and convergent (to the codes of the non-well-founded sets); additionally, its terms eventually become codes of certain well-founded hereditarily nite sets which can be seen as approximations of the corresponding non-well-founded set.
We begin by formally de ning the set and multi-set approximating sequences (of the solution) of set systems.
De nition 5 (Hereditarily nite multi-sets). Hereditarily nite multi-sets are collection of elements|themselves multi-sets|that can occur with nite multiplicities.
Remark 2 A natural embedding of the hereditarily nite sets in the hereditarily nite multi-sets is the following: a multi-set can be regarded as a set if and only if each of its elements has multiplicity 1 and, recursively, can be regarded as a set. Thus, in particular, ; is both a set and a multi-set.
De nition 6. Let S (&1; : : : ; &n) be a (normal) set system of the form (8), and let IS be its index map. The set-approximating sequence for (the solution of ) S (&1; : : : ; &n) is the sequence h~ij j 1 6 i 6 ni j2N of the n-tuples of wellfounded hereditarily nite sets de ned by
j h~i j 1 6 i 6 ni := <8 h; j 1 6 i 6 ni : hf~ij;11; : : : ; ~ij;m1i g j 1 6 i 6 ni if j > 0 ; where ~ij;u1 is a shorthand for ~jIS (1i;u), for i 2 f1; : : : ; ng and u 2 f1; : : : ; mig.
The multi-set approximating sequence for (the solution of ) S (&1; : : : ; &n) is the sequence h ij j 1 6 i 6 ngi j2N of the n-tuples of well-founded hereditarily nite multi-sets de ned by
j h i j 1 6 i 6 ni := <8 h; j 1 6 i 6 ni : h[ ij;11; : : : ; ij;m1i ] j 1 6 i 6 ni if j > 0 ; if j = 0 if j = 0 where ij;u1 is a shorthand for j 1
IS (i;u), for i 2 f1; : : : ; ng and u 2 f1; : : : ; mig.
and &i0 , with i; i0 2 f1; : : : j; ng, are distinguished at step k > 0 by the setapproximating sequence h~i j 1 6 i 6 ni j2N for S (&1; : : : ; &n) (resp., multi-set approximating sequence h ij j 1 6 i 6 ni j2N for S (&1; : : : ; &n)) if ~ik 6= ~ik0 (resp., ik 6= ik0 ). Further, we shall refer to ~ij (resp., ij ) as the (j-th) setapproximation value (resp., multi-set approximation value ) of &i at step j.
8> &1 = f&2; &3g S (&1; &2; &3; &4) = ><> &&23 == ff&g3g >: &4 = f&2g : In this case, we have: m1 = 2; m2 = 0; m3 = 1, and m4 = 1; in addition, &1;1, &1;2, &3;1, and &4;1 are &2, &3, &3, and &2, respectively, so that IS (1; 1) = 2, IS (1; 2) = 3, IS (3; 1) = 3, and IS (4; 1) = 2.
The rst four elements of the set-approximating sequence for S are: = hf;; ff;ggg; ;; fff;ggg; f;gi :
Notice that, for j = 2 and j = 3, all the ~ij 's are pairwise distinct. In fact, as a consequence of the next lemma, this is true also for all j > 3.
The rst four tuples of the multi-set approximating sequence of S are:
Also in this case, for j = 2 and j = 3, all the ij 's are pairwise distinct and this holds also for j > 3. Observe that the unknowns &i and &j are distinguished by the multi-set approximating sequence before than by the set-approximating sequence: indeed, 11 6= 31, whereas ~11 = ~31.
itarily nite sets. The initial tuples of a multi-set approximating sequence may contain proper multi-sets (as in the above example). However, as a consequence of the following lemma (whose proof can be found in the extended version [CP18] of this paper), after at most n steps all pairs of distinct unknowns are distinguished and each tuple contains only proper sets.
Lemma 2. Let S (&1; : : : ; &n) be a normal set-system, and let h~ij j 1 6 i 6 ngi j2N and h ij j 1 6 i 6 ni j2N be its set- and multi-set approximating sequences, respectively. The following conditions hold: (a) for i; i0 2 f1; : : : ; ng and j; k > 0, we have ~ij 6= ~ij0 =) (~ij+k+1 6= ~ij0+k+1 ^ ij 6= j i0 ) (namely, if at step j > 0 two unknowns are distinguished by the set-approximating sequence, then they are also distinguished by the multi-set approximating sequence; in addition, they remain distinguished in all subsequent steps); (b) for j; k > 0 and i 2 f1; : : : ; ng, we have ~ij = ~j+1 =) ~ij = ~j+k+2
i i (namely, as soon as ~ij = ~j+1 holds for some j > 0, the set-approximation i value of &i remains unchanged for all subsequent steps); (c) for i; i0 2 f1; : : : ng and j > n, we have (i 6= i0 =) ~ij 6= ~i0 ) ^ h i j 1 6 i 6 ni = h~i j 1 6 i 6 ni
j j j (namely, starting from step n, all pairs of distinct unknowns are distinguished and the set- and multi-set approximating sequences coincide). approximating sequence i 2 f1; : : : ; ng and j 2 N:
approximating sequences will eventually \separate" all solutions of a set system, multi-set can introduce inequalities rst. This is our rst motivation for extending the notion of RA-code to multi-sets and use such code-extension to approximate regular RA-codes. The second motivation is given in Remark 3. De nition 7. Given a normal set system S (&1; : : : ; &n) and its multi-set approximating sequence h ij j 1 6 i 6 ngi j2N, we de ne the corresponding code hRA( ij ) j 1 6 i 6 ngi j2N by recursively putting, for (
RA( i0) := 0 RA( ij+1) := Pum=i 1 2 RA( ij;u) : (10) (11) j We also de ne the corresponding code increment sequence h i j 1 6 i 6 ni j2N by putting, for i 2 f1; : : : ; ng and j 2 N: ij := RA( ij+1)
RA( ij ) :
Plainly, RA( ij ) > 0, for all i 2 f1; : : : ; ng and j 2 N.
Remark 3 Consider a normal set system S (&1; : : : ; &n) and its solutions ~1; : : : ; ~n. The values RA( i1) and RA( i10 ) are equal if and only if j~ij = j~i0 j. The values RA( i2) and RA( i20 ) are equal if and only if the multi-sets of the cardinalities of elements in ~i and ~i0 are equal. The values RA( i3) and RA( i30 ) are equal if and only if the multi-sets of multi-sets of the cardinalities of elements of elements in ~i and ~i0 are equal, and so on.
Lemma 3. Let S (&1; : : : ; &n) be a normal set system of the form with index map IS , code approximating sequence and code increment sequence h ij j 1 6 i 6 ngi j2N. Then, for i 2 f1; : : : ; ng and j 2 N, the following facts hold: hRA( ij ) j 1 6 i 6 ngi j2N, (i) RA( ij+1) = i0 + (ii) i0 = mi,
+ ij , (iii) ij+1 = Pum=i 1 2 RA( ij;u) (2 i;u
j (iv) i2j+1 6 0 6 i2j , (v) j ij+1j 6 j i j, and
j (vi) limj!1 ij = 0.
1),
Theorem 4. For any given normal set system, the corresponding code system admits always a unique solution.
Proof. Let S (&1; : : : ; &n) be a normal set system of the form (8), and let hRA( ij ) j 1 6 i 6 ngi j2N and h ij j 1 6 i 6 ngi j2N be its code approximating sequence and code increment sequence, respectively. Also, let C (x1; : : : ; xn) be the code system . .
.
Existence: By Lemma 3(i),(iv),(vi), using the Leibniz criterion for alternating series, it follows that each of the sequences fRA( ij )gj2N is convergent, for i 2 f1; : : : ; ng. Let us put i := limj!1 RA( ij ), for i 2 f1; : : : ; ng. From (10), we have
RA( ij+1) = mi X 2 RA( ij;u); for j 2 N : u=1 Then, by taking the limit of both sides as j approaches in nity, it follows that i = for i 2 f1; : : : ; ng, where i;u is a shorthand for IS (i;u), with IS the index map of S (&1; : : : ; &n), proving that the n-tuple h 1; : : : ; ni is a solution of the code system C (x1; : : : ; xn).
Uniqueness: Next we prove that the solution h 1; : : : ; ni is unique. Let h 10; : : : ; n0i be any solution of the code system C (x1; : : : ; xn). To show that h 10; : : : ; n0i = h 1; : : : ; ni it is enough to prove that
RA 2j i 2j+1 ; for j 2 N and i 2 f1; : : : ; ng; i (12) holds. Indeed, from (12), it follows immediately i = lim RA j!1 2j i 6 i0 6 lim RA j!1 i2j+1 = i ; for every i 2 f1; : : : ; ng, showing that h 10; : : : ; n0i = h 1; : : : ; ni.
We prove (12) by induction on j, for all i 2 f1; : : : ; ng.
For the base case j = 0, we observe that since i0 = Pum=i 1 2
usual, i0;u stands for I0S (i;u)), then
0
i;u (where, as
RA
and recalling that i0 = Pum=i 1 2
i 2 f1; : : : ; ng and u 2 f1; : : : ; mig:
holds for some j 2 N, and prove that it holds for j + 1 as well. From (
RA i;u 2 RA( i2;ju+1) 6 2 6 i0;u 6 RA i;u 6 2 RA( i2;ju) 0 2j+1 i;u mi X 2 RA( i2;ju+1) 6 u=1 for every i 2 f1; : : : ; ng and u 2 f1; : : : ; mig. Hence, by repeating the very same steps as above, one can deduce also the inequalities
RA
2(j+1)
i
= RA
2j+2
i
for i 2 f1; : : : ; ng, proving that (
Remark 5 To show that the code RA is well-de ned over the whole HF1=2, we proceed as follows. Given a hereditarily nite hyperset ~ 2 HF1=2, let ~1; : : : ; ~n be the distinct elements of the transitive closure trCl (f~g) of f~g, where ~1 = ~. Then we have . .
. 8 ~1 = f~1;1; : : : ; ~1;m1 g > > < > > :~n = f~n;1; : : : ; ~n;mn g (14) for suitable hypersets ~i;j 2 f~1; : : : ; ~ng, with i 2 f1; : : : ; ng and j 2 f1; : : : ; mig.
Consider the set system S (&1; : : : ; &n) associated with (14), where &i;j = &` i ~i;j = ~`, for all i; ` 2 f1; : : : ; ng and j 2 f1; : : : ; mig. Plainly, S (&1; : : : ; &n) is normal and ~1; : : : ; ~n is its solution. By Theorem 4, let 1; : : : ; n be the solution to the code system associated with S (&1; : : : ; &n). Then RA(~i) = i, for i 2 f1; : : : ; ng, and, in particular, RA(~) = RA(~1) = 1. Further, it is immediate to check that, for every normal set system S 0(x01; : : : ; x0m) containing ~ in its solution, say at position k 2 f1; : : : ; mg, if 10; : : : ; m0 is the solution to the corresponding code system, then k0 = 1. In other words, the value RA(~) computed by the above procedure is independent of the normal set system used. By the arbitrariness of ~, it follows that RA(~) is de ned for every hyperset ~ 2 HF1=2. 5
A
rst step towards injectivity As already remarked, the problem of establishing the injectivity of the map RA is still open. As an initial example, we provide here a very partial result. However, the arguments used in the proof below do not seem to easily generalize even to the narrower task of proving the injectivity of RA over the well-founded hereditarily nite sets only.
Lemma 4. For all i 2 N, we have: (a) RA(hi) 6= RA(hi+1), and (b) RA(hi) 6= RA(hi+2), where hj is the j-th element of HF in the Ackermann ordering.
Proof. Let i 2 N. From (iii) and (iv) of Lemma 1 and from (4), we have RA(hi+1) = RA(hi)
RA(h2low(i) 1) + RA(h2low(i) ) :
(
RA(h2low(i) 1) = 0 6= 1 = RA(h2low(i) ) :
RA(h2low(i) ) < 1 = RA(fh0g) 6 RA(h2low(i) 1) :
RA(h2low(i) 1) 6= 0, proving (a), by (
j := RA(h2j )
h2j 1, and therefore:
Hence, we have j 6= 1 also for j > 2, since RA(h2j ) = 2 RA(hj) < 1. But
then, from (
RA(hi+2)
R(hi) = RA(hi+2)
R(hi+1) + RA(hi+1)
R(hi) =
low(i+1) + low(i) 6= 0 ; since either i or i + 1 is even and so either low(i) = 1 or low(i+1) = 1, whereas, as we proved above, low(i) 6= 1 6= low(i+1). This proves (b), completing the proof of the lemma.
Remark 6 While the value of RA i0 is 0 for any i 2 f1; : : : ; ng, the value of RA i1 | rst approximation of RA ( i)|is the cardinality of i, and the subsequent approximations oscillate within the interval [0; j ij].
By turning labels into sets, the encoding proposed in this paper can be used on a variety of structures, going from labelled graphs to Kripke models. This can be done in many di erent ways and in [DPP04,PP04] the reader can nd a rather general|albeit non optimised|technique to carry out this label elimination task. A label elimination performed to optimise code computation (or its form) is under study.
its usage|for example in bisimulation computation|starts from the observation that only the computation of a bounded number of digits is actually necessary to realise all the inequalities in any given set system.
The authors thank Eugenio Omodeo for very pleasant and fruitful conversations, and an anonymous reviewer for his/her comments.