 # Tip: concrete functions

So the event reification pattern [aside, is anyone writing up Alloy/Electrum expertise in one of the defined Pattern forms?] defines a function in a way that I’d not seen before, what in this example I’m calling “product style”.

Given

``````let multiplication_table =
0 -> 0 -> 0
+ 0 -> 1 -> 0
+ 1 -> 0 -> 0
+ 1 -> 1 -> 1
+ 0 -> 2 -> 0
+ 2 -> 0 -> 0
+ 2 -> 1 -> 2
+ 1 -> 2 -> 2
+ 2 -> 2 -> 4
``````

then these

``````fun mul_product_style: Int -> Int -> Int {
multiplication_table
}

fun mul_dereference_style[x, y: Int]: Int{
y::(x::(multiplication_table))
}
``````

behave identically, as shown by

``````run {
all x, y: {i: Int | 0 <= i && i < 3} | {
let p = x fun/mul y | {
mul_product_style[x,y]      = p
mul_product_style[x][y]     = p
x::mul_product_style[y]        = p
y::(x::mul_product_style)          = p
y.(x.mul_product_style)          = p

mul_dereference_style[x,y]  = p
mul_dereference_style[x][y] = p
x::mul_dereference_style[y]    = p
y::(x::mul_dereference_style)      = p
y.(x.mul_dereference_style)      = p
}
}
}
``````

which along the way illustrates all the ways I know of to apply a function.

The crucial difference is that the `mul_product_style` form creates a relation in the instance, which we can see in the evaluator

``````mul_product_style

┌─┬─┬─┐
│0│0│0│
│ ├─┼─┤
│ │1│0│
│ ├─┼─┤
│ │2│0│
├─┼─┼─┤
│1│0│0│
│ ├─┼─┤
│ │1│1│
│ ├─┼─┤
│ │2│2│
├─┼─┼─┤
│2│0│0│
│ ├─┼─┤
│ │1│2│
│ ├─┼─┤
│ │2│4│
└─┴─┴─┘
``````

but `mul_dereference_style` does not, it can only be named in an expression to be evaluated.

Indeed. The name I’ve most seen used is derived relation (or set depending in the arity). You could also call it a view as in databases. Can’t remember if it’s discussed in Daniel’s book?

Derived relations work this way too, but that’s not the intent I see in the use of this fact about functions in the event reification pattern. These:

``````fun _send : Event -> Node {
Send -> { n : Node | send[n] }
}

fun _compute : Event -> Node {
Compute -> { n : Node | compute[n] }
}

fun _skip : Event {
{ e : Skip | skip }
}
``````

from your event reification example aren’t meant to be invoked, or even mentioned other than in this

``````fun events : set Event {
(_send + _compute).Node + _skip
}
``````

so far as I can tell.

So not the usual sense of “a function”. They also don’t seem to me like views onto any prior thing, or a derived anything, they look to me like a way to force a structural relation into the instance de novo.

As a matter of fact:

• they don’t force anything, why is why I call them derived or views, as:
• the possible traces would be exactly the same without these event `fun`s
• at the same time, their value is computed out of the meaningful parts of the model (tuples for which the respecting `pred`s are true in a given state)
• BUT: they can be used (and are actually used) to reason over the model: for instance, if you want to say that `compute` happens in a state, you can write `some _compute` instead of `some n : Node | compute[n]`. For events with larger arity, this is quite neat!

I must not understand what you mean.

Witness my model above, in which the instance still contains a representation of `2 -> 2-> 4` even if the set of `Int`s in the run is restricted to `{i: Int | 0 <= i && i < 2}`.

The definition of a function like `mul_product_style` or `fun _send` doesn’t force anything to happen, or not happen, in the execution of a model, but it plainly does force a relation to exist in the instances even if it is not used by a `run` or `check`. In fact, if I comment out the body of the `run` in my model completely, the relation is still present in the instance, but if comment out the definition of `mul_product_style` as well then the instance is empty. It is in this sense that I say that such functions force relations into existence in an instance.

