Open bvssvni opened 7 years ago
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.
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.
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:
To enumerate such functions, create a
PowerSet<Of<DimensionN>>
space with the discrete library and use dimensionvec![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: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 -> ()
:unit
functionThe
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
:false_0
functiontrue_0
functionThis is the first space that contains boolean functions. There are only 2 functions.
Unary space
a -> a
:id
(boolean) functionnot
functionThis space also contains
false_1
andtrue_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
This sequence can be used to count boolean functions that depends on all its arguments.