32 Universal Navigation

Ordinary navigation reaches values that can be reached from at least one current value. Universal navigation reaches values that can be reached from every current value.

For example, the following expression reaches the teaching days used by every advanced course:

u.course.[advanced]⇒session.time.day

A day is output only if each advanced course has some session on that day. The left side, u.course.[advanced], supplies the courses being tested. The right side, session.time.day, is tested from each of those courses.

The logical shape is:

day=D:Day
where
  ∀C:Course ∀A:Boolean
    (u.course(C) ∧ C.advanced(A) ∧ A)
  → ∃S:Session ∃T:TimeSlot
      C.session(S)
    ∧ S.time(T)
    ∧ T.day(D)

For every advanced course C, the right-hand path must be able to reach the output day D.

Ordinary navigation versus universal navigation

Changing ⇒ to . changes the meaning:

u.course.[advanced].session.time.day

This reaches days used by at least one advanced course. The universal version:

u.course.[advanced]⇒session.time.day

reaches only days used by all advanced courses. Ordinary navigation is like a union of what each current value can reach. Universal navigation is like an intersection of what each current value can reach.

Asking whether all values satisfy a condition

Often a universal requirement is easiest to write by looking for counterexamples. This expression reaches courses that have no assessment worth more than 60 percent:

u.course.[assessment.[weight > 60].Σempty]

The inner filter reaches the bad assessments. Σempty then says that there are none. This pattern is often the clearest way to say "all reached values satisfy the condition".

Using folds and subset tests

Another common pattern is to collect reached values with .Σ, then compare sets. For example, this expression reaches advanced courses whose prerequisites are all mathematics courses:

u.course.[advanced].[
    prerequisite.Σ ⊆ u.department.[name = "Mathematics"].course.Σ
]

Here the requirement is naturally a set inclusion. The left side is the set of prerequisites of the current course. The right side is the set of courses offered by the mathematics department.

Relation to relational division

Universal navigation is the path-expression form of division-style queries. A division query asks for the values related to all values in some divisor relation. In the first example, the divisor is the advanced courses, and the result contains days related to every one of those courses by the session.time.day path.

The classic supplier-parts query "suppliers who supply all parts" has exactly this shape:

In Tutorial D, it can be written using non-existence:

S WHERE NOT EXISTS (
    P WHERE NOT EXISTS (
        SP WHERE SP.S# = S.S#
           AND SP.P# = P.P#
    )
)

It can also be written using DIVIDEBY:

S MATCHING (
    SP { S#, P# }
    DIVIDEBY P { P# }
    PER ( S { S# } )
)

In Predica, universal navigation gives the same query directly:

s.part⇒(shipment.supplier)

The left side supplies the required parts. The right side reaches the suppliers for each part. The output suppliers are those reached from every part.

Adding a filter gives the usual "suppliers who supply all red parts" query:

In Tutorial D, the non-existence form is:

S WHERE NOT EXISTS (
    (P WHERE COLOR = 'Red')
    WHERE NOT EXISTS (
        SP WHERE SP.S# = S.S#
           AND SP.P# = P.P#
    )
)

The corresponding DIVIDEBY form is:

S MATCHING (
    SP { S#, P# }
    DIVIDEBY (P WHERE COLOR = 'Red') { P# }
    PER ( S { S# } )
)

In Predica, the filter is part of the left side of the universal navigation:

s.part.[color = Color.red]⇒(shipment.supplier)

The DIVIDEBY versions make the relation to relational division explicit. In practice, Tutorial D users will often prefer the non-existence form: choose the candidate values for which there does not exist a required value with no matching relationship. Universal navigation packages that double-negation pattern into a path operator.

Choosing the universal pattern

There are three common ways to express universal requirements. The best choice usually depends on the sentence you are trying to write.

prerequisite.Σ ⊆
  u.department.[name="Mathematics"].course.Σ

u.course.[
    assessment → assessment.weight ≤ 60
]

The difference is that Σempty tests for absence, a.Σ ⊆ b.Σ compares two collected sets, ⇒ produces common reachable values, and → states a conditional requirement.

Using → inside a filter often makes universal quantification appear when the frame condition is written out. The implication itself is the condition, but the witnesses used by its antecedent are usually universally closed when the filter is rendered. This is why:

u.course.[assessment → assessment.weight ≤ 60]

reads like "courses for which every assessment has weight at most 60". The same idea can also be written by looking for no counterexamples:

u.course.[assessment.[weight > 60].Σempty]

The two expressions approach the universal requirement from different directions. The first says what must follow from each reached assessment. The second says there are no reached assessments that break the rule.

Do not reach for it too soon

Universal navigation is powerful, but it is not the only way to write universal requirements. Use ⇒ when the result should be values reachable from every left-side value. Use Σempty when the clearest thought is "there are no bad cases". Use .Σ with subset testing when the clearest thought is "this set is contained in that set".