Hmm in `run { all x, y: {i: Int | 0 <= i && i < 3} | { ... }}` you’re limiting the scope of `x` and `y` but not of their product, which remains `Int`, so `2->2->4` is an acceptable tuple. Unless you add ` for 2 Int` to your `run`.

Sure, I agree that these relations appear in the instances. This is the reason why we used them for the event reification idiom. It’s a very nice aspect of Alloy to have this feature, including styling capabilities.

But what I meant is that these relations are defined out of others and do not add constraints (they do not reduce the set of instances).

OK, thanks for sticking with this.

You say

Which I don’t understand. In the complete model below, out of what other relations is `mul_product_style` built, if as previously claimed a `fun` is just a name for an expression?

``````fun mul_product_style: Int -> Int -> Int {
0 -> 0 -> 0
+ 0 -> 1 -> 0
+ 1 -> 0 -> 0
+ 1 -> 1 -> 1
+ 0 -> 2 -> 0
+ 2 -> 0 -> 0
+ 2 -> 1 -> 2
+ 1 -> 2 -> 2
+ 2 -> 2 -> 4
}

run {
all x, y: {i: Int | 0 <= i && i < 2} | {
let p = x fun/mul y | {
mul_product_style[x,y]      = p
mul_product_style[x][y]     = p
x::mul_product_style[y]        = p
y::(x::mul_product_style)          = p
y.(x.mul_product_style)          = p
}
}
}
``````

Your point about not limiting the scope of the product is interesting. Doing so has a very surprising effect, I find. The below model has an instance containing this value for `mul_product_style`

``````┌──┬──┬──┐
│-2│-2│0 │
│  ├──┼──┤
│  │0 │0 │
│  ├──┼──┤
│  │1 │-2│
├──┼──┼──┤
│0 │-2│0 │
│  ├──┼──┤
│  │0 │0 │
│  ├──┼──┤
│  │1 │0 │
├──┼──┼──┤
│1 │-2│-2│
│  ├──┼──┤
│  │0 │0 │
│  ├──┼──┤
│  │1 │1 │
└──┴──┴──┘
``````

Where do those negative numbers come from? In

``````fun mul_product_style: Int -> Int -> Int {
0 -> 0 -> 0
+ 0 -> 1 -> 0
+ 1 -> 0 -> 0
+ 1 -> 1 -> 1
+ 0 -> 2 -> 0
+ 2 -> 0 -> 0
+ 2 -> 1 -> 2
+ 1 -> 2 -> 2
+ 2 -> 2 -> 4
}

run {
all x, y: {i: Int | 0 <= i && i < 2} | {
let p = x fun/mul y | {
mul_product_style[x,y]      = p
mul_product_style[x][y]     = p
x::mul_product_style[y]        = p
y::(x::mul_product_style)          = p
y.(x.mul_product_style)          = p
}
}
} for 2 Int
``````

the evaluator gives

``````┌──┬──┬─┬─┐⁻¹
│-1│-2│0│1│
└──┴──┴─┴─┘
``````

as the value of `univ`

Out of integers.

In the Alloy language and type system, you can only manipulate relations. An atom is only manipulable as a a singleton set containing one 1-tuple. So `1` is in fact `{(1)}`. And, for a scope of `2 Int`, you have these implicit declarations:

``````abstract sig Int {}
one sig -2 extends Int {}
one sig -1 extends Int {}
one sig 0 extends Int {}
one sig 1 extends Int {}
``````

or

``````enum Int { -2, -1, 0, 1 }
``````

As a convenience, Alloy has a special treatment for integers to ensure that they follow the laws of two-complement integers (e.g. `plus[1,1] = -2` for a scope of `2 Int`) and that these laws rely on machine integers (for efficiency).

I don’t use the tabular notation… The “real” instance is the one you can see when you click the “Txt” button in the Viz.