Assumptions about partial order

[bvssvni]

Joker Calculus has two variants of normalization. This makes it harder to reason about partial orders.

This issue keeps track of various assumptions about partial order.

Uniform Evaluation

If x => a and y => b where => is evaluation, then the evaluation is uniform.

This means that both x => a and y => b are evaluated using same variant of Open/Closed.

The motivation for this assumption is that it seems weird to think about order by two different variants.

Partial Order Reservation

Partial Order can return None for a case where the partial order is yet to be determined.

None can mean "known unknown" (reserved for all times) or "unknown unknown" (reserved for some unknown time).

A reservation happens for an ordered pair (x, y).
This implies that a partial reservation exists for x and y, respectively.
When (x, y) and (z, x) is reserved for all y and z, the reservation is total for x.

Well Ordering

x is well ordered when (x, y) for any y is either:

• Defined
• Reserved

Partial Order Reservation of Non-Evaluated Expressions

When x => a, where => is evaluation:
When x is not identical to a, it follows that x has not been evaluated.

In that case, as long a is well ordered, x can be reserved.

This is possible because one can just evaluate x.
However, this does not imply whether one ought to evaluate of some variant Open/Closed.

Asymmetry

If (x, y) is defined then (y, x) is defined with inverted ordering.