# Tip: concrete functions

**URL:** <https://alloytools.discourse.group/t/tip-concrete-functions/114>\
**Category:** models\
**Created:** [September 29, 2020, 12:24pm UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114 "2020-09-29T12:24:45Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 29, 2020, 12:24pm UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/1 "2020-09-29T12:24:45Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [September 29, 2020, 12:51pm UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/2 "2020-09-29T12:51:46Z")

</div>

> [@keithb\_b](#):
>
> 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”.

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?

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 29, 2020, 2:59pm UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/3 "2020-09-29T14:59:14Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [September 29, 2020, 3:50pm UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/4 "2020-09-29T15:50:42Z")

</div>

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!

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [September 29, 2020, 4:57pm UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/5 "2020-09-29T16:57:55Z")

</div>

> [@grayswandyr](#):
>
> they don’t force anything, why is why I call them derived or views

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.

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [September 29, 2020, 7:14pm UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/6 "2020-09-29T19:14:29Z")

</div>

> [@keithb\_b](#):
>
> I must not understand what you mean, as this statement by itself appears to be untrue. 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}` .

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`.

> [@keithb\_b](#):
>
> 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.

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).

---

<div class="post-metadata">

**Author:** ![keithb\_b](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/keithb_b/32/7_2.png) [@keithb\_b](https://alloytools.discourse.group/u/keithb_b)\
**Post date:** [October 2, 2020, 9:25am UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/7 "2020-10-02T09:25:06Z")

</div>

OK, thanks for sticking with this.

You say

> [@grayswandyr](#):
>
> these relations are defined out of others

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`

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [October 2, 2020, 10:17am UTC](https://alloytools.discourse.group/t/tip-concrete-functions/114/8 "2020-10-02T10:17:21Z")

</div>

> [@keithb\_b](#):
>
> 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?

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:

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

```

or

```auto
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.