A semantic construction of two-ary integers

Gabriele Ricci

April 26, 2004

Abstract. To binary trees, two-ary integers are what usual integers are to natural numbers, seen as unary trees. We can represent two-ary integers as binary trees too, yet with leaves labelled by binary words and with a structural restriction. In a sense, they are simpler than the binary trees, they relativize. Hence, contrary to the extensions known from Arithmetic and Algebra, this integer extension does not make the starting objects more complex.

We use a semantic construction to get this extension. This method differs from the algebraic ones, mainly because it is able to find equational features of the extended objects. Two-ary integers turn out to form the free algebra corresponding to the Jónsson–Tarski’s “paradoxical” equations. This entails that they have a sum extending the usual sum as well as other operations of higher “dimensions”.

In Programming, we use usual integers as address jumps for a direct access usual (“unary”) memory. Such a memory differs from the (virtual) memory of LISP programming language which is both binary and sequential (to reach a location we need to pass through intermediate locations). Even unary memories can be sequential (the tape of a Turing machine), yet we know that a direct access one works better. This carries over to the binary case: two-ary integers can provide LISP memories with convenient direct access jumps and the above low complexity hints at feasible hardware implementations.

Key words: universal matrix, analytic monoid, LISP, semantic, jump.

0 Preliminaries

0.0 Extending a generalization. Two-ary integers generalize integer numbers: as the latter integers extend natural numbers, they have to extend some generalization of natural numbers in a similar way. Then, the latter generalization will identify the former.

There are different generalizations of natural numbers depending on how we see them. For instance, if we see a natural number as a word on a singleton alphabet, then a larger alphabet, let us say a binary one, will define such a generalization as binary words. This is to say that we replace the single unary operation of successor with two unary ones, while keeping a single zero and a single partial predecessor. Then, the extension will concern such words.

M. Servi introduced such an approach in [22] by his “clan”’s. They inhabit the single infinite binary tree corresponding to the words to be extended: its root is the zero (or empty word) and its finite sub-paths from the root are such words. Clans consist of relational structures with one predecessor and two successors as for the words they extend. Their ensuing theory reached results of an order-theoretic interest [23] – [25].

Our approach, on the contrary, comes from seeing a natural number as a unary tree, a finite chain with the zero leaf. Then, binary trees will exemplify the generalization we want to extend. Hence, we now start from a single binary successor operation with two partial predecessors and any number of “zeroes”.

Natural numbers are “unary”, because we can think of them as the terms of a singleton unary species (according to Peano’s axioms). Hence, one might well think of the “two-ary” natural numbers as the terms for the singleton binary species on arbitrary unknowns (the “zeroes”). Such an algebraic view does not solve the problem of extending them in a way close to the unary extension(s), yet it serves to introduce it.

0.1 The extension problem. The usual construction of integers by algebraic extension starts from N × N, the set of pairs ⟨m, n⟩ of natural numbers, and divides it by the equivalence ≡, such that ⟨m′, n′⟩ ≡ ⟨m′′, n′′⟩ iff m′ + n′′ = m′′ + n′. In the two-ary case, this does not work because the “sum” does not merely involve two binary trees, but two (indexed) forests of them (see the term matrix product in 1.6 and 1.7 (B)).

Then, one might resort to the Universal Algebra construction of free algebras from their equational specifications. One could use it also for the usual integers from the two equations stating that a unary successor is the inverse of a (total) unary predecessor. Unfortunately, this abstract construction is not an extension. It looses the link with the unary or binary trees concerned.

Furthermore, one has to guess both the freedom and the new equations. On the contrary, they are what we want to prove and find in the two-ary case. Then, we need a third way to build two-ary integers. 0.2 Semantic constructions are intermediate between algebraic extensions and equational constructions. As the former, they start from the objects we want to extend, yet they do not involve their “sums” (universal matrix products [20]). As the latter, they require to guess the species of the extended algebra, yet neither its freedom nor its equations.

To introduce this new idea let us outline how it could work in the familiar case of usual integers. We do from the point of view of a programmer, who considers an integer j − i as the jump from a present address i to a new address j in a direct access standard memory. This also serves to introduce the LISP addressing problem of 0.4.

Without the direct access capability, our programmer has a sequential memory: a semi-infinite Turing tape. He can go from address i to any j through some finite succession of two “atomic” jumps: an upward one, +1 for successor, and a downward one, −1 for predecessor, where +1: N → N, while −1 only is a partial function.

Formally, all such successions form the minimal set T such that it contains the empty succession, ∅, and is closed under atomic jumps, {+1, −1} × T ⊆ T. Hence, they are the terms (words) for a binary species of unary “symbols”. We use such functions as “symbols” also because different practices, as the ones of Algebra, can reach inconsistencies as 1.5 will recall.

These binary word have a natural functional “semantic”. In fact, we can define the semantic s_{w} of word w ∈ T by word induction as

s_{∅} = i_{N} ,
s_{⟨+1,v⟩} = +1 · s_{v} and
s_{⟨−1,v⟩} = −1 · s_{v} ,  (1)

where · denotes functional composition as in 0.5. For instance, s_{⟨+1,∅⟩} = +1 and in general any semantic is a partial function, s_{w} ⊆ N × N.

Then, we consider the domain Δ_{w} ⊆ N of the semantic of any word w, called the domain induced by w, which is a co-finite segment. For instance, by (1) Δ_{⟨−1,v⟩} ⊂ N is the set of positive natural numbers, because we cannot backtrack our tape below its beginning. Clearly, such domains form a semilattice with zero (N itself) under containment.

Two words can have different equivalent semantics. For instance, ∅ has the identity on all natural numbers, whereas for ⟨+1, ⟨−1, ∅⟩⟩ by (1) the identity is on the positive ones only. Clearly, this equivalence is defined by the relation ≍ on T such that v ≍ w iff s_{v}(i) = s_{w}(i) for all i ∈ Δ_{v} ∩ Δ_{w}, which forgets the above finite domain differences.

Trivially, we also got a congruence of the term algebra. Then, its congruence classes are made of binary words, not of the pairs ⟨n, m⟩ for ≡ in 0.1. Yet, the two equivalences easily identify each other. The canonical representatives of the latter classes, pairs as ⟨0, m⟩ or ⟨n, 0⟩, correspond to similar canonical representatives: all words on a single “symbol”.

Canonical representatives are the only interesting ones for our programmer. Among several other properties, they have maximal induced domains in each congruence class, i.e. the maximal addressing ability.

Such a semantic construction of integers works as the one of algebraic extension, yet it did not use sums. Moreover, from it we can easily prove, not just guess, the freedom of the quotient algebra, which comes from the numbers under extension, as well as the two inversion equations of 0.1. This now does not matter, as usual integers are well-known. It will do with new numbers.

0.3 Universal matrices. Seemingly, the semantic construction has a drawback: the quotient of the term algebra does not provide the new numbers with their (new) “sum”, contrary to what the algebraic extension did through the old sum. Actually, this pertains to the new corresponding arithmetic, a development beyond the present step.

In the unary case, integer arithmetic provides direct access memories with the most of their gains. It allows our programmer to compute an address before using it. Without it, he could merely access fixed locations bypassing other locations, whereas address computations allow him memory relocations, addressing in many-dimensional arrays, hashing and so on.

However, another unconventional tool, the universal matrices [13] – [20], always assure that a new arithmetic exists with at least some minimal features, once a semantic construction has reached a free algebra.

Universal (“square”) matrices are to any universal based algebra what usual square matrices are to a finitely based vector space: there always is a new binary associative operation (the “matrix product”) on them, together with properties relevant to the original algebra, and an heterogeneous one (the “Menger system” corresponding to the product of a vector times a matrix). In case of a one-dimensioned vector space, the two operations are almost the same: the product of the underlying field.

In the above unary case, the term algebra only has a singleton base and again both operations essentially coincide. Now, we get the integer sum, while its algebra relevant properties are the ones of integer arithmetic.

In case of two-ary integers, the details of their new arithmetic have to await the application of the theory of universal matrices to the based algebras coming from the present semantic construction. Still, we will already find an associative sum and other uncommon features of some practical interest.

0.4 Set-interpretative LISP semantic. While natural numbers can be addresses for actual memories, binary trees are the basic structure for the virtual memories of some high level programming languages, the earliest of which is LISP. Then two-ary integers will serve to “jump” from one such tree to another or from one their forest to another in the same way a usual integer does from a standard memory location to another.

Actually, such jumps will appear as wide memory reorganizations. To help programmers to grasp them, we borrowed from LISP some basic terminology. Yet, their corresponding notions are set-theoretical.

Our semantic construction will also provide a small part of LISP with a semantic, oriented more to its set-theoretical interpretation than to its set-theoretical formalization. This “set-interpretative” semantic does use set-theoretical formalism, like the set-theoretical semantic of (a wider part of) LISP in [10], yet it does not formalize how an actual computer has to behave under LISP instructions. It merely tries to interpret the settheoretical meaning of a few LISP structures and instructions.

The recalled set-theoretical semantic succeeded in providing present day LISP with predictability results for computations on present day computers.

Our set-interpretative one, on the contrary, hints at possible small extensions of LISP and of computer architecture: a new data type, the “jump”, and a new arithmetical register, the “two-ary” adder. Jumps are canonical representatives of two-ary integers. Two-ary adders should perform “sums” on them to enable index registers to directly “access” a (reorganized) tree structured memory.

However, our set-theoretical notions merely formalize intensional ideas, namely they ideally come from Combinatory Logic as LISP did. In 1.9 we will hint a possible further connection with Combinatory Logic that also concerns Algorithmic Information Theory.

0.5 Notation. We give up any efficient functional notation for the one of Calculus, where repeated functional applications alternate subscripting and right parenthesizing. In spite of this choice of conventional notation, the foundation chosen here is the pure set–theoretical one not the conventional algebraic one, as motivated in 0.6 of [20].

Hence, we conform to [12], but for the following few differences. We denote the set-theoretical pair {{a}, {a, b}} by ⟨a, b⟩, yet we still simplify f(⟨a, b⟩) into f(a, b) and ⟨⟨x, y⟩, z⟩ into (x, y, x) as in [12]. For instance, we write the basic property of pairs of I.1.33 ibid. as

⟨t′, t′′⟩ = ⟨v′, v′′⟩ iff t′ = v′ and t′′ = v′′  (2)

and from the regularity axiom of Set Theory in I.1.18 of [12] we get

a, b ≠ ⟨a, b⟩ .  (3)

PX denotes the set of subsets of set X and i_{X} its identity function. Contrary to [12], see [18], we consider functional composition as the restriction of relational composition, namely f · g is “the composition of g and f” and (f · g)(x) = f(g(x)). Accordingly, we perform the restriction of a function f to some set S merely by functional composition: f · i_{S}.

As usual, we write f: A → B to say that f is a function with arguments in the whole set A and values in B, f: A ↦B or f: A→^{≻}B to say that it also is one to one or onto B and f: A ↦^{≻}B to say it is a bijection onto B. Yet, as motivated in 0.6 of [20], we will forget that “function – domain” and “family – index” are pairwise synonymic and we avoid the notation {a_{i}}_{i∈I} or (a_{i} | i ∈ I). Within informal comments we will replace “function” with “labelling”, to emphasize arguments, and with “indexing”, to emphasize values. Also, we denote the set-theoretical power ^{A}B = {f | f : A → B} as the arithmetic one B^{A}. (The latter will not occur here.)

1 S-terms and search terms

1.0 Definitions. Given any set U, consider the class of the sets T′ containing it and closed under pairing. It has a smallest set, T = ⋂{T′ | U ⊆ T′ and T′ × T′ ⊆ T′}. In fact, this intersection is one of such T′’s,

U ⊆ T and  (4)
T × T ⊆ T  ,  (5)

as one could easily check by considering any u ∈ U and any ⟨t′, t′′⟩ ∈ T × T. Often, we deal with subsets of T and, to get T′ = T, the trivial consequence

T′ ⊇ T  (6)

can replace the full induction principle that we will state in 1.3 (A). Then, let D = T × T, which by (5) is a subset of T. We easily get

U ∪ D = T .  (7)

In fact, U ∪ D ⊆ T follows from U, D ⊆ T, while U ∪ D ⊇ T from U ∪ D being such a superset T′, because the closure under pairing follows from (4) and (5) by the distributivity of × with respect to ∪ (see I.3.13 (e) in [12]) through the preservations of inclusions by cartesian products.

If

U ∩ D = ∅ ,  (8)

then we say that U is a set of unknowns for pairing and that T is the set of two-ary natural numbers on U. We will denote T by N_{2}(U) to specify its unknowns. For example, N_{2}(1) is the set of two-ary natural numbers on the single unknown ∅, because U = {∅} = 1 satisfies (8), since a pair cannot be empty whereas our unknown u = ∅ is.

One might well think of two-ary natural numbers as terms of a species with only one binary operation symbol. Since it is the only operation symbol, we do not need to specify it.

We will use several U’s. We choose one of them as a “main” U, we call atoms its elements and S-terms on U the corresponding two-ary natural numbers. Hereinafter, we reserve notation T for their set, unless otherwise stated, whereas for any other U′ we use N_{2}(U′). We call dyads the pairs forming D.

The “S” in “S-terms” recalls the “S-expressions” of LISP [29]. Actually, the letter “D” and the word “dyads” are a notational abuse with respect to Combinatory Logic [6], where such pairs correspond to the terms composed by combinatory application, whereas “D” and “dyads” denote the combinators modelling set-theoretical pairs, or remodelling combinatory application within combinatory calculus.

LISP assumes an enumerable infinite set U of atoms: variable-length words. For now, we do not. Still, we can well assume U ≠ ∅, because in the opposite case T = ∅ and all the following theory becomes very trivial.

Under this assumption, T cannot be finite: its proper subset D = T × T should have more elements than T. Hence, hereinafter U ≠ ∅ and by (8) and (7) U and D define a bipartition of T.

We will also use some subsets of T. For every natural number n we define the set of full terms of height n, denoted by ⌊n⌋, by arithmetic induction as

⌊0⌋ = U and  (9)
⌊m + 1⌋ = ⌊m⌋ × ⌊m⌋ .  (10)

(It is easy to show that ⌊n⌋ ⊂ T.) Among them we also consider the ones built from a single atom u ∈ U ≠ ∅. We define their set ⌊n⌋_{u} ⊆ ⌊n⌋ ⊆ T, called the set of the full u-terms (of height n), by replacing (9):

⌊0⌋_{u} = {u} and  (11)
⌊m + 1⌋_{u} = ⌊m⌋_{u} × ⌊m⌋_{u} .  (12)

Clearly, every ⌊n⌋_{u} is singleton.

1.1 Definitions. Now, let us idealize the cons, car and cdr commands of LISP by respectively defining the functions dyad of, left of and right of

d: T × T ↦^{≻}D , l, r: D→^{≻}T , i.e. d, l, r: T × T → T  (13)

by d(t′, t′′) = ⟨t′, t′′⟩ ,  (14)

l(t′, t′′) = t′  and  (15)
r(t′, t′′) = t′′  for all t′, t′′ ∈ T .  (16)

Notice that, while l and r are nontrivial functions (the ones that extract the components of a pair), d merely is the identity on D. Of course, this is not the way any LISP transducer (either compiler or interpreter) behaves, since among other things it has to exploit memory efficiently: the car and cdr are reading instructions on already filled cells, whereas cons, a write instruction, fills a new cell when needed. This allows a LISP program to get any S-expression without wasting memory by a runtime dynamic allocation of cells.

However, if, for a while, one assumes to have a “large” ROM memory, filled with all written cells one will use, then one can implement cons too as a read instruction merely by (the computation on pointers corresponding to) our identity, seen as a binary operation. One might think to ideally replace the actual runtime dynamic allocation of cells with a static “expensive” one.

We also do not need to distinguish between a command identifier and what the command does, as 1.3 (C) and 1.5 will show, and, for the purposes of this work, one might well call the three functions d, l and r “search commands”. Yet, they are dependent on our U. For later purposes, independent search commands will be convenient. Then, we refer to the set of atoms U = 1 and we denote the three corresponding functions by d, l and r.

