Is the dot operator only left-associative, not just associative?

Questions
1

From the alloy spec:

All binary operators associate to the left, with the exception of implication and sequence, which associate to the right, and of binary temporal connectives which are not associative.

Is the dot operator only left-associative, not both left- and right-associative, which is just associative?

When is (a.b).c != a.(b.c)?

2 
sig A, B, C, D {}

pred whenNotAssociative[ a : A->B, b : B->C, c : C->D ] { 
	a.(b.c) != (a.b).c 
}

run whenNotAssociative
3

This is a cool answer, thanks.

4

@peter.kriens’ command yields no counterexample, which could make think dot join is associative while it’s not.

Here is the explanation by @DanielJackson in his book:

If the arguments are binary relations, it is [associative]. But in general, the expressions (a.b).c and a.(b.c) are not equivalent. Moreover, one may be ill-formed and the other well-formed. Because of the dropped column, the arity of a join is always one less than the sum of the arities of its arguments. If s and t are unary, and r is ternary, for example, the expression t.r will be binary, and s.(t.r) will be unary. The expression s.t, however, would have zero arity, and is thus illegal, so (s.t).r is likewise illegal, and is certainly not equivalent to s.(t.r).

2 Likes
5

David is right. I should have reacted to my suspicion when I realized I need to specify the cardinality of the type. Sadly Alloy has no Any type which could also vary the cardinality.

Sorry.

1 Like
6

Incidentally, I just noticed this sentence of the book is incorrect:

Because of the dropped column, the arity of a join is always one less than the sum of the arities of its arguments.

The arity of a join is two less than the sum of the arities of its arguments, not one, because the join column disappears entirely.

The example immediately following that sentence gets it right though:

If s and t are unary, and r is ternary, for example, the expression t.r will be binary, and s.(t.r) will be unary.

t is unary (1), r is ternary (3), so t.r is is binary (3+1-2 = 2).

2 Likes
7

Indeed you’re right :+1: