ietf-wg-jsonpath / draft-ietf-jsonpath-base

Development of a JSONPath internet draft
https://ietf-wg-jsonpath.github.io/draft-ietf-jsonpath-base/
Other
59 stars 20 forks source link

Frame <= in terms of < or == and >= in terms of > or == #245

Closed glyn closed 2 years ago

glyn commented 2 years ago

According to the current draft certain types, such as Booleans, are unordered:

However, <= is often understood the way it is read: "less than or equal to". Similarly for >=.

If we could define <= as "< or ==" and >= as "> or ==", then they could be easier to understand.

With this change true <= true, for example, would yield true (whereas according to the current draft, it yields false).

Total orders

There is often an assumption that orderings are "total" or "linear" (see wikipedia for a definition). A total order obeys the following laws:

a < b if and only if not b <= a
a > b if and only if not b >= a

But according to the current draft, for example, false < true and true <= false both yield false, contrary to the first of the above laws. This is because the ordering of Boolean values is not total.

In the discussion at today's interim meeting (2022-08-17), it was suggested that the above laws could cause a problem for this issue. This does not appear to be the case because we are not dealing with total orders.

cabo commented 2 years ago

The above section about </>= is phrased in terms of total orders; I believe this is a POLS violation as most people will not think in terms of total orders here.

glyn commented 2 years ago

@cabo Ok. That section isn't necessary: I was merely trying to capture the concern you expressed in the meeting. Please could you explain your concern with the above proposal (ignoring the "Total orders" section)?

glyn commented 2 years ago

Note to self: to avoid delta clashes, I intend to wait for the following PRs to land or close before submitting a PR for this issue:

glyn commented 2 years ago

Note to self (and anyone else who finds mathematics helpful)...

tl;dr

With the proposed change, a <= a for all a including when a is "absent", an object, an array, a boolean, or null.

Apart from that <= is just as in the current draft.

Similarly for >= which can be dealt with similarly.

Reflexive closure

The ordering <= in the current draft is almost a partial order. That is, the following are true for all a, b, c:

a <= a (reflexive)
if a <= b and b <= c then a <= c (transitive)
if a <= b and b <= a then a == b (antisymmetric)

except that the reflexive axiom is not true if a or b are "absent", an object, an array, a boolean, or null.

When restricted to numbers or restricted to strings <= is a total order. That is if a and b are both numbers or both strings, then in addition to the partial order axioms, the following is true:

a <= b or b <= a (strongly connected)

Note: <= is not a total order when restricted to arrays (if we decide to support <= for arrays), since, for example:

not [true] <= [false], and
not [false] <= [true]

The ordering < in the current draft is a strict partial order:

not a < a  (irreflexive)
if a < b then not b < a (asymmetric)
if a < b and b < c then a < c (transitive)

The reflexive closure of < defines <= in terms of <:

a <= b if and only if (a < b or a == b)

The result is the same as in the current draft except that a <= a for all a. So, for example, $.absent <= $.absent (where $.absent is "absent", since $.absent == $.absent), true <= true, null <= null and $.obj1 <= $.obj2 (where $.obj1 and $.obj2 are objects for which $.obj1 == $.obj2).

So <= is a partial order (without exception) and is still a total order when restricted to numbers or when restricted to strings.

glyn commented 2 years ago

NB. if https://github.com/ietf-wg-jsonpath/draft-ietf-jsonpath-base/pull/248 lands, [true] <= [true] is false, but with the above proposal it would be true.