Therefore, we call the three functions d, l, r: N_{2}(1) × N_{2}(1) → N_{2}(1) search commands. Anyway we boldfaced them, like as the “operation symbols” of [5] in order to help algebraic readers, unfamiliar with 1.5.

The (last two) search commands define the set T of the (unary) search terms by

{∅} ⊆ T and  (17)

(T ∪ {l, r}) × T ⊆ T ,  (18)

namely, T is the minimal set (as T was in 1.0) satisfying them or satisfying the following ones:

∅ ∈ T  ,  (19)
t′, t′′ ∈ T imply ⟨t′, t′′⟩ ∈ T and  (20)
t ∈ T implies ⟨l, t⟩, ⟨r, t⟩ ∈ T .  (21)

A reason to possibly call “terms” such objects is given in 1.3 (C), 1.4 and 1.5, where we show that they behave as the terms for a species with one (omitted) binary symbol and two unary ones. There, we also show that the set of “search unknowns” is the singleton 1 = {∅} as for N_{2}(1). Hence, here one might call “unary” such terms. The proof that larger arities are not necessary pertains to the (later) arithmetical development. In the same way we got (7), we still have

{∅} ∪ (T ∪ {l, r}) × T = T .  (22)

Also, notice that

l ≠ r and l, r ∉ T .  (23)

In fact, by (3) l(∅, ⟨∅, ∅⟩) = ∅ ≠ ⟨∅, ∅⟩ = r(∅, ⟨∅, ∅⟩) and, since N_{2}(1) = Dom l = Dom r, the sets l and r are infinite as N_{2}(1) is, whereas by (22) every t ∈ T is finite. (The same holds for l and r, since U ≠ ∅.)

We also define two subsets of search terms. The set N_{2}(1) ⊆ T of the upward paths is the one of the search terms we get by (19) and (20) only and the set W ⊆ T of the downward paths or (search) words by (19) and (21) only. To define both subsets we used the usual minimality assumptions, which also imply such inclusions.

Hereinafter, “word” will only denote such binary words, unless otherwise stated. As usual, the length of a word is the number of the “induction steps generating it”. (We are omitting their formal definition that here would occur only after 1.3 (D).)

Given a word, we consider its letters construction–ordered, not ordered by reading them, e.g. in (l, r, ∅) = ⟨l, ⟨r, ∅⟩⟩ its first letter is r, while l is the last. In our notation we will also keep the generator ∅, though necessary only with the empty word. When words occur in search terms, it is a useful landmark that improves reading.

Then, we define another identity function

τ: (T ∪ {l, r}) × T → T by τ(x, t) = ⟨x, t⟩ ,  (24)

for all x ∈ T ∪ {l, r} and t ∈ T. As we will show in the proof of 1.3 (C), one might well think of it as the definition of three operations on T, called τ-operations,

τ′_{d}: T × T → T, τ′_{l}, τ′_{r}: T → T  (25)

by

τ′_{d}(t′, t′′) = ⟨t′, t′′⟩ , τ′_{l}(t) = ⟨l, t⟩ and τ′_{r}(t) = ⟨r, t⟩ .  (26)

for all t, t′, t′′ ∈ T.

1.2 Examples. The formal notation for search terms allows us to see their structure as long as they are small: ∅, ⟨∅, ∅⟩, ⟨l, ∅⟩, ⟨r, ∅⟩. Bigger terms, as ⟨(l, l, ∅), ⟨r, ∅⟩⟩ and ⟨(l, l, ∅), ⟨(l, r, ∅), (r, r, ∅)⟩⟩, needs some graphical support, as in fig. 1 and fig. 2 respectively. There, we adapted the standard diagrams for algebraic terms (vertex-labelled trees). For later purposes, more proper diagrams are the directed acyclic graphs we get from them by collapsing all identical subterms, e.g. fig. 2 will become fig.3.

[figure: l; l; ∅; ∅; r; Fig. 1; l; l; ∅; l; r; ∅; r; r; ∅; Fig. 2; l; l; r; ∅; l; r; Fig. 3]

1.3 Lemata. (A) The sets U and T and the binary operation d satisfy the three Peano properties

d(t′, t′′) ∉ U for all t′, t′′ ∈ T ,  (27)
d: T × T ↦^{≻}D , i.e. d^{−1}: T ∖ U ↦^{≻}T × T ,  (28)

and, for all sets T′,

