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.
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 => aandy => bwhere=>is evaluation, then the evaluation is uniform.This means that both
x => aandy => bare 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
Nonefor a case where the partial order is yet to be determined.Nonecan 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 forxandy, respectively. When(x, y)and(z, x)is reserved for allyandz, the reservation is total forx.Well Ordering
xis well ordered when(x, y)for anyyis either:Partial Order Reservation of Non-Evaluated Expressions
When
x => a, where=>is evaluation: Whenxis not identical toa, it follows thatxhas not been evaluated.In that case, as long
ais well ordered,xcan 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.