 3.8.4 Ordinated product

3.8.4.1 Introduction

Ordinated product

dened below is a variation of Cartesian product, but is associative unlike Carte-

sian product. However, ordinated product unlike Cartesian product is dened 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.8.4.2 Concatenation

Denition 3.81.

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

:

Obvious 3.82.

If

z

is a nite family of nitary typles, it is concatenation of dom

z

tuples in the

usual sense (as it is commonly used in computer science).

Proposition 3.83.

If

z

2

Q

(

GR

F

)

then concat

z

=

uncurry

(

z

)

(

L

(

arity

F

))

¡

1

.

Proof.

If

z

2

Q

(

GR

F

)

then dom

z

(

i

) =

dom

(

GR

F

)

i

=

dom

F

i

=

arity

F

i

for every

i

2

dom

F

.

Thus dom

z

=

arity

F

.

Proposition 3.84.

dom concat

z

=

P

i

2

dom

z

dom

z

i

.

Proof.

Because dom

(

L

(

dom

z

))

¡

1

=

P

i

2

dom

F

dom

z

i

, it is enough to prove that

dom uncurry

(

z

) =

dom

M

(

dom

z

)

:

Really,

dom

M

(

dom

z

) =

f

(

i

;

x

)

j

i

2

dom

(

dom

z

)

; x

2

dom

z

i

g

=

f

(

i

;

x

)

j

i

2

dom

z; x

2

dom

z

i

g

=

a

z

and dom uncurry

(

z

) =

`

i

2

X

z

i

=

`

z

.

3.8.4.3 Finite example

If

F

is a nite family (indexed by a natural number dom

F

) of anchored nitary relations, then by

denition GR

Q

(

ord

)

F

=

f

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

J

a

0

;

0

;

:::

;

a

0

;

arity

F

0

¡

1

K

2

GR

F

0

^

:::

^

J

a

dom

F

¡

1

;

arity

F

dom

F

¡

1

¡

1

K

2

GR

F

dom

F

¡

1

g

and

arity

Y

(

ord

)

F

=

arity

F

0

+

:::

+

arity

F

dom

F

¡

1

:

The above formula can be shortened to

GR

Y

(

ord

)

F

=

concat

z

j

z

2

Y

(

GR

F

)

:

3.8.4.4 The denition

Denition 3.85.

The anchored relation (which I call

ordinated product

)

Q

(

ord

)

F

is dened by

the formulas:

arity

Y

(

ord

)

F

=

X

(

arity

F

);

GR

Y

(

ord

)

F

=

concat

z

j

z

2

Y

(

GR

F

)

:

Proposition 3.86.

Q

(

ord

)

F

is a properly dened anchored relation.

3.8 Infinite associativity and ordinated product

45