T′ ⊇ T iff \{ \begin{matrix}U ⊆ T′ & and, for all t′, t′′ ∈ T , \\ t′, t′′ ∈ T′ & imply d(t′, t′′) ∈ T′ . \end{matrix}  (29)

(B) The left and right functions provide the dyad function with a partial “binary” inverse

d(l(t), r(t)) = t for all t ∈ D ,  (30)
l(d(t′, t′′)) = t′ and  (31)
r(d(t′, t′′)) = t′′ for all t′, t′′ ∈ T .  (32)

(C) The sets 1 = {∅} and T and the function τ satisfy the Peano properties

τ^{−1}: T ∖ {∅} ↦^{≻}(T ∪ {l, r}) × T , hence  (33)
τ(x, t) ≠ ∅ , for all x ∈ T ∪ {l, r} and t ∈ T ,  (34)

and, for all sets T′,

T′ ⊇ T iff \{ \begin{matrix}1 ⊆ T′  and, for all & x and all t ∈ T, \\ x ∈ (T ∩ T′) ∪ \{l, r\} and t ∈ T′ & imply τ(x, t) ∈ T′ \end{matrix} (35)

(that one could well restate by means of the operations τ′_{d}, τ′_{l} and τ′_{r}). (D) For all sets T′,

T′ ⊇ W iff \{ \begin{matrix}1 ⊆ T′ & and, for all t ∈ W , \\ t ∈ T′ & implies ⟨l, t⟩, ⟨r, t⟩ ∈ T′ . \end{matrix}

Proofs. (A) Condition (27) is a restatement of (8). As motivated in 1.4 (A), it corresponds to Peano’s first axiom. Condition (28), comes from defining d as an identity on set-theoretical pairs. It corresponds to Peano’s axioms about successor and uniqueness of predecessor, since we can rewrite it as d: T × T ↦T.

The last condition corresponds to Peano’s induction axiom. Its (only if) part easily follows from (4) and (5) by the transitivity of ⊆. To prove its (if) consider T′′ = T ∩ T′. Our premises get T′′ ⊇ T as it was for T′ in (6). Hence, T′ ⊇ T.

(B) To prove (30), consider that by (28) for every t ∈ D there are t′, t′′ ∈ T such that ⟨t′, t′′⟩ = t. Then, d(l(t), r(t)) = d(l(⟨t′, t′′⟩), r(⟨t′, t′′⟩)) = d(t′, t′′) = ⟨t′, t′′⟩ = t by (14) – (16). Such definitions also prove (31), l(d(t′, t′′)) = l(t′, t′′) = t′, as well as (32) (after replacing r for l).

(C) At now, contrary to (A), we do not need a disjunctive assumption, like as (8), to prove (34). In fact, ∅ can never be any of such pair composed terms, because pairs never are empty. See 1.31 in [12] and 3.1 in [15].

The identity argument, used in (A) for (28), still holds for (33). However, now (33) enables any nonempty term t to have a single decomposition within three sorts (t = ⟨t′, t′′⟩, ⟨l, t′⟩, ⟨r, t′⟩) that are disjoint because of (23). This allows us to see τ as the τ′ of (26). Yet, we cannot think to always replace τ or τ′ by an “absolutely free algebra” for one binary and two unary operations, because of an inconsistency we are going to show in 1.5.

Finally, one could prove the induction principle in (35) in the same way we did in (A).

(D) Same proof as in (C), but for the case t = ⟨t′, t′′⟩ that drops out. Q.E.D.

1.4 Inductions. (A) When we replace a (properly chosen) unary operator, say S, for our (binary) dyad operator in (5) and a proper singleton set for U, definition 1.0 becomes the one of a model of natural numbers, where (8) or (27) corresponds to the first Peano’s axiom, while (28) to the second. Then, the proper choice of S will provide Peano’s induction axiom with a proof within the model (e.g. see 2.4.1 in [2]). Hence, the properties in 1.3 (A) are to S-terms what Peano’s axioms are to natural numbers.

We can restate this correspondence for 1.3 (C), but for two details. The former is the occurrence of two other (unary) “successors”, τ′_{l} and τ′_{r}, in addition to the binary one τ′_{d} replacing the d of 1.3 (A). The latter is that we replace the given set 1, as the recalled model did, for the undeterminate one U. This allowed us to omit an assumption like as (8). In fact, {∅} ∩ (T ∪ {l, r}) × T = ∅, because pairs never are empty.

In 1.3 (D) things are as in 1.3 (C). There, we omitted the statements corresponding to the initial Peano’s axioms, because they were trivial cases (restrictions) of the ones in 1.3 (C). Yet, all such statements, as well as (28), are mathematically necessary as the counterexample in 1.5 will show.

(B) We will call the Peano induction principle in (29) T -induction, or in case of upward paths upward induction, the one in (35) T -induction or bold induction, and the one in 1.3 (D) for words word induction. We will introduce another induction for a third subset of T in 4.0 and 4.1 (E). Seldom, we will also exploit Peano’s induction, which we call arithmetic induction.

We will use the above Peano induction properties, as well as the ones we will introduce, both for proving statements and for defining functions (or predicates). In the former case the sets T′ of 1.3 are the ones where a statement holds. In the latter, they are the “sets where a function is being defined” (not the domains of a defined function). They are not settheoretical sets, since our Set Theory does not define “to define”.

Therefore, in the latter case one should prove the existence of the function to be defined. One could do it by proving corollaries of the general recursion principle in 2.13.1 of [12]. Such proofs contain several uninteresting details (but one) and we will follow the algebraic practice of taking “algebraic recursion” as granted.

Yet, we cannot follow Algebra in calling our inductions “recursions”. In fact, they will correspond to the arithmetical case of “induction”, which is intermediate between primitive recursion and iteration, where the function defining the induction step is constant with respect to the induction variable.

We can expect that in two-ary arithmetics the cases corresponding to primitive recursion and recursion will occur. Hence, to keep the word “induction” as in (unary) Arithmetic serves to save “recursion” for future proper uses. Here, we will not state any general recursion principle for any of our terms. The only recursion, we will use, concerns words, yet it will come from word induction through word reversals, without such a general principle.

Furthermore, we cannot disregard one of the details of the corollaries we are omitting, as Algebra does. It concerns a well-founded relation occurring in the above mentioned recursion principle. To get this condition of being well-founded we stated the firsts of Peano axioms.

Without them one cannot define predicates nor functions on the terms concerned, for the very reason one cannot do on natural numbers: without such Peano’s axioms the base part of a definition contradicts its induction part, unless the defined object is a constant.

1.5 Counterexample. We can see how the above contradiction rises, when we deny (8), i.e. within two-ary natural numbers. Assume we define the depth d(t) of a term t by (29) as

d(u) = 0 , for all u ∈ U ,
d(t′, t′′) = 1 + max(d(t′), d(t′′)) , for all t = ⟨t′, t′′⟩ ∈ D .

Let u ∈ U. Without (8), U can well contain ⟨u, u⟩. In such a case d(u, u) = 0 by the former step as well as d(u, u) = 1 by the latter. Hence, the function d was misdefined.

If we keep (4), this misdefinition has to occur even if we change the construction in the induction step (5): just replace ⟨u, u⟩ by the new corresponding object. We have to stress this, because sometimes people in Algebra and Logic (but for [6]) try to weaken (or omit) (8) through such changes. For instance, a proper choice of operation symbols should allow any set to play the rôle of a set of “variables” and get a “symbolic term” functor.

It does not matter whether the construction in an induction step uses “good operation symbols” (nor whether one fails to specify such a construction, as when one states that a composed term is a word, without defining words). If the construction is not trivial, it will anyway build new terms other than the generators and any such term is a possible extra element for another “inconsistent” set of generators, as ⟨u, u⟩ was.

Algebraically, such inconsistency is the lack of independence within the algebra of terms, while set-theoretically it prevents the recursion principle mentioned in (B) to have its well-founded relation. Disjunction assumptions, like (8), cannot become weaker.

Hence, there are not functions sending an arbitrary set of generators into a nontrivial set of terms on such generators: “symbolic term” functors cannot exist. A formal proof of this is in lemata 7.3 (A) and (B) of [14].

On the contrary, there are sets that are made only of unknowns for whatever algebraic species we choose, as shown in 3.1 in [15]: while one cannot freely choose generators, then we always can freely choose operation symbols, contrary to Algebra.

The only hope to use an arbitrary set U of algebraic “variables” might be to give up inclusion assumptions, like as (4). For instance [8] claims to be able to do so by replacing the injection i_{U}: U ↦T, as in (4), by another (burdensome) injection j: U ↦T. Yet, it does use (4) wherever.

Anyway, whatever j we choose to replace i_{U}, this is tantamount to replace U ⊆ T by V ⊆ T, where V is the j-image of U. Then, the set of generators is V that is not arbitrary. The only way to use arbitrary U’s is not to use their elements as generators, contrary to what we want. The so called “absolutely free” algebras behave like as all other free algebras: one cannot choose a base at will.

Within Set Theory we always have to (carefully) define unknowns for any nonempty species, whereas operation symbols (including the nullary ones) can be freely chosen depending on the application. As the latter freedom is consistent, in 1.1 we are exploiting it for the unary “symbols” and — in a sense — for the omitted binary one. 1.6 Definitions. Given two search terms u, v ∈ T, define u ⊕ v, the catenation of v with u, by bold induction on v, as

u ⊕ ∅ = u,  (36)
u ⊕ ⟨t′, t′′⟩ = ⟨u ⊕ t′, u ⊕ t′′⟩ ,  (37)
u ⊕ ⟨l, t⟩′ = ⟨l, u ⊕ t′⟩ and u ⊕ ⟨r, t′⟩ = ⟨r, u ⊕ t′⟩ ,  (38)

for all t′, t′′ ∈ T. Hence, we defined a binary operation ⊕: T × T → T. As 1.7 (A) will show ⊕ and ∅ define a monoid on search terms. Later on, we also will use the (reversed) catenation monoid that we define by commuting ⊕, namely there the monoid composition of v with u is v ⊕ u.

Catenation allows us to define the reversed w^{↩} of every word w ∈ W by word induction, ∅^{↩}= ∅, ⟨l, v⟩^{↩}= ⟨l, ∅⟩⊕ v^{↩} and ⟨r, v⟩^{↩}= ⟨r, ∅⟩⊕ v^{↩}. We omit the proof that reversal is a permutation, ^{↩}: W ↦^{≻}W. Yet, we will use this when, while defining or proving something about any w^{↩} inductively, we will say that we do about w by backward induction on w.

By catenation we also define a search increment function η^{∘}: T → T T by

η^{∘}_{u} (t) = u ⊕ t , for all t, u ∈ T .  (39)

Here and whenever the letter η will occur, it denotes a function that \underline{e}xtends its argument to some \underline{e}ndomorphism. For the present occurrence, this will be shown in 1.7 (A).

On S-terms and two-ary natural numbers, on the contrary, we define a heterogeneous operation ˆ+ : T^{U} × T → T, we call upward addition, by T - induction on the latter argument: for all M: U → T, u ∈ U and ⟨t′, t′′⟩ ∈ D,

M ˆ+ u = M(u),  (40)
M ˆ+ ⟨t′, t′′⟩ = ⟨M ˆ+ t′, M ˆ+ t′′⟩ .  (41)

By it we also define the (bottom) term increment function η̂: T^{U} → T^{T} by

η̂_{M}(t) = M ˆ+ t , for all M: U → T and t ∈ T ,  (42)

where we call function M the increment matrix, and the term matrix product ⋄: T^{U} × T^{U} → T^{U} by

(M ⋄ L)(u) = M ˆ+ L(u) , for all L, M: U → T and u ∈ U .  (43)

Again, we call M ⋄ L the product of L times M. ([18] shows the necessity of such reversed readings.) As 1.7 (B) will show, ⋄ is the composition of a monoid with unit i_{U}. Hence, from this product we can define a term matrix power by iteration:

M^{⟨0⟩} = i_{U}  (44)
M^{⟨m+1⟩} = M^{⟨m⟩} ⋄ M or M^{⟨m+1⟩} = M ⋄ M^{⟨m⟩} .  (45)

We can see the tree of η̂_{M}(t) and M ˆ+ t as the S-term tree we get from the one of t by replacing each leaf u ∈ U in it with the tree of M(u). When we have a matrix L: U → T, we see an “indexed forest” of such trees t and the product of L and M corresponds to the indexed forest we get by sprouting each tree t of the former in the same way as above. Fig. 4 shows such sprouts from circled nodes for U = {u, v}.

[figure: u; v; u; v; u; \overbrace{u  v}^{M}; ⋄; u; u; v; u; v; \overbrace{u  v}^{L}; Fig. 4; =; u; v; u; u; v; u; v; u; v; u; u; v; u; \overbrace{u  v}^{M⋄L}]

Given any natural number n, the product ∏_{u∈U}⌊n⌋_{u} is singleton, since by (11) and (12) every factor is. We call its element C_{n}: U → T the full matrix of height n. Hence, by (11) and (12) respectively

C_{0} = i_{U},  (46)
C_{n+1}(u) = ⟨C_{n}(u), C_{n}(u)⟩ .  (47)

When M = C_{n} is a full matrix of some positive height, n > 0, we call its increment η̂_{M}: T → T a full increment.

A matrix M: U → T can have a fixed value t = M(u), for all u ∈ U. We call it a constant matrix and we denote it as M = K_{t}, where function K is a generator of constants defined by

K_{t}(u) = t ,  (48)

for all t ∈ T and u ∈ U and, clearly, K: T ↦T^{U}. Later on, we will use other generators of constants (where t and u belongs to other sets), yet we will not repeat (48).

Consider a function h: T → T such that, for all t′, t′′ ∈ T,

h(t′, t′′) = ⟨h(t′), h(t′′)⟩ ,  (49)
h(l, t′) = ⟨l, h(t′)⟩ and h(r, t′) = ⟨r, h(t′)⟩ .  (50)

We call h a search endomorphism and denote the set of all such h’s by E_{τ} ⊆ T T. Clearly, E_{τ} is the carrier of a monoid of functional composition (i_{T} ∈ E_{τ} and h′′ · h′ ∈ E_{τ} for all h′, h′′ ∈ E_{τ}) that we call the search endomorphism monoid. Then, define the search endomorphism representation r^{∘}: E_{τ} → T by

r^{∘} (h) = h(∅) , for all h ∈ E_{τ} .  (51)

Finally, in case of S-terms, we define the term endomorphisms as the functions l: T → T such that

l(t′, t′′) = ⟨l(t′), l(t′′)⟩ , for all t′, t′′ ∈ T  (52)

and we denote their set by Ê. Again, we get a monoid of functional composition on it, which we call the endomorphism monoid of S-terms. Then, define the term endomorphism representation r̂: Ê → T^{U} by r̂(l)_{u} = l(u) , for all l ∈ Ê and u ∈ U, namely by

r̂(l) = l · i_{U} , for all l ∈ Ê .  (53)

Clearly, there are functions l: T → T which are not term endomorphisms, i.e. not the endomorphism of d: T × T → T. On the contrary, any f: T → T is an endomorphism of l, r: T × T → T, because by 1.1 for instance we have

l(f(t′), f(t′′)) = f(t′) = f(l(t′, t′′)) , for all t′, t′′ ∈ T .  (54)

Then, Ê is the set of endomorphisms of all d, l, r: T × T → T.

1.7 Theorems. (A) The search increment function is the inverse of the search endomorphism representation and the image under such a representation of the composition of search endomorphisms is catenation. Hence, r^{∘}: E_{τ} ↦^{≻}T, η^{∘}: T ↦^{≻}E_{τ} and for all t, u ∈ T

(v ⊕ u) ⊕ t = v ⊕ (u ⊕ t) and  (55)
∅ ⊕ t = t ⊕ ∅ = t .  (56)

(B) The term increment function is the inverse of the term endomorphism representation and the image under such a representation of term endomorphism composition is term matrix product. Hence, r̂: Ê↦^{≻}T^{U}, η̂: T^{U} ↦^{≻}Ê and for all L, M: U → T and t ∈ T

(M ⋄ L) ˆ+ t = M ˆ+ (L ˆ+ t) and  (57)
i_{U} ˆ+ t = t .  (58)

Proofs. (A) At first, let us show that η^{∘} · r^{∘}= i_{E_{τ}}. We prove η^{∘}_{r^{∘}(h)} (t) = h(t), i.e. we prove

h(∅) ⊕ t = h(t) ,  (59)

for all h ∈ E_{τ} and all t ∈ T by bold induction. The basis step, h(∅) ⊕ ∅ = h(∅), immediately follows from (36).

When t = ⟨t′, t′′⟩ and h(∅) ⊕ h(t′) = h(t′) and h(∅) ⊕ t′′ = h(t′′), by (37) and (49) h(∅) ⊕ t = ⟨h(∅) ⊕ t′, h(∅) ⊕ t′′⟩ = ⟨h(t′), h(t′′)⟩ = h(t). When t = ⟨l, t′⟩ and h(∅)⊕h(t′) = h(t′), by (38) and (50) h(∅)⊕t = ⟨l, h(∅)⊕t′⟩ = ⟨l, h(t′)⟩ = h(t). When t = ⟨r, t′⟩, merely replace l with r.

Now, let us prove that r^{∘} is onto T. The endomorphism conditions (49) and (50) allow (35) to define any h ∈ E_{τ} on the whole T by bold induction, once we have only chosen a value for h(∅). Hence, given any t ∈ T, we get an h ∈ E_{τ} such that r^{∘} (h) = h(∅) = t by merely choosing h(∅) = t.

Finally, we get r^{∘} (h′′)⊕ r^{∘} (h′) as the representation r^{∘} (h′′ · h′) of composition, for all h′′, h′ ∈ E_{τ}, merely by (59). In fact, by (51) this is to prove that h′′(∅) ⊕ h′(∅) = h′′(h′(∅)) and, if we set t = h′(∅) and h = h′′ in (59), we find that we already proved it by bold induction on h′(∅). Notice also that the consequence η^{∘} = r^{∘} ^{−1} allows us to rewrite r^{∘} (h′′)⊕ r^{∘} (h′) =r^{∘} (h′′ · h′) as η^{∘}_{v⊕u}=η^{∘}v · η^{∘}_{u} , where u =r^{∘} (h′) and v =r^{∘} (h′′). Hence, we get (55) by (39) after applying t to both sides, while (56) comes from η^{∘}_{∅}= i_{T} ∈ E_{τ}.

(B) Let us show that η̂ · r̂ = iÊ. We prove η̂_{r̂(l)}(t) = l(t), i.e. we prove

r̂(l) ˆ+ t = l(t) ,  (60)

for all l ∈ Ê and all t ∈ T by T -induction. The basis step, r̂(l) ˆ+ u = r̂(l)_{u}, immediately follows from (40).

When t = ⟨t′, t′′⟩ where r̂(l) ˆ+ t′ = l(t′) and r̂(l) ˆ+ t′′ = l(t′′), by (41) and (52) r̂(l) ˆ+ t = ⟨r̂(l) ˆ+ t′, r̂(l) ˆ+ t′′⟩ = ⟨l(t′), l(t′′)⟩ = l(t). Hence, we proved the induction step too.

Now, let us prove that r̂ is onto T^{U}. The endomorphism axiom (52) allows (29) to define any l ∈ Ê on the whole T by T -induction, once we have only chosen any value for l · i_{U}: U → T. Hence, given any t: U → T, we get an l ∈ Ê such that r̂(l) = l · i_{U} = t by merely choosing l · i_{U} = t.

Finally, we get r̂(l′′) ⋄ r̂(l′) as the representation r̂(l′′ · l′) of composition, for any l′, l′′ ∈ Ê, merely by (60). In fact, by (53) this is to prove that (l′′ ·i_{U})⋄(l′ ·i_{U}) = l′′ ·l′ ·i_{U} and, if we set t = l′(u) and l = l′′ in (60), we find that we already proved it by T -induction on l′(u), namely (l′′ · i_{U}) ˆ+ l′(u) = l′′(l′(u)) for all u ∈ U. Notice also that we can rewrite r̂(l′′) ⋄ r̂(l′) = r̂(l′′ · l′) as η̂_{M⋄L} = η̂_{M} · η̂_{L} , where L = r̂(l′) and M = r̂(l′′), since η̂ is the inverse of r̂. Hence, we get (57) by (42) after applying t to both sides and (58) comes from i_{T} ∈ Ê. Q.E.D.

1.8 Lemata. (A) The values of full increments are dyads: η̂_{M}: T → D , for every M = C_{n} with n > 0. (B) The height of a full matrix is the exponent of the term matrix power of C_{1} giving it: C_{n} = C_{1}^{⟨n⟩}. (C) Full increments are one to one. (D) Full increments do not have fixed points. (E) The restrictions of catenation to upward and downward paths are suboperations: for all u, t ∈ N_{2}(1) and v, w ∈ W, t ⊕ u ∈ N_{2}(1) and w ⊕ v ∈ W, where t ⊕ u = (t ⋄ u)(∅), when t, u: 1 → N_{2}(1), t(∅) = t and u(∅) = u. Namely, the generator of constants K: T ↦^{≻}T^{1} is an isomorphism from the former restriction of ⊕ onto ⋄: T^{1} × T^{1} → T^{1}, the term matrix product for the singleton U′ = 1.

Proofs. (A) Consider C_{n} ˆ+ t for n > 1 and all t ∈ T = U ∪ D. When t = u ∈ U, by (40) it is C_{n}(u) ∈ D because of (47). When t = ⟨t′, t′′⟩ ∈ D, by (41) it is ⟨C_{n} ˆ+ t′, C_{n} ˆ+ t′′⟩ ∈ D.

(B) Arithmetic induction on n. The basis step is in (46) and (44). The induction step comes from (45), (43), (47), (46), (41), (40) and (47): C_{1}^{⟨m+1⟩}(u) = (C_{m}⋄C_{1})(u) = C_{m} ˆ+ C_{1}(u) = C_{m} ˆ+ ⟨C_{0}(u), C_{0}(u)⟩ = C_{m} ˆ+ ⟨u, u⟩ = ⟨C_{m} ˆ+ u, C_{m} ˆ+ u⟩ = ⟨C_{m}(u), C_{m}(u)⟩ = C_{m+1}(u) for all u ∈ U.

(C) By (B) and 1.7 (B) any full increment is a positive power of functional composition for the full increment of C_{1}. Hence, we can merely show that the latter increment is one to one. By T –induction we show that for all t ∈ T, if C_{1} ˆ+ t = C_{1} ˆ+ d for some d ∈ T, then t = d.

When t = u ∈ U, C_{1} ˆ+ d = C_{1} ˆ+ t = ⟨u, u⟩ ∈ U × U by (40), (47) and (46). This implies that d ∉ D, since d ∈ D by (41) contradicts (A). Then, by (8) d ∈ U as t did and C_{1} ˆ+ d = ⟨d, d⟩ that by (2) gets t = d. Notice that we get this also from the symmetric assumption d ∈ U.

When t = ⟨t′, t′′⟩ where both t′ and t′′ satisfy our implication, d ∉ U as d ∈ U implies t = d ∈ U. Then, d = ⟨d′, d′′⟩ ∈ D and the implication premise gets ⟨C_{1} ˆ+ t′, C_{1} ˆ+ t′′⟩ = ⟨C_{1} ˆ+ d′, C_{1} ˆ+ d′′⟩ by (41), i.e. by (2) C_{1} ˆ+ t′ = C_{1} ˆ+ d′ and C_{1} ˆ+ t′′ = C_{1} ˆ+ d′′. Hence, t = ⟨t′, t′′⟩ = ⟨d′, d′′⟩ = d.

(D) We show that, when n > 0, C_{n} ˆ+ t ≠ t by T -induction on t. When t ∈ U, C_{n} ˆ+ t = C_{n}(t) ∈ D by (40) and (A), whereas t ∈ U and U ∩ D = ∅.

When t = ⟨t′, t′′⟩ and both C_{n} ˆ+ t′ ≠ t′ and C_{n} ˆ+ t′′ ≠ t′′, by (41) and (2) C_{n} ˆ+ t = ⟨C_{n} ˆ+ t′, C_{n} ˆ+ t′′⟩ ≠ ⟨t′, t′′⟩ = t.

(E) The trivial either upward or word induction on u and v respectively can exploit (36) and either (37) or (38). In the former case (37) becomes (41) through (43). Q.E.D.

1.9 Combinatory translators. Readers acquainted with Combinatory Logic will likely find an immediate example of term increment in the substitutions of combinatory terms for variables. When U is the set of atoms for (a set-theoretical model of) combinatory terms with reducible constants K and S as in [6], this occurs with any increment matrix M that keeps such constants: M(K) = K and M(S) = S.

However, such term increments make sense even without variables. For instance, when, U = {K, S}, namely for pure combinators, we can keep K only and replace S by B(BW)(BBC) in combinatory notation. This increment sends every combinator into an extensionally equal combinator that only sprouts the combinators B, C, K, and W, namely that belongs to N_{2}(U′) where the unknowns of U′ are the trees of the latter combinators. Within our K–S system, we see a translation of this system to the B–C–K–W system of chapter 5 of [3].

In general, U will contain more than two reducible constants and the matrix M: U → T more non trivial replacements. Then, η̂_{M}: T → T will be a “translator” between combinatory systems, namely an idealized compiler or translator between ideal programming languages. At a soft level, it performs what emulations between universal Turing machines do at the hard level.

(The formalization of G.J. Chaitin [0] implements such emulations by “unary increments”, viz. by catenations with a word prefix that identifies the Turing machine under emulation. Contrary to other attempts, it succeeded in proving the Minsky–Solomonoff’s conjecture [11] neatly: asymptotic invariance under such emulations defines algorithmic complexity, the quantity of “intrinsic information”. Among many results, a major result of Logic of the past century [1] followed from this.)

2 Semantics of search terms

2.0 Definition. Given any set of atoms U, the search commands d, l and r get their “execution meaning” merely from the functions d, l and r of (13) that we can also see as partial functions in P(T × T) , since T × T ⊂ T. Even the search terms become so through a function σ: T → P(T × T) that provides each search term t with its (pure) semantic σ_{t} ⊆ T × T, which is the function T -inductively defined for all t, t′, t′′ ∈ T by

σ_{∅} = i_{T} ,  (61)
σ_{⟨t′,t′′⟩}(t) = ⟨σ_{t}′(t), σ_{t}′′(t)⟩ , for all t ∈ Dom σ_{t}′ ∩ Dom σ_{t}′′ , (62)
σ_{⟨l,t⟩} = l · σ_{t} and σ_{⟨r,t⟩} = r · σ_{t} .  (63)

When Σ ⊆ P(T × T) denotes the σ-image of T, σ: T →^{≻}Σ, each f ∈ Σ is a partial function from T to T indexed by some t ∈ T, f = σ_{t}. It represents the “pure address jump” that enables any S-term of its domain to reach another S-term by the search term t. Hence, this direct addressing disregards the departure S-terms, yet it does so only within some domain. To denote it, we define the induced domain function Δ: T → PT by Δ_{t} = Dom σ_{t}, for all t ∈ T.

This domain is the whole T by (61), when t = ∅. Since by (62) ⟨t′, t′′⟩ keeps the common domain of t′ and t′′, Δ_{t}′ ∩ Δ_{t}′′, it will remain the whole T, as long as we build search terms by τ′_{d} only as in (20),

Δ_{u} = T for all u ∈ N_{2}(1) .  (64)

By τ′_{l} or τ′_{r}, on the contrary, it can narrow:

Δ_{⟨l,t⟩} = Δ_{⟨r,t⟩} ⊆ Δ_{t} .  (65)

In fact, since by (13) the domains of l and r are the proper subset D of T,

(63) states that only the t’s, such that σ_{t}(t) ∈ D, stay in this (narrower) domain. For example, Δ_{⟨l,∅⟩} = D ⊂ T = Δ_{∅}. From (62) we also get for every t ∈ T

Δ_{⟨t,t⟩} = Δ_{t} .  (66)

We can denote all upward paths by S-terms through the unlabel function ł : T → N_{2}(1) defined by T -induction as

ł (u) = ∅ , for all u ∈ U , and  (67)
ł (t′, t′′) = ⟨ł (t′), ł (t′′)⟩ , for all t′, t′′ ∈ T .  (68)

Clearly,

ł : T →^{≻}N_{2}(1) .  (69)

Since N_{2}(1) ⊆ T, this allows a two-ary natural number or S-term v ∈ T to have a term semantic σ_{ł (v)}, namely this defines a term semantic function that by (64) is σ · ł : T → T^{T}.

We can also denote some increment matrices, the constant matrices of 1.6, by S-terms through the generator of constants in (48). This allows an S-term v ∈ T to be uniformly incremented by another S-term t ∈ T, namely we define the growth function γ: T → T^{T} by the growth of v by t, γ_{v}(t) = η̂_{K(t)}(v), for all t, v ∈ T.

With respect to term incrementing as in 1.6, this uniform growth looses something, due to the proper injectivity of the generator of constants (“proper” in case of more than one atom). On the other hand, with respect to the semantic function, term semantic also does, because by (67) the unlabel function collapses all the atoms in U onto ∅. As 2.3 (B) will show, the two different losses get the same function.

Since all semantics in Σ ⊆ P(T × T) are (partial) functions, we can consider the functional composition of any two of them. By next theorem 2.2 (B) it is again a semantic. This composition and i_{T} as in (61) form a monoid that we call the complete semantic monoid. In fact, 4.5 and 4.6 will introduce a “smaller” monoid that is more relevant to effective semantics. Recall that by 0.4 the composition notation is reversed.

2.1 Example. Consider the search terms t′ = ⟨(l, l, ∅), ⟨r, ∅⟩⟩ and t′′ = ⟨(l, l, ∅), ⟨(l, r, ∅), (r, r, ∅)⟩⟩ of fig. 1 and 2. Clearly, they work the same by (62), (63) and (30), but only the latter requires that the right of its argument be a dyad as the diamond in fig. 3 depicts. Hence, their semantics are the functions that build the same S-term ⟨t′, t′′⟩, once they are given arguments of the same form ⟨⟨t′, t⟩, t′′⟩ for some t, t′ ∈ T, yet respectively with t′′ ∈ T and t′′ ∈ D.

In fig. 5 σ_{t}′ sends both boxed S-terms (among others) into the two circled ones (bold arrows), whereas σ_{t}′′ sends the rightmost only. The above dyad requirement determines two properly inclusive induced domains, which correspond to the concave areas at the left and top of the dotted lines.

[figure: u; v; u; u; u; u; v; v; u; u; v; u; u; v; u; v; v; u; u; u; v; v; v; v; u; v; v; u; u; u; v; u; u; v; v; u; v; u; u; u; u; v; u; u; u; v; v; v; u; u; v; u; v; u; *; v; u; u; v; u; *; u; v; v; v; u; u; u; u; v; u; v; u; v; *; v; v; v; v; u; u; u; v; v; u; u; v; v; v; u; v; u; v; v; *; v; v; u; v; Fig. 5; Δt′; Δt′′; σ_{t}′ and σ_{t}′′; σ_{t}′]

The equality of these two semantics on the common part of their different domains hints how section 3 will define the notion of two-ary integers semantically. This will overcome the failures of conventional algebraic extensions we mentioned in 0.1.

Clearly, both induced domains are infinite. We starred four trees outside them. Their left to right sequence hints that also the complement of an induced domain can be infinite, contrary to the co-finiteness of induced domains of unary integers. Still, 4.4 (C) will extend the characterization of the latter domains (co-finite segments of natural numbers) to the twoary integers, while this section will introduce certain “cartesian sets” that extend this characterizing feature to the two-ary case.

2.2 Theorems. (A) Semantics preserve term increments: for every t ∈ T and M: U → T σ_{t} · η̂_{M} = η̂_{M} · σ_{t}, namely for all t ∈ Δ_{t}

σ_{t}(M ˆ+ t) = M ˆ+ σ_{t}(t)  (70)

or also σ_{t} · (M ⋄ L) = M ⋄ (σ_{t} · L), for every L: U → Δ_{t}. (Notice that this implies η̂_{M}(t) ∈ Δ_{t} for all t ∈ Δ_{t}.) (B) The semantic function is a homomorphism from the catenation monoid onto the complete semantic one, namely together with (61) we have σ_{u⊕t} = σ_{t} · σ_{u} , for all t, u ∈ T.

Proofs. (A) When t = ∅, by (61) we get η̂_{M} · σ_{t} = η̂_{M} · i_{T} = i_{T} · η̂_{M} = σ_{t} · η̂_{M}, since in 1.6 η̂_{M}: T → T.

When t = ⟨t′, t′′⟩ and both σ_{t}′(η̂_{M}(t)) = η̂_{M}(σ_{t}′(t)) for all t ∈ Δ_{t}′ and σ_{t}′′(η̂_{M}(t)) = η̂_{M}(σ_{t}′′(t)) for all t ∈ Δ_{t}′′, by (62), 1.7 (B), (52) and (62) we get η̂_{M}(σ_{t}(t)) = η̂_{M}(σ_{t}′(t), σ_{t}′′(t)) = ⟨η̂_{M}(σ_{t}′(t)), η̂_{M}(σ_{t}′′(t))⟩ = ⟨σ_{t}′(η̂_{M}(t)), σ_{t}′′(η̂_{M}(t))⟩ = σ_{t}(η̂_{M}(t)) for all t ∈ Δ_{t}′ ∩ Δ_{t}′′ = Δ_{t}.

Now, assume t = ⟨l, t′⟩ and σ_{t}′(η̂_{M}(t′)) = η̂_{M}(σ_{t}′(t′)) for all t′ ∈ Δ_{t}′. When t ∈ Δ_{t}, by (63) and (65) σ_{t}′(t) ∈ D. Hence, by (42) and (41) η̂_{M}(σ_{t}′(t)) too is a dyad and we have the left of it. By our induction assumption, (65) and (63)

l(η̂_{M}(σ_{t}′(t))) = l(σ_{t}′(η̂_{M}(t))) = σ_{t}(η̂_{M}(t)) .  (71)

Besides, for all ⟨s′, s′′⟩ ∈ D, by 1.7 (B) η̂_{M}(s′, s′′) = ⟨η̂_{M}(s′), η̂_{M}(s′′)⟩ and by (54) l(η̂_{M}(s′, s′′)) = l(η̂_{M}(s′), η̂_{M}(s′′)) = η̂_{M}(l(s′, s′′)). Then, for ⟨s′, s′′⟩ = σ_{t}′(t) ∈ D by (71) and (63) σ_{t}(η̂_{M}(t)) = η̂_{M}(l(σ_{t}′(t))) = η̂_{M}(σ_{t}(t)).

Finally, the step for t = ⟨r, t′⟩ comes from the preceding step by replacing l as usual.

(B) Use bold induction on t. When t = ∅, by (36) σ_{u⊕t} = σ_{u} and σ_{t} = i_{T} by (61). Hence, σ_{u⊕t} = i_{T} · σ_{u} = σ_{t} · σ_{u}.

When t = ⟨t′, t′′⟩ and both σ_{u⊕t′} = σ_{t}′ · σ_{u} and σ_{u⊕t′′} = σ_{t}′′ · σ_{u}, by (37) and (62) σ_{u⊕t}(t) = σ_{⟨u⊕t′,u⊕t′′⟩}(t) = ⟨σ_{u⊕t′}(t), σ_{u⊕t′′}(t)⟩ = ⟨σ_{t}′(σ_{u}(t)), σ_{t}′′(σ_{u}(t))⟩ = σ_{⟨t′,t′′⟩}(σ_{u}(t)), for all t ∈ Δ_{u⊕t} = Δ_{u⊕t′} ∩ Δ_{u⊕t′′}. Also, by the induction premises and (62) Δ_{u⊕t′} ∩ Δ_{u⊕t′′} = {t | σ_{u}(t) ∈ Δ_{t}′} ∩ {t | σ_{u}(t) ∈ Δ_{t}′′} = {t | σ_{u}(t) ∈ Δ_{t}′ ∩ Δ_{t}′′} = {t | σ_{u}(t) ∈ Δ_{⟨t′,t′′⟩}} = {t | σ_{u}(t) ∈ Δ_{t}} = Dom (σ_{t} · σ_{u}). Hence, t ∈ Δ_{u⊕t} iff t ∈ Dom (σ_{t} · σ_{u}) and by (62) σ_{u⊕t}(t) = σ_{⟨t′,t′′⟩}(σ_{u}(t)) = σ_{t}(σ_{u}(t)) = (σ_{t} · σ_{u})(t), for all such t’s, namely σ_{u⊕t} = σ_{t} · σ_{u}.

When t = ⟨l, t′⟩ and σ_{u⊕t′} = σ_{t}′ ·σ_{u}, by (38) and (63) σ_{u⊕t} = σ_{u⊕⟨l,t′⟩} = σ_{⟨l,u⊕t′⟩} = l · σ_{u⊕t′} = l · (σ_{t}′ · σ_{u}) = (l · σ_{t}′) · σ_{u} = σ_{⟨l,t′⟩} · σ_{u} = σ_{t} · σ_{u}, since the composition of partial functions in P(T × T) is associative. When t = ⟨r, t′⟩, merely replace l with r. Q.E.D. 2.3 Lemata. (A) The semantic of any upward path is one to one, for all u ∈ N_{2}(1)

σ_{u}: T ↦T .  (72)

(B) The growth function is the term semantic function, γ = σ · ł . (C) For all full terms z ∈ ⌊m⌋ and w ∈ ⌊l⌋,

γ_{z}(w) ∈ ⌊l + m⌋ .  (73)

(D) If t ∈ Δ_{t}, then C_{1} ˆ+ t ∈ Δ_{⟨l,t⟩}, Δ_{⟨r,t⟩}. (E) Induced domains are “bottom-cofinite”, namely for each t ∈ T there is a full matrix C_{n}: U → T, for some natural number n, such that its increment of every t ∈ T, v = C_{n} ˆ+ t, reaches the domain of σ_{t}, v ∈ Δ_{t}. (F) Catenating any search term t ∈ T with a single letter word restricts the induced domain D = T × T of the word to

Δ_{⟨l,∅⟩⊕t} = Δ_{t} × T or  (74)
Δ_{⟨r,∅⟩⊕t} = T × Δ_{t} .  (75)

Proofs. (A) Use upward induction on u. When u = ∅, by (61) σ_{u} = i_{T} is one to one. When u = ⟨u′, u′′⟩ and σ_{u}′ and σ_{u}′′ are one to one, for all t′, t′′ ∈ T, σ_{u}(t′) = σ_{u}(t′′) implies by (62) that ⟨σ_{u}′(t′), σ_{u}′′(t′)⟩ = ⟨σ_{u}′(t′′), σu′′(t′′)⟩. Hence, by (2) and the induction premises t′ = t′′.

(B) We prove η̂_{K(t)}(v) = σ_{ł (v)}(t) for all t, v ∈ T by T -induction on v. By (42) this induction has to prove K_{t} ˆ+ v = σ_{ł (v)}(t). The basis step for all v = u ∈ U ⊂ T follows from (40), (48), (61) and (67), K_{t} ˆ+ u = K_{t}(u) = t = σ_{∅}(t) = σ_{ł (u)}(t).

When v = ⟨v′, v′′⟩ and both K_{t} ˆ+ v′ = σ_{ł (v′)}(t) and K_{t} ˆ+ v′′ = σ_{ł (v′′)}(t), by (41), (62) and (68) K_{t} ˆ+ ⟨v′, v′′⟩ = ⟨K_{t} ˆ+ v′, K_{t} ˆ+ v′′⟩ = ⟨σ_{ł (v′)}(t), σ_{ł (v′′)}(t)⟩ = σ_{⟨ł (v′),ł (v′′)⟩}(t) = σ_{ł (v)}(t). Hence, we proved the induction step too.

(C) We prove (73) by arithmetic induction on m. When m = 0, z ∈ U and γ_{z}(w) = K_{w} ˆ+ z = K_{w}(z) = w ∈ ⌊l⌋ = ⌊l + m⌋ by (42),(40) and (48). Assume z = ⟨z′, z′′⟩ ∈ ⌊m + 1⌋ with z′, z′′ ∈ ⌊m⌋, according to (10), and γ_{z′}(w), γ_{z′′}(w) ∈ ⌊l + m⌋. Then, by (42),(41) and sum associativity, γ_{z}(w) = K_{w} ˆ+ ⟨z′, z′′⟩ = ⟨K_{w} ˆ+ z′, K_{w} ˆ+ z′′⟩ = ⟨γ_{z′}(w), γ_{z′′}(w)⟩ ∈ ⌊(l + m) + 1⌋ = ⌊l + (m + 1)⌋.

(D) When t ∈ Δ_{t}, by 2.2 (A) C_{1} ˆ+ t ∈ Δ_{t} and σ_{t}(C_{1} ˆ+ t) = C_{1} ˆ+ σ_{t}(t) ∈ D by (70) and 1.8 (A). Hence, by (63) and (13) C_{1} ˆ+ t ∈ Δ_{⟨l,t⟩}, Δ_{⟨r,t⟩}.

(E) Use bold induction on t. When t = ∅, it comes from Δ_{t} = T as in (61). In fact, when we take C_{0} = i_{U}, by (42) and (58) for all such t’s v = i_{U} ˆ+ t = t ∈ Δ_{t}.

When t = ⟨t′, t′′⟩ and there are C_{n′} and C_{n′′} such that v′ = C_{n′} ˆ+ t ∈ Δ_{t}′ and v′′ = C_{n′′} ˆ+ t ∈ Δ_{t}′′ for all t ∈ T, we take n = max(n′, n′′) and get v ∈ Δ_{t} from (62) because both v ∈ Δ_{t}′ and v ∈ Δ_{t}′′. In fact, assume n = n′ and let m = n − n′′, then v = v′ ∈ Δ_{t}′ and v = (C_{m} ⋄ C_{n′′}) ˆ+ t = C_{m} ˆ+ v′′ ∈ Δ_{t}′′ by 1.8 (B), (57) and 2.2 (A). The same for the assumption n = n′′.

When t = ⟨l, t′⟩ and there is C_{n′} such that v′ = C_{n′} ˆ+ t ∈ Δ_{t}′ for all t ∈ T, take n = n′ + 1. Then, v = C_{n} ˆ+ t = (C_{1} ⋄ C_{n′}) ˆ+ t = C_{1} ˆ+ v′ ∈ Δ_{t} by 1.8 (B), (57) and (D). Finally,we prove the step t = ⟨r, t′⟩ by replacing l with r as usual.

(F) For (74) notice that by 2.2 (B), (63) and (61) σ_{⟨l,∅⟩⊕t} = σ_{t} · σ_{⟨l,∅⟩} = σ_{t} · l. Hence, its domain is the set {t | t ∈ T × T and l(t) ∈ Δ_{t}} = {t | t ∈ T × T and t ∈ Δ_{t} × T } = T × T ∩ (Δ_{t} × T) = Δ_{t} × T by (13), the distributivity in I.3.13 (f) of [12] and because Δ_{t} ⊆ T. For (75) merely replace l with r and commute these cartesian products. Q.E.D.

2.4 Corollary. No induced domain can be empty, Δ_{t} ≠ ∅ for all t ∈ T. Furthermore, every Δ_{t} is infinite.

Proof. At least the v’s of 2.3 (E) are in Δ_{t}. They are infinite because T, the domain of any (full) increment, is and because of 1.8 (C). Q.E.D.

2.5 Definitions. For every two-ary natural number t ∈ N_{2}(1) we define the t–structured cartesian set X(t) by upward induction on t as

X(∅) = T and  (76)
X(t′, t′′) = X(t′) × X(t′′) .  (77)

By (5) such an induction also shows that every t–structured cartesian set is made of S-terms,

X(t) ⊆ T = N_{2}(U) .  (78)

If a set of S-terms is t–structured for some such a t, then we say that it is a cartesian set and we denote their set by T = {X(t) | t ∈ N_{2}(1)} ⊂ PT. Notice that U ∉ T , since the only cartesian set containing it is T ≠ U. Hence, we got the cartesian structure function X: N_{2}(1)→^{≻}T .

We define the branch (left) opposite ⇁w of a word w recursively by the backward induction of 1.6 as

⇁∅ = ∅ ,
⇁(⟨l, ∅⟩ ⊕ v) = ⟨⇁v, ∅⟩ and ⇁(⟨r, ∅⟩ ⊕ v) = ⟨∅, ⇁v⟩ .

For instance, this backward induction gets ⇁(⟨r, ⟨l, ⟨l, ∅⟩⟩⟩) = ⟨⟨⟨∅, ∅⟩, ∅⟩, ∅⟩. By backward induction also we clearly get ⇁: W → N_{2}(1).

For each z ∈ N_{2}(1) we say that t ∈ N_{2}(1) is younger or equal to z and we write t ≤ z, when we can relate them by the preorder such that

∅ ≤ ⟨∅, ∅⟩  and, for all t′, t′′, z′, z′′ ∈ N_{2}(1),  (79)
t′ ≤ z′, t′′ ≤ z′′  imply ⟨t′, t′′⟩ ≤ ⟨z′, z′′⟩ .  (80)

We could easily make these conditions (together with reflexivity and transitivity) into the definition of the Galois connection for ≤ by upward induction on t. As 2.7 (C) will show ≤ to be a partial order, for any set V ⊆ N_{2}(1) with a g.l.b v = ⋀ V, we say that v is its youngest term, when v ∈ V.

These age related names refer to the sprouting in botanical trees, which contrary to mathematical ones grow bottom up. In fact, we want to distinguish ≤ from the preorder ⪯ such that t′, t′′ ⪯ ⟨t′, t′′⟩, even though the latter will not occur here.

2.6 Lemata. (A) If Y, Z ∈ T , then Y ∩ Z ∈ T . (B) No cartesian set is finite. (C) Cartesian sets identify their structures, namely the cartesian structure function is a bijection X: N_{2}(1) ↦^{≻}T .

(D) X · ł : T →^{≻}T is a homomorphism from the dyad operation d: T × T → T onto the cartesian product of cartesian sets ×: T × T → T , such that X(ł (u)) = T for u ∈ U and t ∈ X(ł (t)) for all t ∈ T. (E) ∅ is the youngest term of N_{2}(1).

Proofs. (A) Given Y, let Z = X(z). Then we can prove our statement by upward induction on z. When z = ∅, Z = T by (76) and, since Y ⊆ T, Y ∩ Z = Y ∈ T . If z = ⟨z′, z′′⟩ with Y ∩ X(z′), Y ∩ X(z′′) ∈ T , then there are t′, t′′ ∈ N_{2}(1) such that Y ∩ X(z′) = X(t′) and Y ∩ X(z′′) = X(t′′). Hence, by (77) and the usual distributivity in I.3.13 (f) of [12] we get Y ∩ Z = Y ∩ (X(z′) × X(z′′)) = (Y ∩ X(z′)) × (Y ∩ X(z′′)) = X(t′) × X(t′′) = X(t′, t′′) ∈ T .

(B) Trivial upward induction.

(C) We prove that X(z) = X(t) implies z = t by upward induction on t. When t = ∅, by (4) and (76) U ⊆ T = X(t) = X(z), which by (77), (8) and (34) implies that z cannot be a dyad, z = ∅ = t.

Now, consider t = ⟨t′, t′′⟩, where, for all z ∈ N_{2}(1), both X(z) = X(t′) implies t′ = z and X(z) = X(t′′) implies t′′ = z. By (77) and (8) X(t) = X(z) cannot contain U. Hence, z is a dyad ⟨z′, z′′⟩.

Then, (77) rewrites the assumption X(z) = X(t) as an equality of cartesian products, X(z′) × X(z′′) = X(t′) × X(t′′). This implies two equalities on their factors, which by (B) are not empty: X(z′) = X(t′) and X(z′′) = X(t′′). Therefore, by the induction premises t = z, because of (2).

(D) X(ł (u)) = T immediately follows from (67) and (76) and X(ł (d(t′, t′′))) = X(ł (t′)) × X(ł (t′′)) from 1.1, (68) and (77), for all t′, t′′ ∈ T. Finally, to get t ∈ X(ł (t)), we use T -induction on t and the recalled definitions.

(E) We prove ∅ ≤ z by upward induction on z. When z = ∅, we use reflexivity. When z = ⟨z′, z′′⟩ with ∅ ≤ z′ and ∅ ≤ z′′, by (80) we get ⟨∅, ∅⟩ ≤ z and by (79) and transitivity ∅ ≤ z. Q.E.D.

2.7 Theorems. (A) Containment between cartesian sets is a semilattice with zero. (This is not the main motivation of our choice of ⊇ and ∩ as the order and join respectively, instead of the dual choice. The main one will appear in 4.5.) (B) The branch opposite of any word w ∈ W defines the structure of its induced domain by Δ_{w} = X(⇁w). Hence, the induced domains of words are cartesian sets. (C) The cartesian structure function X: N_{2}(1) ↦^{≻}T , namely the function X· ł : T ↦^{≻}T for U = 1, is an isomorphism from the age relation ≤ onto the containment of (A),

t ≤ z iff X(t) ⊇ X(z) for all t, z ∈ N_{2}(1) ,  (81)

where for U = 1 each argument is the youngest term of its cartesian set: for all t ∈ N_{2}(1), t ∈ X(t) and t ≤ z for all z ∈ X(t), hence X defines a closure system.

Proofs. (A) The join closure is in 2.6 (A). The zero is in (76) because of (78).

(B) Use backward induction on w. By 2.5 and 1.6 this is to prove that

Δ_{∅} = T ,
Δ_{⟨l,∅⟩⊕w} = Δw × T and  (82)
Δ_{⟨r,∅⟩⊕w} = T × Δw ,  (83)

The base of this recursion is in (64). For the induction step notice that (82) and (83) are cases of (74) and (75) respectively.

(C) After 2.6 (C), to get the isomorphism, we only have to prove (81). (Only if) Since ⊇ on T is a preorder as ≤ is, we only prove the cases corresponding to (79) and (80) by upward induction on t: the basis step for (79) comes from (5) with U = 1 through (76) and (77), while case (80) comes from the induction premises through (77), because for all sets X′, X′′, Y′ and Y′′, if X′ ⊇ Y′ and X′′ ⊇ Y′′ then X′ × X′′ ⊇ Y′ × Y′′.

(If) Upward induction on z. When z = ∅, by (76) X(z) = T and by (78) X(t) = X(z), which by 2.6 (C) implies t = z in agreement with age reflexivity. Then, assume that z = ⟨z′, z′′⟩, where X(t′) ⊇ X(z′) implies t′ ≤ z′, while X(t′′) ⊇ X(z′′) implies t′′ ≤ z′′. Either t = ∅, which by 2.6 (E) implies t ≤ z, or t = ⟨t′, t′′⟩ for some t′, t′′ ∈ N_{2}(1). In the latter case we easily get both premises of the induction premises from X(t) ⊇ X(z). Hence, by (80) we get t ≤ z.

Finally, we get t ∈ X(t) from 2.6 (D) with U = 1 and t ≤ z for z ∈ X(t) by upward induction on t. In fact, the basis step comes from (76) and 2.6 (E). Then, assume t = ⟨t′, t′′⟩ with t′ ≤ z′ and t′′ ≤ z′′ for all z′ ∈ X(t′) and z′′ ∈ X(t′′). Since z ∈ X(t′, t′′), by (77) z is a dyad ⟨z′, z′′⟩ such that z′ ∈ X(t′) and z′′ ∈ X(t′′). Hence, the induction premises by (80) imply t ≤ z. Q.E.D.

3 Two-ary integers.

3.0 Definition. Consider two search terms t, u ∈ T. When

σ_{t}(t) = σ_{u}(t) for all t ∈ Δ_{t} ∩ Δ_{u} ,  (84)

namely when the semantics of t and u agree whenever both of them are defined, we say that the two search terms are locally equal and write t ≍ u.

3.1 Recursivity. From 2.1 we can fairly guess that the domain of a semantic is recursive and that semantics are (recursive restrictions of) recursive functions. (We omit the technical details.) Yet, the domain intersection in (84) is infinite by 2.4 and (62). Hence, as far as the computability of local equality is concerned, now we can only guess that local inequality is enumerable.

This rises the problem whether local equality is recursive or not. Its affirmative answer will come from the characterization of local equality in 4.3. This characterization will use a recursive procedure defined in 4.0.

3.2 Lemata. (A) τ-operations preserve ≍,

t ≍ u implies ⟨l, t⟩ ≍ ⟨l, u⟩ , ⟨r, t⟩ ≍ ⟨r, u⟩ and (85)
t′ ≍ u′, t′′ ≍ u′′ imply ⟨t′, t′′⟩ ≍ ⟨u′, u′′⟩ .  (86)

for all t, u, t′, u′, t′′, u′′ ∈ T. (B) Relation ≍ is an equivalence on T. (C) Local equality on words becomes equality, for all v, w ∈ W, v ≍ w implies v = w.

Proofs. (A) Consider (85) , then by (65) the domains of σ_{⟨l,t⟩} and σ_{⟨l,u⟩} respectively are subsets of Δ_{t} and Δ_{u}. Hence their intersection is a subset of Δ_{t} ∩ Δ_{u}, where l · σ_{t} and l · σ_{u} coincide by (84). By (63) σ_{⟨l,t⟩} and σ_{⟨l,u⟩} too coincide, as required. The same holds when we replaces l by r.

To prove (86) let us introduce some more notation. Let Δ_{t}′ = x, Δ_{t}′′ = y, Δ_{u}′ = u and Δ_{u}′′ = v, We have to show that σ_{⟨t′,t′′⟩} and σ_{⟨u′,u′′⟩} agree on Δ_{⟨t′,t′′⟩} ∩ Δ_{⟨u′,u′′⟩} = (x ∩ y) ∩ (u ∩ v) = (x ∩ u) ∩ (y ∩ v), once we know that σ_{t}′ agrees with σ_{u}′ on x ∩ u and that σ_{t}′′ agrees with σ_{u}′′ on y ∩ v. This comes from (x ∩ u) ∩ (y ∩ v) ⊆ x ∩ u , y ∩ v, because of (62) and (2).

(B) Symmetry and the domain are trivial. Hence, we only show that, for all t, v, w ∈ T, t ≍ v and v ≍ w imply t ≍ w. Take any t ∈ Δ_{t} ∩ Δw. By lemma 2.3 (E) there is M = C_{n}: U → T such that v = η̂_{M}(t) ∈ Δ_{⟨t,⟨v,w⟩⟩}. Hence, by (62)v ∈ Δ_{t} ∩ Δv ∩ Δw. Therefore, by (84) the premises imply that σ_{t}(v) = σv(v) = σw(v).

From σ_{t}(v) = σw(v) 2.2 (A) gets η̂_{M}(σ_{t}(t)) = η̂_{M}(σw(t)). When n = 0, this already is σ_{t}(t) = σw(t) by (58), while for n > 0 we get it from lemma 1.8 (C). Hence, t ≍ w.

(C) At first, notice that the only word locally equal to the empty one is the empty word: for all w ∈ W, w ≍ ∅ implies w = ∅. In fact, by (61) this premise implies σw(t) = t for all t ∈ Δw, where Δw ≠ ∅ by 2.4. By the definition of pair in 0.4 it is trivial to show that this violates the regularity axiom of Set Theory in I.1.18 of [12], as in theorem I.1.19 ibid., unless the sequence of compositions of l and r in σw is empty. Hence, w = ∅.

Now, it is enough to prove our statements for nonempty words v, w ∈ W and we do it by contradiction. Assume that v is such that v ≍ w and v ≠ w. Then, there are v′, w′ ∈ W and words of length one v′′, w′′ = ⟨l, ∅⟩, ⟨r, ∅⟩ such that

v = v′′ ⊕ v′ and w = w′′ ⊕ w′ .  (87)

Let us consider the four possible choices of v′′ and w′′.

(Case v′′ = ⟨l, ∅⟩ ≠ w′′ = ⟨r, ∅⟩) By 2.3 (E) there is a natural number n such that, for all t ∈ T, C_{n} ˆ+ t ∈ Δ_{⟨v,w⟩} = Δv ∩ Δw. Hence, σv(C_{n} ˆ+ t) = σw(C_{n} ˆ+ t) and by 2.2 (B) (87) gets σv′(σv′′(C_{n} ˆ+ t)) = σw′(σw′′(C_{n} ˆ+ t)). When t ∈ D, by 2.2 (A) this implies

σv′(C_{n} ˆ+ σv′′(t)) = σw′(C_{n} ˆ+ σw′′(t)) .  (88)

Now, take t = ⟨⟨u, u⟩, u⟩ for some u ∈ U. Then, this choice of v′′ and w′′ gets C_{n} ˆ+ σv′′(t) = C_{n} ˆ+ ⟨u, u⟩ = ⟨C_{n} ˆ+ u, C_{n} ˆ+ u⟩ = ⟨C_{n}(u), C_{n}(u)⟩ = C_{n+1}(u) = C_{1} ˆ+ C_{n}(u) by (41), (40), (47), 1.8 (B), (57) and (45) as well as C_{n} ˆ+ σw′′(t) = C_{n} ˆ+ u = C_{n}(u) by (40). Flip our S-term, t = ⟨u, ⟨u, u⟩⟩, and get C_{n} ˆ+ σw′′(t) = C_{1} ˆ+ C_{n}(u) and C_{n} ˆ+ σv′′(t) = C_{n}(u) in the same way.

Hence, from (88) the former t by 2.3 (E) and (70) gets

σv′(C_{1} ˆ+ C_{n}(u)) = C_{1} ˆ+ σv′(C_{n}(u)) = σw′(C_{n}(u)) ,  (89)

while the latter gets

σv′(C_{n}(u)) = σw′(C_{1} ˆ+ C_{n}(u)) = C_{1} ˆ+ σw′(C_{n}(u)) .  (90)

This implies σv′(C_{n}(u)) = C_{1} ˆ+ (C_{1} ˆ+ σv′(C_{n}(u))) = (C_{1}⋄ C_{1}) ˆ+ σv′(C_{n}(u)) = C_{2} ˆ+ σv′(C_{n}(u)) by (57) and 1.8 (B). Thus, σv′(C_{n}(u)) is a fixed point of a full increment, contrary to 1.8 (D).

(Case v′′ = ⟨r, ∅⟩ ≠ w′′ = ⟨l, ∅⟩) In all the preceding argument we can exchange l with r and v with w. Hence, the fixed point violation takes place again.

(Case v′′ = ⟨l, ∅⟩ = w′′) Here, flipping the t’s does not work. We resort to the usual minimal length contradiction argument. Assume that v is of a minimal length. Then, by 2.2 (B), (63) and (87) our premise v ≍ w becomes σv′(l(t)) = σw′(l(t)) for all t ∈ Δ_{v} ∩ Δ_{w}. By (74) Δ_{v} ∩ Δ_{w} = (Δv′ × T) ∩ (Δw′ × T) = (Δv′ ∩ Δw′) × T because of the distributivity of the set operations involved, e.g. see I.3.13 (f) of [12].

Moreover, for any T′ ⊆ T, t ∈ T′ × T iff t′ = l(t) ∈ T′ as it follows from 1.1. Hence, σv′(t′) = σw′(t′) for all t′ ∈ Δv′ ∩ Δw′, namely v′ ≍ w′, where v′ is shorter than v of one letter contrary to our minimality assumption.

(Case v′′ = ⟨r, ∅⟩ = w′′) In the preceding argument replace l with r and (74) with (75). Q.E.D.

3.3 Definition. The relation ≍ we have defined in 3.0 is an equivalence relation on T by 3.2 (B). Hence, by dividing T by ≍ we get a set I_{2} that we call of the two-ary integers. In fact, I_{2} generalizes the usual integers, in the way introduced by 0.0 and 0.2. In another way, lemma 3.2 (C) hints it might well generalize words. (Besides, 4.2 (E) will extend the uniqueness property in this lemma to the upward paths in N_{2}(1).) We will confirm this hint in 4.2 and 5.1 (A).

By lemma 3.2 (A) and (B) ≍ also is a congruence of the τ–operations. Then, by an algebra division one might get an abstract algebra on I_{2}. We do not because we want to peer into it.

For instance, the abstract algebra of usual integers, the equivalence classes of pairs ⟨m, n⟩ of natural numbers we recalled in 0.1, is of little use. The actual algebra is the one of the reduced representatives of such abstract elements, the ones of the forms ⟨m, 0⟩ or ⟨0, n⟩. It gets an effective representation of usual integers: “natural numbers with sign”.

Here also, we will modify our two-ary natural numbers (S-terms) to get an effective concrete representation of two-ary integers. In fact, Section 4 will define a reduction procedure that gets certain S-terms. As in the unary case, this procedure has a functional nature: no need of any Church-Rosser property.

3.4 Lemma. For all t, t′, t′′ ∈ T,

⟨⟨l, t⟩, ⟨r, t⟩⟩ ≍ t  and  (91)
⟨l, ⟨t′, t′′⟩⟩ ≍ t′ and ⟨r, ⟨t′, t′′⟩⟩ ≍ t′′ ,  (92)

(While the inversion equations of 1.3 (B) do not always hold for two-ary natural numbers because of the quantification in (30), this states they could become identities for all two-ary integers, if we had introduced their algebra.)

Proof. When we replace σ_{t}(t) for t in (30), (14), (62) and (63) prove that σ_{⟨⟨l,t⟩,⟨r,t⟩⟩}(t) = σ_{t}(t) holds for all t such that σ_{t}(t) ∈ D. Let T′ be their set and T′′ = Δ_{t} be the domain of σ_{t}. Then T′ ⊆ T′′, because σ_{t}(t) ∉ D for t ∉ Δ_{t} (see I.1.43 (c) in [12]). Since T′ also is the domain of both σ_{⟨l,t⟩} and σ_{⟨r,t⟩}, Δ_{⟨l,t⟩} = Δ_{⟨r,t⟩}, by (62) it is the domain of σ_{⟨⟨l,t⟩,⟨r,t⟩⟩}, hence, the intersection required in (84) for (91).

For (92) it is enough to prove the former equivalence, as the latter comes from replacing r for l. Now, we replace σ_{t}′(t) for t′ and σ_{t}′′(t) for t′′ in (31). Then, we use (14), (63) and (62) and get the intersection required in (84), immediately from (62). Q.E.D.

4 Jumps and reduction.

4.0 Definitions. At first, notice that (23) allows us to define two functions p_{1}, p_{2} ⊆ T × T such that

p_{1}(t′, t′′), p_{1}(l, t′), p_{1}(r, t′) = t′ and p_{2}(t′, t′′) = t′′ ,  (93)

for all t′, t′′ ∈ T , which pick the first and possible second search term in a composed search term. Trivially, (3) prevents any fixed point:

p_{1}(t), p_{2}(t) ≠ t , for all t ∈ T .  (94)

By such a notation we say that t′, t′′ ∈ T are confluent, when t′ = ⟨l, p_{1}(t′)⟩ and t′′ = ⟨r, p_{1}(t′)⟩, see the bottom of the diamond in fig. 3, and that t ∈ T is a d-term, when t = ⟨p_{1}(t), p_{2}(t)⟩. (Confluence is antisymmetric.)

Then, by bold induction we can define a reduction (function) ρ: T → T as

ρ(∅) = ∅ ;  (95)
ρ(t′, t′′) = \{ \begin{matrix}p_{1}(ρ(t′)) & when ρ(t′) and ρ(t′′) are confluent, \\ ⟨ρ(t′), ρ(t′′)⟩ & otherwise \end{matrix} ; (96)
ρ(l, t) = \{ \begin{matrix}p_{1}(ρ(t)) & when ρ(t) is a d-term, \\ ⟨l, ρ(t)⟩ & otherwise \end{matrix} ;  (97)
ρ(r, t) = \{ \begin{matrix}p_{2}(ρ(t)) & when ρ(t) is a d-term, \\ ⟨r, ρ(t)⟩ & otherwise \end{matrix} .  (98)

We also define the set A of the jumps or reduced terms as the minimal set such that

W ⊆ A and,  (99)
if a′, a′′ ∈ A are not confluent, then ⟨a′, a′′⟩ ∈ A .  (100)

Clearly, A satisfies both conditions. We allow two different names for its elements, because of the next two different inclusions in 4.1 (B) and (C). Also, because of the latter inclusion, we will sometimes boldface the letters denoting them. When a jump is a d-term, we call it a composed jump and we denote the set of them by D′. The restriction of the premise in (100) works only when both a′ and a′′ are words (atoms), since no composed jump can begin with l or r: for all a′, a′′ ∈ A

⟨a′, a′′⟩ ∉ A implies a′, a′′ ∈ W .  (101)

Lemma 4.1 (E) is going to state a (full) induction principle for reduced terms that we call reduced induction. Since its basis step requires to check a superset of W and this in most cases involves a word induction or a backward one, it is not “reduced” at all: often it will require two induction steps.

4.1 Lemata. (A) (Binary) search words are unknowns for pairing. (B) Jumps are two-ary natural numbers on (search) words: A ⊆ N_{2}(W). (C) Reduced terms are search terms: A ⊆ T. (D) We can partition jumps into words and composed jumps: A = W ∪ D′ and W ∩ D′ = ∅. (E) For all sets A′, A′ ⊇ A iff W ⊆ A′ and, for all t′, t′′ ∈ A ∩ A′ that are not confluent, ⟨t′, t′′⟩ ∈ A′. (F) The first and second search term of a jump are jumps: p_{1}(a) ∈ A, for ∅ ≠ a ∈ A, and p_{2}(a) ∈ A , for all a ∈ D′. (G) The first and second search term of a composed jump cannot be confluent: ⟨a′, a′′⟩ ∈ A and a′ = ⟨l, a⟩ imply a′′ ≠ ⟨r, a⟩. (H) For every reduced term a ∈ A there is a natural number n such that, for each word w ∈ W of a length not less than n, a ⊕ w ≍ v for some word v ∈ W and, for every such a v, v = a ⊕ w iff a ∈ W. (I) The catenation of any reduced term a ∈ A with any word w ∈ W is reduced, w ⊕ a ∈ A.

Proofs. (A) When in (4) U = W, the elements of T in (7) are finite sets, because both words and the pairs in D = T × T are. The latter pairs neither can be the empty word nor can have an infinite component as any other word does. In fact, such nonempty words are pairs w = ⟨l, v⟩ or w = ⟨r, v⟩, where both l and r are infinite sets.

(B) Since T′ = N_{2}(W) satisfies (4), with U = W, and (5), it will also satisfy (99) and (100). Hence, N_{2}(W) ⊇ A by the minimality of A.

(C) Again , we use the minimality of A, but for (4)-(5) replaced by (17)- (18).

(D) Since D′ ⊆ N_{2}(W) × N_{2}(W), W ∩ D′ = ∅ has been shown in (A). Trivially, W ∪ D′ ⊆ A. To see that A′ = W ∪ D′ ⊇ A, since W ⊆ A, we merely consider a′, a′′ ∈ A′ and show that ⟨a′, a′′⟩ ∈ D′ ⊆ A′, when they are not confluent. This follows from ⟨a′, a′′⟩ being a d–term that must belong to all sets containing W and closed under our restricted pairing.

(E) As for 1.3 (A), the (only if) comes from (99) and (100), while the (if) from A′ ∩ A ⊆ A′ being a superset of A.

(F) and (G) In the opposite cases the minimality of A fails, because one could delete the corresponding jumps.

(H) Use reduced induction on a. For a ∈ W take n = 0. Hence, for each w ∈ W, a ⊕ w ∈ W by 1.8 (E) and, by the reflexivity of ≍, we get a ⊕ w ≍ v with v = a ⊕ w ∈ W.

Let a = ⟨a′, a′′⟩, where a′, a′′ ∈ A (are not confluent and) have natural numbers n′ and n′′ such that, for all words w′ of a length not less than n′ and w′′ of a length not less than n′′, a′ ⊕ w′ ≍ v′ and a′′ ⊕ w′′ ≍ v′′ for some v′, v′′ ∈ W. Then, take n = 1 + max(n′, n′′).

Clearly, for every w ∈ W of length not less than n, there is a one-letter word u = ⟨l, ∅⟩, ⟨r, ∅⟩ such that w = u ⊕ z for some word z ∈ W of a length not less than both n′ and n′′. Hence, by (55) a ⊕ w = (a ⊕ u) ⊕ z, where by (38) and (36) a ⊕ u = ⟨l, a⟩, ⟨r, a⟩. In both cases the induction premises

get a ⊕ w = \{ \begin{matrix}⟨l, ⟨a′, a′′⟩⟩ ⊕ z ≍ a′ ⊕ z ≍ v′ & for some v′ ∈ W \\ ⟨r, ⟨a′, a′′⟩⟩ ⊕ z ≍ a′′ ⊕ z ≍ v′′ & for some v′′ ∈ W \end{matrix} by (92),

namely a ⊕ w ≍ v for some v ∈ W.

(iff) When a ∈ W, by 1.8 (E) a ⊕ w ∈ W and by 3.2 (C) a ⊕ w = v, which conversely gets a ∈ W by an easy word induction on w: trivial for w = ∅ while the induction step comes from (38) and (21).

(I) Reduced induction on a. When a ∈ W, by 1.8 (E) w ⊕ a ∈ W ⊆ A. When a = ⟨a′, a′′⟩, where a′, a′′ ∈ A are not confluent and w ⊕ a′, w ⊕ a′′ ∈ A, even w⊕a′ and w⊕a′′ cannot be confluent. In fact, either both a′, a′′ ∈ W and by (38) w ⊕ a′, w ⊕ a′′ ∈ W respectively end as a′ and a′′ do or some of them is composed and by (37) even its corresponding catenation with w does, contrary to (101). Therefore, by (37) and (100) w ⊕ ⟨a′, a′′⟩ ∈ A. Q.E.D.

4.2 Theorems. Jumps are “canonical” two-ary integers, namely: (A) reduction preserves local equality: for all t ∈ T, t ≍ ρ(t); (B) reduced terms are irreducible, ρ · i_{A} = i_{A}, i.e. ρ(a) = a for all a ∈ A; (C) conversely, if a search term is irreducible, ρ(t) = t, then it is reduced, t ∈ A; (D) all reductions of search terms are reduced terms and conversely: ρ: T →^{≻}A; (E) Among reduced terms local equality is identity: for all a, u ∈ A

a ≍ u implies a = u .  (102)

Proofs. (A) Use bold induction on t. When t = ∅, it comes from (95), since ≍ is reflexive.

When t = ⟨t′, t′′⟩ and both t′ ≍ ρ(t′) and t′′ ≍ ρ(t′′), we set u′ = ρ(t′) and u′′ = ρ(t′′) in (86) and get ⟨t′, t′′⟩ ≍ ⟨ρ(t′), ρ(t′′)⟩. By (96) this immediately implies that ⟨t′, t′′⟩ ≍ ρ(t′, t′′), when ρ(t′) and ρ(t′′)) are not confluent. When they are, ⟨ρ(t′), ρ(t′′)⟩ ≍ p_{1}(ρ(t′)) by (91). Hence, ⟨ρ(t′), ρ(t′′)⟩ ≍ ρ(t′, t′′) by (96) and transitivity.

When t = ⟨l, t′⟩ and t′ ≍ ρ(t′), we set u = ρ(t′) in (85) and gets ⟨l, t′⟩ ≍ ⟨l, ρ(t′)⟩. By (97) this immediately implies that ⟨l, t′⟩ ≍ ρ(l, t′), when ρ(t′) is not a d-term. When it is, ⟨l, ρ(t′)⟩ ≍ p_{1}(ρ(t′)) by (92). Hence, ⟨l, t′⟩ ≍ ρ(l, t′) by (97) and transitivity. Finally, we prove the step t = ⟨r, t′⟩ by replacing l with r (and p_{1} with p_{2}) as usual.

(B) Consider the steps (96), (97) and (98). When ⟨t′, t′′⟩, ⟨l, t⟩, ⟨r, t⟩ ∈ A, so are t′, t′′ and t by 4.1 (F). Moreover, t′ and t′′ cannot be confluent by 4.1 (G), while t ∈ W by 4.1 (D) and the minimalities of A and W. Hence. in all three steps the former case cannot occur and this restriction of ρ is an identity by a trivial reduced induction.

(C) Use bold induction. For t = ∅, t ∈ A, since ∅ ∈ W. When t = ⟨t′, t′′⟩ and both ρ(t′) = t′ implies t′ ∈ A and ρ(t′′) = t′′ implies t′′ ∈ A, we use the premise in (C) and (94) to find that t′ and t′′ cannot be confluent nor reducible. Then the premises in the induction premise and (100) to get t ∈ A. The cases t = ⟨l, t′⟩ and t = ⟨r, t′⟩ easily follow from 4.1 (D).

(D) After (B), we only have to prove ρ: T → A, namely that the reduction of a search term is a reduced term, ρ(t) ∈ A for all t ∈ T, by bold induction on t. When t = ∅, ρ(t) = ∅ ∈ A by (95), (19) for W and (99).

When t = ⟨t′, t′′⟩ and both ρ(t′), ρ(t′′) ∈ A, ρ(t′) and ρ(t′′) cannot be confluent, unless they are in W as in (101). In the former circumstance, ρ(t) ∈ A by (100) and the latter case of (96). In the latter, it does by (99) and the former case of (96), since ρ(t′) ∈ A implies p_{1}(ρ(t′)) ∈ A by 4.1 (F).

When t = ⟨l, t′⟩ and ρ(t′) ∈ A, either ρ(t′) ∈ W or it is a d-term. In the former circumstance, ρ(t) ∈ W ⊂ A by (99), (21) for W and the latter case of (97). In the latter, it does by the former case of (97), again because ρ(t′) ∈ A implies p_{1}(ρ(t′)) ∈ A. A similar proof holds for t = ⟨r, t′⟩.

(E) The proof of (102) will use reduced induction on a. Yet, at now we prove a lesser statement that has a proof useful both in its basis step and induction step. We only prove that (102) holds for all a ∈ A and all u ∈ W and we do it by reduced induction on a.

This basis step is for a ∈ W and 3.2 (C) provides it with the proof of (102). The induction step is a = ⟨a′, a′′⟩ for some a′ and a′′ such that, for all u′, u′′ ∈ W, a′ ≍ u′ implies a′ = u′, while a′′ ≍ u′′ implies a′′ = u′′. Then, by (85) a ≍ u implies ⟨l, a⟩ ≍ ⟨l, u⟩. By (92) this implies a′ ≍ ⟨l, u⟩, where u′ = ⟨l, u⟩ ∈ W by (21) for W. Hence, our former induction premise gets a′ = ⟨l, u⟩, while, after replacing l with r, the latter gets a′′ = ⟨r, u⟩. This contradicts the confluence free assumption of 4.1 (G) and makes the implication, we are proving, trivially true, as there are not such pairs ⟨a′, a′′⟩ in A.

We can now prove (102) with its full quantification. The basis step, for a ∈ W, comes from the preceding proof after flipping a and u, namely by a reduced induction on u nested in the present induction on a. For the induction step, a = ⟨a′, a′′⟩, the induction premises now hold for all u′, u′′ ∈ A. Hence, when u′, u′′ ∈ W, the proof is the one of the preceding induction step, while, when u = ⟨v′, v′′⟩ for some v′, v′′ ∈ A, we still get a′ ≍ ⟨l, u⟩ and a′′ ≍ ⟨r, u⟩. From this, by (92) a′ ≍ v′ and a′′ ≍ v′′. Therefore, if we take u′ = v′ and u′′ = v′′, then the induction premises get a′ = v′ and a′′ = v′′ and by (2) a = ⟨a′, a′′⟩ = ⟨v′, v′′⟩ = u (now, by a non trivial implication). Q.E.D.

4.3 Corollary. Local equality is the equivalence induced by reduction. Hence, every two-ary integer has a single reduced term.

Proof. (A) To show that, for all t, ∈ T, t ≍ u implies ρ(t) = ρ(u), we first use 4.2 (A) and transitivity to get ρ(t) ≍ ρ(u). Then, we use 4.2 (D) and (E). To get the converse implication we merely use 4.2 (A) and transitivity. Q.E.D.

4.4 Theorems. (A) Reduced terms have the maximal domain property: for all t ∈ T, Δ_{t} ⊆ Δ_{ρ(t)}. (B) Conversely, for all t, u ∈ T, σ_{t} ⊆ σ_{ρ(u)} implies that t ≍ u. Yet, σ_{t} ⊆ σ_{u} for all t ∈ T, such that t ≍ u, does not imply that u ∈ A. (C) A set of S-terms is the domain of a reduced term iff it is cartesian.

Proofs. (A) Use bold induction on t. When t = ∅, it comes from (95) and (64).

When t = ⟨t′, t′′⟩ and both Δ_{t}′ ⊆ Δ_{ρ(t′)} and Δ_{t}′′ ⊆ Δ_{ρ(t′′)}, by (62) we get Δ_{⟨t′,t′′⟩} = Δ_{t}′ ∩ Δ_{t}′′ ⊆ Δ_{ρ(t′)} ∩ Δ_{ρ(t′′)} = Δ_{⟨ρ(t′),ρ(t′′)⟩}. By (96) this immediately implies that Δ_{⟨t′,t′′⟩} ⊆ Δ_{ρ(t′,t′′)}, when ρ(t′) and ρ(t′′)) are not confluent. When they are, Δ_{ρ(t′)} = Δ_{ρ(t′′)} by (65). Hence, Δ_{⟨ρ(t′),ρ(t′′)⟩} = Δ_{ρ(t′)} by (62), which implies Δ_{⟨t′,t′′⟩} ⊆ Δ_{ρ(t′,t′′)}, because Δ_{ρ(t′)} ⊆ Δ_{p_{1}(ρ(t′))} = Δ_{ρ(t′,t′′)} by (65) and (96).

When t = ⟨l, t′⟩ and Δ_{t}′ ⊆ Δ_{ρ(t′)}, we get Δ_{⟨l,t′⟩} ⊆ Δ_{⟨l,ρ(t′)⟩} by (65) and (63). By (97) this immediately implies that Δ_{⟨l,t′⟩} ⊆ Δ_{ρ(l,t′)}, when ρ(t′) is not a d-term. When it is, Δ_{ρ(t′)} = Δ_{p_{1}(ρ(t′))} ∩ Δ_{p_{2}(ρ(t′))} ⊆ Δ_{p_{1}(ρ(t′))} by (93) and (62). Hence, Δ_{t}′ ⊆ Δ_{p_{1}(ρ(t′)} = Δ_{ρ(l,t′)} by transitivity and (97). By (65) and transitivity Δ_{t} = Δ_{⟨l,t′⟩} ⊆ Δ_{t}′ ⊆ Δ_{ρ(l,t′)} = Δ_{ρ(t)}. Finally, we prove the step t = ⟨r, t′⟩ by the usual replacements.

(B) σ_{t} ⊆ σ_{ρ(u)} implies t ≍ ρ(u) as in (84). Then, by 4.2 (A) t ≍ u. (Yet) Take u = ⟨l, ⟨⟨l, ∅⟩, ∅⟩⟩ and a = ⟨l, ∅⟩ = ρ(u). Then, u ≍ a by 4.3, Δ_{u} = D = Δ_{a} and a ∈ A, whereas u ∉ A.

(C) (if) To see that every X(t) is a Δ_{a} for some a ∈ A use upward induction on t. For t = ∅, by (76) and (61) X(t) = T = Δ_{∅} and ∅ ∈ W ⊆ A.

When t = ⟨t, u⟩, where X(t) = Δ_{a} and X(u) = Δ_{b} for some a, b ∈ A, we set a′ = ⟨l, ∅⟩ ⊕ a and b′ = ⟨r, ∅⟩ ⊕ b and get a′, b′ ∈ A again by 4.1 (I). By (23) they cannot be confluent unless a = b = ∅ and in such a case by (61) and (62) Δ_{t} = T ∩ T = T = Δ_{∅} again. In all other cases ⟨a′, b′⟩ ∈ A still provides X(t) with the required induced domain: Δ_{⟨a′,b′⟩} = Δ_{a′} ∩ Δ_{b′} = (Δ_{a} × T) ∩ (T × Δ_{b}) = Δ_{a} × Δ_{b} = X(t) × X(u) = X(t, u) by (62), 2.3 (F), the inclusions Δ_{a}, Δ_{b} ⊆ T and (77).

(Only if) Use reduced induction on the reduced term. The basis comes from 2.7 (B). The induction step comes from (62) and 2.6 (A). Q.E.D.

4.5 Cartesian sets. At first glance, two-ary integers look clumsier than unary integers, which can be positive, null or negative. As 5.1 (A) and (B) will detail, also in A we can distinguish three disjoint sets or genders: the singleton set of the zero {∅} = {0}, the null jump, with the same zero of (settheoretical) natural numbers, the set of negative jumps, A^{−} = W ∖ {0}, and the set of positive jumps A^{+} = N_{2}(1) ∖ {0}. Yet, contrary to usual integers, it is not all: e.g. ⟨⟨l, ∅⟩, ∅⟩ does not belong to any of the above genders. Now, we have a fourth gender: the set A^{±} = A ∖ ({0} ∪ A^{−} ∪ A^{+}).

On the contrary, the theorems, we just proved, hint that from a semantic point of view things are not so different. By (64) positive and null jumps have the whole T as the induced domain like positive and null integers, which have the whole set of natural numbers. Now, we can say that the other jumps behave much like negative integers.

In fact, the induced domain of any negative integer is a cofinite segment of natural numbers. Such sets form a semilattice with zero, once we take ⊇ as the order among them. We take it, instead of ⊆, because we can identify each cofinite segment by its (finite) lowest number and such a containment becomes (directly) isomorphic to the natural order ≤ of natural numbers.

In case of jumps, 4.4 (C) and 2.7 (A) provide our induced domains with a semilattice, now of cartesian sets, with zero. By 2.6 (B) a cartesian set is infinite, like the cofinite segments, and 2.6 (C) always provides it again with a finite two-ary natural number as an identifier. By 2.7 (C) the age relation is the natural order among two-ary natural numbers, isomorphic to the semilattice on cartesian sets.

Furthermore, the induced domains of jumps, canonical representatives of two-ary integers, are maximal by 4.4 (A), like the ones of canonical integers in 0.2. For instance, the induced domain of ⟨−1, ∅⟩, corresponding to −1, is the segment [1, ∞], whereas the one of its equivalent ⟨+1, ⟨−1, ⟨−1, ∅⟩⟩⟩ is its subset [2, ∞].

This also shows that within usual integers the effective monoids of semantics is not the functional one: the composition of the semantic of ⟨−1, ⟨−1, ∅⟩⟩ and the one of ⟨+1, ∅⟩ has the smaller domain [2, ∞], whereas the bigger [1, ∞] is the one we use, e.g. when finding the solution of equation 1 + x = 0 “semantically”. This prompt us to introduce a new semantic monoid in the next definition, by discarding the semantics that are not maximal and — accordingly — by rounding the compositions up.

4.6 Definitions. Consider the set S′ ⊆ Σ of the maximal semantics, namely such that σ · ρ: T →^{≻}S′, and by 4.2 (B) define the prime semantic as the function s′: A → S′ we get by restricting the semantic function to jumps, s′ = σ · i_{A}. By 4.4 (A), (B) and 4.3 inclusion of semantics in maximal semantics is a function ϱ: Σ→^{≻}S′: for all f ∈ Σ and g ∈ S′, f ⊆ g iff ϱ(f) = g. This defines the rounded composition ⊙: S′ × S′ → S′ between maximal semantics by

g′′ ⊙ g′ = ϱ(g′′ · g′) for all g′, g′′ ∈ S′ .  (103)

Therefore,

g′′ · g′ ⊆ g′′ ⊙ g′ , for all g′, g′′ ∈ S′ ,  (104)

and g′′ ⊙ g′ is the only maximal semantic satisfying it.

By 4.7 (B) rounded composition is associative and has the unit i_{T} ∈ S′ by (61) and (95). Hence, they form a monoid that we call the prime semantic monoid (for the set of atoms U).

4.7 Corollaries. (A) The prime semantic is a bijection from jumps onto maximal semantics, s′: A ↦^{≻}S′. (B) For all f′, f′′ ∈ Σ, ϱ(f′′ · f′) = ϱ(ϱ(f′′) · f′) = ϱ(f′′ · ϱ(f′)). Hence, rounded composition is associative, (g′′ ⊙ g′) ⊙ g = g′′ ⊙ (g′ ⊙ g) for all g, g′, g′′ ∈ S′.

Proofs. (A) 4.2 (D) and 4.4 (A) prove this ontoness. To check that s′ is one to one, consider any a, u ∈ A. If s′_{a} = s′_{u}, then σ_{a} = σ_{u} and a ≍ u as in 3.0. Hence, by 4.2 (E) a = u.

(B) From 2.2 (B) and the notion of functional (or relational) composition we immediately get Σ ∋ f′′ · f′ ⊆ ϱ(f′′) · f′, f′′ · ϱ(f′) ∈ Σ for all f′, f′′ ∈ Σ. Since the inclusion ϱ is a function, this implies ϱ(f′′ · f′) = ϱ(ϱ(f′′) · f′) = ϱ(f′′ · ϱ(f′)). Hence, (g′′ ⊙ g′) ⊙ g = ϱ(ϱ(g′′ · g′) · g) = ϱ((g′′ · g′) · g) = ϱ(g′′ · (g′ · g)) = ϱ(g′′ · ϱ(g′ · g)) = g′′ ⊙ (g′ ⊙ g). Q.E.D.

5 The prime representation of the jump algebra.

5.0 Definitions. The property in 4.2 (D) allows us to introduce the following operations on jumps. The sum of jump a′′ and jump a′ is the jump

a′ + a′′ = ρ(a′ ⊕ a′′) .  (105)

Hence, we defined a binary operation +: A × A → A that we call jump sum. From it we also get the jump increment function η′: A → A^{A} by

η′_{a′}(a′′) = a′ + a′′ , for all a′, a′′ ∈ A .  (106)

The jump cons too is a binary operation α_{d}: A × A → A that we define by

α_{d}(a′, a′′) = ρ(a′, a′′) , for all a′, a′′ ∈ A ,  (107)

whereas the jump car and jump cdr are unary, α_{l}, α_{r}: A → A, and are respectively defined by

α_{l}(a) = ρ(l, a) and α_{r}(a) = ρ(r, a) , for all a ∈ A .  (108)

Since it might occur that α_{d}(a′, a′′) ≠ ⟨a′, a′′⟩, α_{l}(a) ≠ ⟨l, a⟩ or α_{r}(a) ≠ ⟨r, a⟩, one cannot properly call such operations jump dyad, jump left or jump right respectively. Even the LISP keywords, we are using, lack this propriety. Yet, since they are less usual, this lessens. Anyway, we call the function α, we just defined, the (finite dimensional) jump algebra. 5.6 will motivate why we are discarding the notion of an algebra, ⟨A, α⟩.

Given a set B, we also consider another function β on the domain {l, r, d} indexing three operations β_{l}, β_{r}: B → B and β_{d}: B ×B → B and we say that a function h: A → B is a homomorphism from α into β, when for all a, a′ ∈ A

h(α_{d}(a, a′)) = β_{d}(h(a)), h(a′)) and  (109)
h(α_{l}(a)) = β_{l}(h(a)) and h(α_{r}(a)) = β_{r}(h(a)) .  (110)

H_{αβ} will denote the set of such h’s. When β = α, E_{α} will replace H_{αα} and we call any h an endomorphism of α or a jump endomorphism.

We say that β is binary invertible, when the operations it indexes always satisfy the binary inversion equations of 1.3 (B), due to B. Jónsson and A. Tarski [7], namely when for all b, b′ ∈ B

β_{d}(β_{l}(b), β_{r}(b)) = b and  (111)
β_{l}(β_{d}(b, b′)) = b = β_{r}(β_{d}(b′, b)) .  (112)

Then, for each β, we define r′: H_{αβ} → B by

r′(h) = h(∅) , for all h ∈ H_{αβ} .  (113)

As 5.4 (B) will show, when β = α, r′ is one of the representations of E_{α}. Hence, we call it the prime (analytic) representation of (the endomorphisms of) the jump algebra.

5.1 Lemata. (A) For all v, w ∈ W, α_{l}(w) = ⟨l, w⟩ ∈ W, α_{r}(w) = ⟨r, w⟩ ∈ W and w + v = w ⊕ v ∈ W. Hence, jump sum is an extension of word catenation. (B) Whenever a, a′ ∈ A are not confluent, α_{d}(a, a′) = ⟨a, a′⟩. Hence, α_{d}(u, t) = ⟨u, t⟩ for all u, t ∈ N_{2}(1). (C) For all u, t ∈ N_{2}(1) ⊆ A, t + u = K_{t} ˆ+ u = g_{u}(t), where ˆ+ and g are on T = N_{2}(1) and K: T ↦^{≻}T^{U} for U = 1. Namely, K^{−1}: T^{1} ↦^{≻}T, with T = N_{2}(1) ⊆ A, extends term increments into jump increments, η̂ = η′·K^{−1}. (D) We can perform jump car and cdr by sums: α_{l}(a) = a + ⟨l, ∅⟩ and α_{r}(a) = a + ⟨r, ∅⟩, for all a ∈ A.

Proofs. (A) By 4.1 (I) every w = ∅ + w ∈ W is reduced and is not a d–term. Hence, by (97) and (98) α_{l}(w) = ρ(l, w) = ⟨l, w⟩ and α_{r}(w) = ρ(r, w) = ⟨r, w⟩, while from this an easy word induction on v and 1.8 (E) gets w + v = w ⊕ v ∈ W by (36) and (38).

(B) It follows from 4.2 (B) and (96).

(C) By 1.9 (E) it is enough to show that t + u = t ⊕ u. The trivial upward induction on u that uses (B) as induction step proves it.

(D) By (108), (38), (36) and (105) we get α_{l}(a) = ρ(l, a) = ρ(a ⊕ ⟨l, ∅⟩) = a + ⟨l, ∅⟩ and similarly for α_{r}(a) = a + ⟨r, ∅⟩. Q.E.D.

5.2 Theorem. α is binary invertible.

Proof. One might derive this property from the similar one of two-ary integers in 3.4. Yet, we prefer to provide it with a direct proof.

By (107) and (108) to prove α_{d}(α_{l}(a), α_{r}(a)) = a is to prove ρ(ρ(l, a), ρ(r, a)) = a. To get this for all a ∈ A, by 4.1 (D) we can prove it for all a ∈ W and for all a ∈ D′. When a ∈ W, we get ρ(ρ(l, a), ρ(r, a)) = ρ(⟨l, a⟩, ⟨r, a⟩) = p_{1}(l, a) = a by 4.2 (B), the latter cases of (97) and (98), the former case of

(96) and by (93). When a ∈ D′, by 4.2 (B), the former cases of (97) and

(98) and by (93) we get ρ(ρ(l, a), ρ(r, a)) = ρ(p_{1}(a), p_{2}(a)) = ρ(a) = a. By (108) and (107) to prove α_{l}(α_{d}(a, a′)) = a is to prove ρ(l, ρ(a, a′)) = a.

To get this for all a ∈ A, by 4.1 (D) we can first consider the case of confluent a and a′. In such a case a, a′ ∈ W and a = ⟨l, p_{1}(a)⟩. Therefore, by 4.2 (B) and the former case of (96) we get ρ(l, ρ(a, a′)) = ρ(l, p_{1}(a)) = ρ(a) = a. Then, we consider the case of non confluent a and a′. In such a case ⟨a, a′⟩ ∈ D′ ⊆ A and by the latter case of (96), 4.2 (B), the former cases of

(97) and by (93) we get ρ(l, ρ(a, a′)) = ρ(l, ⟨a, a′⟩) = p_{1}(a, a′) = a. We finally prove α_{r}(α_{d}(a′, a)) = a by the usual replacements, including

the ones for the p_{i}’s. Q.E.D.

5.3 Servi’s clans. Lemma 5.1 (A) shows that jumps extend words both for the operations of affixing a letter and for catenation. Such an extension considers words as “negative” elements as in 4.5, contrary to Servi’s approach, recalled in 0.0, which got clans from “nonnegative words”.

Such opposite considerations lead to different properties of jumps and clans. Non isomorphic clans are uncountably infinite (yet their partial orders are isomorphic), whereas 5.7 will show that we have a single jump algebra up to isomorphisms. The three unary operations of clans satisfy (a disjunction of) two systems of equations, whereas here we exactly got the single Jónsson– Tarski’s system in (111) and (112).

In fact, while the last theorem shows that the jump algebra α is binary invertible, the next one will show that it is the most general among the binary invertible algebras. It will state that for each element b of a binary invertible algebra β there exists a homomorphism h from α into β that send the empty jump to b, h(∅) = b. Namely, α is a free algebra over the binary invertible class. At now, it is with the empty jump as a single free generating element. This restriction will disappear in 5.5.

5.4 Theorems. (A) When β is binary invertible, r′: H_{αβ} ↦^{≻}B. (B) When β = α, the jump increment function is the inverse of the prime representation r′: E_{α} ↦^{≻}A and the image under such a representation of jump endomorphism composition is jump sum. Hence, η′: A ↦^{≻}E_{α} and for all a, b, c ∈ A

(c + b) + a = c + (b + a) and  (114)
∅ + a = a + ∅ = a .  (115)

Proofs. (A) (1-1) Assume r′(h) = r′(k) for h, k ∈ H_{αβ}, namely h(∅) = k(∅). Then, by word induction h(w) = k(w) for all w ∈ W ⊆ A. In fact, when w = ⟨l, v⟩ with h(v) = k(v), by 5.1 (A) and (110) h(w) = h(α_{l}(v)) = β_{l}(h(v)) = β_{l}(k(v)) = k(α_{l}(v)) = k(w) and we can rewrite the same for w = ⟨r, v⟩.

This provides reduced induction with a base to prove h(a) = k(a) for all a ∈ A. When a = ⟨a′, a′′⟩ for non confluent a′a′′ ∈ A with h(a′) = k(a′) and h(a′′) = k(a′′), by 5.1 (B) and (109) h(a) = h(α_{d}(a′, a′′)) = β_{d}(h(a′), h(a′′)) = β_{d}(k(a′), k(a′′)) = k(α_{d}(a′, a′′)) = k(a).

(A) (onto) Given any b ∈ B, define an h: A → B by reduced induction as

h(∅) = b ,
h(l, v) = β_{l}(h(v)) , h(r, v) = β_{r}(h(v)) for all v ∈ W  (116)
and h(a, a′) = β_{d}(h(a), h(a′)) for all ⟨a, a′⟩ ∈ D′. (117)

Then, we only have to prove (110) and (109).

When a is a composed jump, a = ⟨a′, a′′⟩, by (108), (97) and 4.1 (F) h(α_{l}(a)) = h(a′), as a′ = p_{1}(a) ∈ A. Then, by (112), where b = h(a′) and b′ = h(a′′), 4.1 (G) and (117) h(α_{l}(a)) = β_{l}(β_{d}(h(a′), h(a′′))) = β_{l}(h(a′, a′′)) = β_{l}(h(a)). When a is a word, by (108), 5.1 (A), (97) and (116) we immediately get h(α_{l}(a)) = h(l, a) = β_{l}(h(a)). Then, by replacing l with r as usual, we get all of (110).

To get (109), first consider the case of confluent a, a′ ∈ A, which implies a, a′ ∈ W. By (107), (96), (111) and (116) h(α_{d}(a, a′)) = h(p_{1}(a)) = β_{d}(β_{l}(h(p_{1}(a))), β_{r}(h(p_{1}(a)))) = β_{d}(h(l, p_{1}(a))), h(r, p_{1}(a′))) = β_{d}(h(a)), h(a′)), since p_{1}(a) = p_{1}(a′). Then, for the case of non confluent a, a′ ∈ A, by (107), 5.1 (B), (96) and (117) we immediately get h(α_{d}(a, a′)) = h(a, a′) = β_{d}(h(a), h(a′)).

(B) (inverse) By (A) we know that r′: E_{α} ↦^{≻}A. Hence, we only show that for all b ∈ A the endomorphism h in (A) (onto), such that r′(h) = b, for β = α is η′_{b}. By (106) this is to show that

h(a) = h(∅) + a = b + a for all a ∈ A  (118)

and we do by reduced induction on a. The lowest basis step follows from (105), (36) and 4.2 (B): b + ∅ = ρ(b ⊕ ∅) = ρ(b) = b = h(∅).

To get b + ⟨l, v⟩ = h(l, v) from b + v = h(v) for all v ∈ W, start from b ⊕ v ≍ ρ(b ⊕ v) as in 4.2 (A) and get ρ(l, b ⊕ v) = ρ(l, ρ(b ⊕ v)) by (85) and 4.3. Then, by (105), (108), (38) and (116) (with β = α) get b + ⟨l, v⟩ = ρ(b⊕⟨l, v⟩) = ρ(l, b⊕v) = ρ(l, ρ(b⊕v)) = ρ(l, b+v) = α_{l}(b+v) = α_{l}(h(v)) = h(l, v). The same for b + ⟨r, v⟩ = h(r, v).

For the remaining step, h(a, a′) = b + ⟨a, a′⟩ from two premises as in (118), we first get ρ(ρ(b ⊕ a), ρ(b ⊕ a′)) = ρ(b ⊕ a, b ⊕ a′) as before. Then, h(a, a′) = α_{d}(h(a), h(a′)) = α_{d}(b + a, b + a′) = ρ(b + a, b + a′) = ρ(ρ(b ⊕ a), ρ(b⊕a′)) = ρ(b⊕a, b⊕a′) = ρ(b⊕⟨a, a′⟩) = b+⟨a, a′⟩, follows from (117) (with β = α), (107), (105) and (37).

(B) (jump sum) Finally, we get r′(h′′)+r′(h′) as the representation r′(h′′ · h′) of composition, for all h′′, h′ ∈ E_{α}, merely by (118). In fact, by (113) this is to prove that h′′(∅) + h′(∅) = h′′(h′(∅)) and, if we set a = h′(∅) and h = h′′ in (118), we find that we already proved it by reduced induction on h′(∅). Since jump sum is isomorphic to the composition of endomorphisms,

(114) and (115) are trivial. Anyway, we can get them as in 1.8 (A). Q.E.D.

5.5 Jump Arithmetics. The finding that the jump algebra is the free binary invertible algebra is a test for semantic constructions. In fact, both the problem of transforming binary (or LISP) trees and the latter algebra are known since half century, without any acknowledgment that the problem solution is this algebra.

Early LISP versions [29] embodied some embryonic jumps (the extensions of car and cdr to the primitives corresponding to our words) and observed some of the Jónsson–Tarski’s identities. Yet, later on [28] this was relinquished and no free algebra appeared.

Conversely, since [7] appeared, this free algebra was the subject of an extensive work, e.g. see [26], [4], [27] and [9]. Yet, they neither perceived its relevance to binary trees nor developed its arithmetic.

Here, the sum of jumps begins such a development. Such an operation comes from 5.4 (B), which is an instance of the general theory of Universal Matrices, recalled in 0.3. Since we are concerned with semantic constructions, we will not develop it any further.

However, from the recalled algebraic work Universal Matrices provide us a preview of such arithmetics. E. Marczewski found that this free algebra has bases with every finite positive number of generators, see §31 in [5]. This implies that it is free with any such number of generators. It also implies that for each such a base we have a product of “(square) universal matrices” with as many “columns” as the generators.

Such products define “analytic monoids” of any dimension as in [20]. Every analytic monoid defines an arithmetic for jumps. Some of such arithmetics will collapse into a single one up to jump “transformations”. For instance, with a singleton base its arithmetic is the one of our jump sum, because the isomorphism sending its generator to the empty jump provides its (one-dimensioned) analytic monoid with the required transformation.

Such collapsing transformations will generate a hierarchy of arithmetics. We do not yet know neither its structure (the theory of Universal Transformations has yet to appear in print) nor the single arithmetics. Still, two-ary integers promise to be arithmetically rich, yet different from usual integers.

5.6 Algebras as pairs. All textbooks of Algebra and Universal Algebra define a (homogeneous) algebra as a pair ⟨A, F ⟩, where A denotes its carrier set and F denotes either a set of operations on A or a function indexing them. (The reason to call it “function”, instead of “family”, is in 0.6 of [20].) In our algebras, on the contrary, only an F occurs, in the form of an indexing function α or β, see also τ′ in 1.1.

The main reason for disregarding such textbooks is that none of them motivates such pairs, while the theory we are using (the one of analytic monoids) does not need them. Another (trivial) reason is set-theoretical: most (homogeneous total) operations determines their carrier, e.g. for α_{l}: A → A the carrier is Dom α_{l}. This makes our algebras equivalent to conventional algebras in all practical cases.

In fact, the only exception is an algebra where F contains (or indexes) nullary operations only. Then, given such an F, we have an algebra ⟨A, F ⟩ for every superset A of the set B of the corresponding constant values, whereas here we have just one algebra F. However, even such a difference does not concern the theory of analytic monoids or universal matrices. Their “spaces” correspond to free algebras and it is easy to see that our ⟨A, F ⟩ is free iff A = B, namely we have to loose this proliferation anyway.

5.7 Definitions. By 5.4 (B) the sum and ∅ form a monoid that we call the prime analytic monoid. (Recall that by 5.0 in this monoid the composition of u with a is a + u, see also [18].) On the contrary, we call sum monoid the reversed one where the composition of u with a is u + a.

5.8 Corollary. The prime semantic s′ is an isomorphism from the sum monoid onto the prime semantic monoid. Hence, s′ · r′ is an isomorphism from the jump endomorphism monoid onto the prime semantic monoid, up to a composition reversal.

Proof. By 4.7 (A) s′: A ↦^{≻}S′. For all a, u ∈ A, S′ ∋ s′_{a+u} = σ_{a+u} = σ_{ρ(a⊕u)} ⊇ σ_{a⊕u} = σ_{u} · σ_{a} ∈ Σ, by (105), 4.2 (A), 4.4 (A) and 2.2 (B). Hence, s′_{a+u} = ϱ(s′_{u}· s′_{a}) = s′_{u}⊙ s′_{a} as in 4.6. Finally, s′_{∅} = σ_{∅} = i_{T} by (61). Therefore, s′ is the required isomorphism and by 5.4 (B) also s′ · r′ is, up to the reversal in 5.7. Q.E.D.

Acknowledgments. K. Głazek (T.U. of Zielona Góra), S. Martini (U. of Udine) and M. Servi (U. of Parma) provided the Author with interesting references and helpful talks. Thirty six years ago G. Degli Antoni (U. of Milan) was the first who told the Author about LISP.

References

[0] G.J. Chaitin, Algorithmic Information Theory, IBM J. Res. Develop. 21 (1977), 350–359, 496.

[1] G.J. Chaitin, Information-Thoretic Incompleteness (World Scientific, Singapore, 1992).

[2] R. Chuaqui, Axiomatic Set Theory (Nort–Holland, Mathematics Studies, Amsterdam, 1981).

Two-ary integers 51

[3] H.B. Curry, R. Feys and W. Craig, Combinatory Logic, 1, (North–Holland, Amsterdam, 1959).

[4] A. Goetz & C. Ryll-Nardzewski, On bases of abstract algebras, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 8 (1960), 157–161.

[5] G. Grätzer, Universal Algebra, 2^{th} ed., (Springer–Verlag, New York, 1979).

[6] J.R. Hindley and J.P. Seldin, Introduction to Combinators and λ–Calculus (Cambridge University Press, London, 1986).

[7] B. Jónsson & A. Tarski, Two general theorems concerning free algebras, Bull. Amer. Math. Soc. 62 (1956), 554.

[8] E.G. Manes, Algebraic theories (Springer–Verlag, Berlin, 1976).

[9] E. Marczewski, Independence and homomorphisms in abstract algebras, Fund. Math. 50 (1961–62), 45–61.

[10] I. Mason & C. Talcott, Inferring the equivalence of functional program that mutate data, Theoretical Computer Science 105 (1992), 167–215.

[11] M.L. Minsky, Problems of formulation for Artificial Intelligence, in R.E. Bellman, Mathematical Problems in the Biological Sciences, Proceedings of Symposia in Applied Mathematics XIV, American Mathematical Society, Providence, R.I. 1962, p. 35.

[12] J.D. Monk, Introduction to Set Theory (McGraw–Hill, New York, 1969).

[13] G. Ricci: A Whitehead generator, Quaderni del Dipartimento di Matematica 86, (Universitá di Parma, Parma, 1993).

[14] G. Ricci, Universal eigenvalue equations, Pure Math.and Appl. Ser. B, 3, 2– 3–4 (1992), 231–288. (Most of the misprints appear in ERRATA to Universal eigenvalue equations, Pure Math.and Appl. Ser. B, 5, 2 (1994), 241–243.)

[15] G. Ricci, Two isotropy properties of “universal eigenspaces” (and a problem for DT0L rewriting systems), in: G. Pilz, Contributions to General Algebra 9 (Verlag Hölder–Pichler–Tempsky,Wien 1995 – Verlag B.G. Teubner), 281-290.

[16] G. Ricci, New characterizations of universal matrices show that neural networks cannot be made algebraic, in: D. Dorninger, G. Eigenthaler, H.K. Kaiser, H. Kautschitsch, W. Moren & W.B. Müller, Contributions to General Algebra 10 (J. Hein Verlag, Klagenfurt, 1998), 269-291.

[17] G. Ricci, Analytic monoids, Quaderni del Dipartimento di Matematica 238, (Universitá di Parma, Parma, 2000).

[18] G. Ricci, Boolean matrices … neither Boolean nor matrices, Discuss. Math. General Algebra and Applications 20 (2000), 141–151.

[19] G. Ricci: Isomorphisms between analytic monoids, The Eighth International Workshop in Mathematics Gronów 2000, Institute of Mathematics, Technical University of Zielona Góra, September 25-29, 2000, 33-33.

52 G. Ricci

[20] G. Ricci: Some analytic features of algebraic data, Discrete Appl. Math. 122/1-3 (2002), 235–249.

[21] G. Ricci: A semantic construction of two-ary integers, Quaderni del Dipartimento di Matematica 359, (Universitá di Parma, Parma, 2004)

[22] M. Servi, Classificazione dei Clan binari, Quaderni del Dipartimento di Matematica 113, (Universitá di Parma, Parma, 1995).

[23] M. Servi, Definizione dei clan binari e loro classificazione, Rend. Mat. Acc. Lincei (9) 9 (1998).

[24] M. Servi, Due parole sui Clan di Ordine, Quaderni del Dipartimento di Matematica 186, (Universitá di Parma, Parma, 1998).

[25] M. Servi, I clan binari di ordine, Riv. Mat. Univ. Parma (6) 1 (1998), 207–214.

[26] S. Świerckowski, Algebras independently generated by every n elements, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 7 (1959), 501–502.

[27] S. Świerckowski, Algebras which are independently generated by every n elements, Fund. Math. 49 (1960–61), 93–104.

[28] D.S. Touretzky, Common LISP: a Gentle Introduction to Symbolic Computation (The Benjamin/Cummings Publishing Co. Inc, Redwood City, 1990).

[29] C. Weissman, LISP 1.5 Primer (Dickenson, Belmont, Ca., 1967).

Author’s Address: Gabriele Ricci Universitá di Parma Dipartimento di Matematica, I–43100 Parma, Italy. Telephone: (Italy) 02 – 2841574 Fax: (Italy) 0 521 – 032350 E-mail: gabriele.ricci@unipr.it

Stampato in proprio dal Dipartimento di Matematica dell’Universitá di Parma In Via M. D’Azeglio 85/A 43100 Parma, adempiuti gli obblighi di cui all’articolo 1 del D.L. 31 agosto 1945 n. 660.