Finding paths from discrete spaces of all functions

[bvssvni]

This method uses discrete combinatorics and is comparatively novel compared to other search techniques. It is very interesting from a philosophical perspective of path semantics.

Background

The idea is to exploit some functions that has known output for all inputs. Such functions can be given a unique natural number in the discrete space of their types. Paths become a number connected to another number, by other numbers. Theorems about which paths exists become theorems about relations between numbers.

When studying path semantics, one can consider the space of all functions of a given type, and then examine the paths to another space of a given type. As long as the input arguments are finite and the function returns, one can enumerate all possible functions. This method is only practical for very small number of inputs.

Boolean functions

In practice, this method is restricted to very simple functions, such as boolean functions, but it is also interesting in seeing how this generalizes to other functions. A boolean function takes N boolean values and produces 1 boolean value.

The number of boolean functions of N variables is:

2^(2^N)

To enumerate such functions, create a PowerSet<Of<DimensionN>> space with the discrete library and use dimension vec![2; n].

Irrelevant arguments

An interesting property of such spaces is that they must contain all smaller spaces. If there exists a function type bool -> bool then its space must contain all functions of type () -> bool. Using asymmetric path semantics, we can write:

f: bool -> bool

// Expresses the asymmetric path, removing the argument.
f[unit -> id]

unit : a -> ()
unit _ = ()

id : a -> a
id x = x

Natural hierarchy

Even for simple boolean functions, we see how functions sneak in just the right moment to connect new spaces. For all paths, you can only use functions that belongs to a space of functions with an equal or less number of functions. Therefore, the spaces form a natural hierarchy in path semantical space.

Top space a -> ():

• The unit function

The unit function naturally belongs to the top space. Here you erase input, but there is no output. This space is not a boolean function.

Constant space () -> a:

• The false_0 function
• The true_0 function

false_0 := \() = false
false_0[id -> unit] <=> unit::<()>

This is the first space that contains boolean functions. There are only 2 functions.

Unary space a -> a:

• The id (boolean) function
• The not function

This space also contains false_1 and true_1 functions. There are 2 new functions besides the ones that have an irrelevant argument.

Binary space a x a -> a:

• and, nand, or, nor, exc, nexc, rexc, nrexc, xor, eq

There are 10 new functions besides the ones that have an irrelevant argument.

Number of nondegenerate Boolean functions of n variables.

http://oeis.org/A000371

2, 2, 10, 218, 64594, 4294642034, 18446744047940725978, 340282366920938463334247399005993378250, 11579208923731619542357098500868790785054772573027305633226709598228233779856

This sequence can be used to count boolean functions that depends on all its arguments.

[bvssvni]

One interesting observation is that there exists paths from functions with unbounded inputs, such that their space of functions is infinite, to functions with bounded inputs, which has a finite space of functions.

For example:

add[even] <=> eq

There is no way to construct the discrete space of functions for add that take all natural numbers. However, if you choose some bounds then you might assume that the path holds up to any arbitrary bound, and therefore in general holds for all natural numbers.

The magic is in the path generator even that maps from arbitrary bounds to a fixed one. Some insight could be taken from the number representation of even in relation to the size of the whole function space.

[bvssvni]

Here is an interesting idea:

The functions that take unbounded inputs could be interpreted as dependent types, such that they actually cross the boundary between function spaces. One dependent function can be split into normal functions, each belonging to a finite function space.

For example, in the case of arrays, the first argument can tell how many times the type of the next argument is repeated:

(0) => ()
(1, item, item) => (a, a)
(2, item, item, item) => (a, a, a)

An array of length N belongs to N number of finite function spaces. The function concat takes two arrays of length N and M, so it intersects with N*M finite function spaces.

One can view a dependent function as a higher order function that outputs the finite functions. This supports the idea that higher cardinality of infinities is related to higher order functions.