Associativity and meaning of multi-arity signature declarations

Questions
1

We have been studying the associativity of the → in multi-arity relations and also the meaning of multiplicities in these declarations.

  • Can an Alloy developer please confirm that the associativity of → is RIGHT?, i.e.
    sig A { f: B → one C → D }
    means
    sig A { f: B → one (C → D) }
    rather than
    sig A { f: (B → one C) → D }
    Associativity is only relevant with multiplicities so this question does not apply to regular arrow expressions, which cannot include multiplicities.

    We note that right associativity for → contradicts the Alloy cheat sheet at https://esb-dev.github.io/mat/alloy-cheatsheet.pdf, which says all binary operators besides implication associate left. Although, the point is not addressed in the declarations section of the cheat sheet.

  1. Wrt the meaning of the multiplicities in a field declaration, can an Alloy developer please confirm that our understanding of the three cases below is correct?

    a) in
    sig A {
    f: B → one (C → D)
    }
    the quantification is over (c,d) pairs in f, and thus means:
    there is a exactly one distinct (c,d) pair for any (a,b) pair
    all a:A, b:B | one (b.(a.f))

    b) in
    sig A {
    f: (B → one C) → D
    }
    the quantification is over the c element alone, so it means:
    there is exactly one c for every a,b,d tuple in f
    all a: A, b:B, d:D | one (b.(a.f)).d

    c) in
    sig A {
    f: B one → (C → D)
    }
    the quantification is over the b element alone, which means for every a,c,d tuple there is one B
    all a:A, c:C, d:D | one ((a.f).d).c

  2. Could someone explain why a multiplicity is not allowed in the Alloy syntax before an arrow? As in:
    sig A {
    f: one B → C
    }
    It seems possible to give this a meaning.

Many thanks!