background image

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

[

im

a

dom

a

| ∀

i

dom

a

:

z

(

i

)

a

i

 

.

Obvious 3.

If

a

is a small function, then

Q

a

=

{

z

dom

a

| ∀

i

dom

a

:

z

(

i

)

a

i

}

.

2.1 Currying and uncurrying

2.1.1 The customary definition

Let

X

,

Y

,

Z

are 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

) = (

fx

)

y

.

Obvious 4.

1. uncurry

(

curry

(

f

)) =

f

for every

f

Z

X

×

Y

.

2. curry

(

uncurry

(

f

)) =

f

for every

f

(

Z

Y

)

X

.

2.1.2 Currying and uncurrying with a dependent variable

Let

X

,

Z

are sets and

Y

is a function with the domain

X

. (Vaguely saying,

Y

is a variable dependent

on

X

.)

The disjoint union

`

Y

=

S

{{

i

} ×

Y

i

|

i

dom

Y

}

=

{

(

i

;

x

)

|

i

dom

Y , x

Y

i

}

.

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

) = (

fx

)

y

.

Obvious 5.

1. uncurry

(

curry

(

f

)) =

f

for every

f

Z

`

i

X

Y

i

.

2. curry

(

uncurry

(

f

)) =

f

for every

f

Q

i

X

Z

Y

i

.

Remark 6.

There is nothing said anything about currying with dependent variables in Wikipedia.

Am I really the first person who formulated this simple generalization of currying and uncurrying?

2.2 Functions with ordinal numbers of arguments

Let Ord is the set of small ordinal numbers.

If

X

and

Y

are sets and

n

is an ordinal number, the set of functions taking

n

arguments on

the set

X

and returning a value in

Y

is

Y

X

n

.

The set of all small functions taking ordinal numbers of arguments is

Y

S

n

Ord

X

n

.

I will denote OrdVar

(

X

) =

S

n

Ord

X

n

and call it

ordinal variadic

. (“Var” in this notation is

taken from the word

variadic

in the collocation

variadic function

used in computer science.)

3 On sums of ordinals

Let

a

is an ordinal-indexed family of ordinals.

2

Section 3