Dot join for navigating backwards

Questions
1

Hello. I’m confused about the following from the Practical Alloy book:

Relations can be navigated forwards, from the source signature to the target signature, but also backwards from the target signature to the source one.

Here’s a model from the book:

abstract sig Object {}

sig File extends Object {}
sig Dir extends Object {
  entries : set Entry
}

sig Entry {
  object : one Object,
  name   : one Name
}

I understand the forward navigation. First, it the dot was chosen to make it readable, and second, It’s turtles tuples all the way down.

For example, entries.e denotes the set of directories that contain entry e: this set can be empty, if e is not contained in any directory, or even have more than one directory, since when declaring a field there are no multiplicity restrictions imposed on the source signature. We can also compose with an arbitrary set on the right-hand side: for example, entries.Entry is the set of all directories that contain some entry. Compositions can also be chained to obtain atoms that are somehow indirectly related. For example, d.entries.object denotes the set of all file system objects that are contained in some entry of directory d.

An example from the Software Abstractions book on how the dot join works is helpful:

Examples. Here are some example of joins of tuples:
{(N0, A0)} . {(A0, D0)} = {(N0, D0)}
{(N0, D0)} . {(N0, D0)} = {}
{(N0, D0)} . {(D1)} = {}
{(N0)} . {(N0, D0)} = {(D0)}
{(N0, D0)} . {(D0)} = {(N0)}
{(B0)} . {(B0, N0, D0)} = {(N0, D0)}

The simplest example in our case is {(D0)} . {{D0, E0}} . {(E0, O0)} = {(O0)}, and this is indeed the set of all file system objects that are contained in some entry of directory d.

Now, I find it confusing how to read backwards navigation.

And again, it is possible to navigate backwards through a chain of compositions. For example, entries.object.d denotes the set of all directories that have some entry that points to directory d.

First, I can’t construct a good example for entries.object.d. Is it {(E0, O0)} . {(O0)} . {(D0)}? Could anyone provide an example that clarifies this in terms of tuples?

Second, how to is it meant to be read without looking into tuples? Is it (entries.object).d or entries.(object.d) here? It’s presented as something natural.

2

Note that members of a signature are relations, of an arity one larger than what they appear in the signature, because they are implicitly extended on the left with the set created by the signature they are “contained” in.

So, for example, entries appears to have type set Entry but its actual type is set Dir -> set Entry due to being enclosed in sig Dir.

Second, how to is it meant to be read without looking into tuples? Is it (entries.object).d or entries.(object.d) here? It’s presented as something natural.

The dot operator is left-associative, so it is the former. You read it left-to-right and perform joins as you go.

With that in mind:

  • entries: set Dir -> set Entry
  • object: set Entry -> one Object
  • d: assumed to be an instance of Dir, i.e. a single directory

We now have:

  1. entries.object: set Dir -> set Object
    • Note: Object’s multiplicity is now set due to how joins work. (I’m pretty sure! But I realise now I’ve never seen any formal treatment of this. I’d be curious reading any, if someone happens to know a reference.)
  2. d is a Dir, which is a subset of Object, so we can join with set Object on the right. That is (entries.object).d: set Dir

To make matters concrete, suppose the following model:

entries = {(D0, E0), (D0, E2), (D1, E1)}
object = {(E0, D0), (E1, D0), (E2, F0)}
d = {(D0)}

entries.object = {(D0, E0), (D0, E2), (D1, E1)} . {(E0, D0), (E1, D0), (E2, F0)}
               = {(D0, D0), (D0, F0), (D1, D0)}

entries.object.d   =
(entries.object).d = {(D0, D0), (D0, F0), (D1, D0)} . {(D0)}
                   = {(D0), (D1)}
1 Like
3

Thank you, this is now clear as day.

Basically, reading forward navigation is, well, straightforward, and when use navigation in any other way, including backwards, we have to remember that it’s all about joins, and we should explicitly look into types.

I think this example deserves to be in the book.

4

The dirty part is that the dot is also overloaded for injecting the first parameter in a pred or fun.

    a.b[c]

Can mean:

     (join c ( join a b))
     (join a (call b(c))) // only fun
     (call b(a,c))
     (join c (join a (call b()))) // only fun

Where call is either fun or pred. Alloy will abort when there are multiple possibilities based on type matching.

1 Like
5

Is there a way to disambiguate this in code?

6

Actually good question.

  • With foreign functions or relations, you can put the module name in front of it: module/a
  • If you want a field from a specific sig, you can do (A<:a) (but this can still clash with a function like fun a : A->A {A->A})

I can’t find a way to force a specific function. I actually found out that it is legal to declare the same function twice …


sig A { bar : A}
fun bar : A->A { A->A }
fun bar : A->A { A->A }
run { some (A<:bar) }

This name is ambiguous due to multiple matches:
fun this/bar
fun this/bar
field this/A <: bar

Not sure if there are more rules, I am in the middle of writing a new parser using ANTLR and decide to include a new AST. It was a bit of a surprise how complex Alloy is.

I might be missing something … I tend to always stay on the safe/simple side in languages which keeps me away from these edges. So my experience is limited.

1 Like