 3.7. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

50

3.7.4. Ordinated product.

3.7.4.1.

Introduction. Ordinated product

defined below is a variation of Carte-

sian product, but is associative unlike Cartesian product. However, ordinated prod-

uct unlike Cartesian product is defined not for arbitrary sets, but only for relations

having ordinal numbers of arguments.

Let

F

indexed by an ordinal number be a small family of anchored relations.

3.7.4.2.

Concatenation.

Definition

295

.

Let

z

be an indexed by an ordinal number family of functions

each taking an ordinal number of arguments. The

concatenation

of

z

is

concat

z

= uncurry(

z

)

M

(dom

z

)

1

.

Exercise

296

.

Prove, that if

z

is a finite family of finitary tuples, it is con-

catenation of dom

z

tuples in the usual sense (as it is commonly used in computer

science).

Proposition

297

.

If

z

Q

(GR

F

) then concat

z

= uncurry(

z

)

(

L

(arity

F

))

1

.

Proof.

If

z

Q

(GR

F

) then dom

z

(

i

) = dom(GR

F

)

i

= arity

F

i

for every

i

dom

F

. Thus dom

z

= arity

F

.

Proposition

298

.

dom concat

z

=

P

i

dom

z

dom

z

i

.

Proof.

Because dom(

L

(dom

z

))

1

=

P

i

dom

f

(dom

z

), it is enough to

prove that

dom uncurry(

z

) = dom

M

(dom

z

)

.

Really,

X

i

dom

f

(dom

z

) =

(

i, x

)

i

dom(dom

z

)

, x

dom

z

i

=

(

i, x

)

i

dom

z, x

dom

z

i

=

a

z

and dom uncurry(

z

) =

`

i

X

z

i

=

`

z

.

3.7.4.3.

Finite example.

If

F

is a finite family (indexed by a natural number

dom

F

) of anchored finitary relations, then by definition

GR

(ord)

Y

=

J

a

0

,

0

, . . . , a

0

,

arity

F

0

1

, . . . , a

dom

F

1

,

0

, . . . , a

dom

F

1

,

arity

F

dom

F

1

1

K

J

a

0

,

0

, . . . , a

0

,

arity

F

0

1

K

GR

F

0

. . .

J

a

dom

F

1

,

arity

F

dom

F

1

1

K

GR

F

dom

F

1

and

arity

(ord)

Y

F

= arity

F

0

+

. . .

+ arity

F

dom

F

1

.

The above formula can be shortened to

GR

(ord)

Y

F

=

concat

z

z

Q

(GR

F

)

.