background image

3.8. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

40

3.8.2. Used notation.

We identify natural numbers with finite Von Neu-

mann’s ordinals (further just

ordinals

or

ordinal numbers

).

For simplicity we will deal with small sets (members of a Grothendieck uni-

verse). We will denote the Grothendieck universe (aka

universal set

) as

f

.

I will denote a tuple of n elements like

J

a

0

;

. . .

;

a

n

1

K

. By definition

J

a

0

;

. . .

;

a

n

1

K

=

{

(0;

a

0

)

, . . . ,

(

n

1;

a

n

1

)

}

.

Note that an ordered pair (

a

;

b

) is not the same as the tuple

J

a

;

b

K

of two

elements.

Definition

230

.

An

anchored relation

is a tuple

J

n

;

r

K

where

n

is an index set

and

r

is an

n

-ary relation.

For an anchored relation arity

J

n

;

r

K

=

n

. The graph

1

of

J

n

;

r

K

is defined as

follows:

GR

J

n

;

r

K

=

r

.

Definition

231

.

Pr

i

f

is a function defined by the formula

Pr

i

f

=

x

i

x

f

for every small

n

-ary relation

f

where

n

is an ordinal number and

i

n

. Particularly

for every

n

-ary relation

f

and

i

n

where

n

N

Pr

i

f

=

x

i

J

x

0

;

. . .

;

x

n

1

K

f

.

Recall that Cartesian product is defined as follows:

Y

a

=

(

z

(

S

im

a

)

dom

a

i

dom

a

:

z

(

i

)

a

i

)

.

Obvious

232

.

If

a

is a small function, then

Q

a

=

n

z

f

dom

a

i

dom

a

:

z

(

i

)

a

i

o

.

3.8.2.1.

Currying and uncurrying.

The customary definition.

Let

X

,

Y

,

Z

be sets.

We will consider variables

x

X

and

y

Y

.

Let a function

f

Z

X

×

Y

. Then curry(

f

)

(

Z

Y

)

X

is the function defined by

the formula (curry(

f

)

x

)

y

=

f

(

x

;

y

).

Let now

f

(

Z

Y

)

X

. Then uncurry(

f

)

Z

X

×

Y

is the function defined by the

formula uncurry(

f

)(

x

;

y

) = (

f x

)

y

.

Obvious

233

.

1

. uncurry(curry(

f

)) =

f

for every

f

Z

X

×

Y

.

2

. curry(uncurry(

f

)) =

f

for every

f

(

Z

Y

)

X

.

Currying and uncurrying with a dependent variable.

Let

X

,

Z

be sets and

Y

be a function with the domain

X

. (Vaguely saying,

Y

is a variable dependent on

X

.)

The disjoint union

`

Y

=

S

n

{

i

Y

i

i

dom

Y

o

=

n

(

i

;

x

)

i

dom

Y,x

Y

i

o

.

We will consider variables

x

X

and

y

Y

x

.

Let a function

f

Z

`

i

X

Y

i

(or equivalently

f

Z

`

Y

). Then curry(

f

)

Q

i

X

Z

Y

i

is the function defined by the formula (curry(

f

)

x

)

y

=

f

(

x

;

y

).

Let now

f

Q

i

X

Z

Y

i

. Then uncurry(

f

)

Z

`

i

X

Y

i

is the function defined

by the formula uncurry(

f

)(

x

;

y

) = (

f x

)

y

.

Obvious

234

.

1

It is unrelated with graph theory.