Semantics
Virtual paths in
jvvfs are conceptually
a list of
names,
with the empty list representing the root.
A path p0 is an ancestor of
p1 iff
p0 is a prefix of
p1 (that is, the first length p0
elements of p1 are equal to
p0), but
p0 ≠ p1.
Consequently, a path p0 is the parent of
p1 iff
p0 is an ancestor of
p1 and ∃n. app p0 n = p1
(where app is the standard list append function).
Iff p1 is an ancestor of
p0, or p0 = p1,
the subtraction of
p1 from
p0 is defined as the removal of the
first length p1 elements of
p0.
It naturally follows that it is possible to obtain a list
of all ancestors of a path p
by successively concatenating the elements of
p to the root, minus the last element.