One-level symmetric path equality

[bvssvni]

This is a particular kind of knowledge of the form:

Algorithm [Property] = Hypothesis

For example:

and [not] = or
add [odd] = xor
mul [is_zero] = or
concat [len] = add
concat [sum] = add
concat [max] = max_bin
concat [min] = min_bin
concat [prod] = mul

For example, if the algorithm is add, then the property odd behaves under add according to the hypothesis xor. With other words, if you add two odd or two even numbers, you get an even number. Otherwise, you get an odd number.

Symmetric types

A symmetric path means the type of inputs and return value must be the same.

For example:

add(num, num) -> num

Orthogonal to type knowledge

A member of a type is a function from the type to itself, for example:

true(bool) -> true

The extended axiom of equality https://github.com/bvssvni/path_semantics/issues/100 disallows cycles such as:

bool(bool) -> bool

It is is therefore known that knowledge inferred from equations of one-level symmetric path equality is orthogonal to type knowledge. These two forms of knowledge forms basic concepts.

Testing is trivial

For all deterministic algorithms, a one-level symmetric path equality is trivial to test. If it is true for all inputs, then this is a proof of Hypothesis.

For example, it is easy to check and [not] = or for all inputs:

not(and(not(false), not(false))) = false
not(and(not(false), not(true))) = true
not(and(not(true), not(false))) = true
not(and(not(true), not(true))) = true

Empirical testing

For many algorithms, it is not possible to check for all inputs, or equality is ambiguous. Instead, one can use the following method:

• If it is not possible to check for all inputs, a random input can be generated from a closure
• If equality is ambiguous, one can use a closure

Assume we have a closure RandomSample and Equality, we can run an algorithm like this:

n := 1000
all i n {
    S := \RandomSample()
    \Equality(\Property(Algorithm(S)), \Hypothesis(\Property(S)))
}

This is also considered trivial testing.

Automatic derivation

Since testing is trivial, one can take a list of functions and generate all possible one-level symmetric path equations. By testing each of them, one can generate all this kind of knowledge.

The knowledge can be reproducible by representing this as a list of 5 closures:

• Algorithm
• Property
• Hypothesis
• Equality
• RandomSample

Complete, monotonic, precise and basic knowledge

The knowledge about one-level symmetric path equations have the following properties:

• Complete, which means that all input values are covered
• Monotonic, which means it is true no matter what else might be discovered about Algorithm
• Precise, which means everything that is possible to infer further can be known from Hypothesis, independently of the existence of Algorithm
• Basic, which means it is the shortest way of representing non-compositions of knowledge

Tuple paths

It follows from tuple paths (https://github.com/bvssvni/path_semantics/issues/101) that since:

concat [len] = add
concat [sum] = add

then:

concat [(len, sum)] = (add, add)

This is a composition and therefore not basic knowledge.

Meta^N property

All meta-properties that one-level symmetric path equations have, can be defined in terms of one-level symmetric path equations, because the knowledge is complete, monotonic, precise and basic.

These definitions can then be carried over to asymmetric paths. This is the same for meta knowledge about meta-properties, meta knowledge about meta knowledge about meta-properties and so on. It called the "Meta^N property".

In other words, a motivation to study on-level symmetric path equations is to derive meta knowledge.