# Functional Modelling System

### Scoping

Up till now, all translated expressions were not really nested into each other.

However when handling more complex expressions another difficulty arises: how to translate expressions with free variables. Take for instance the (anonymous) function `\x -> ~x`

, suppose this is translated to `l0`

. This function contains the expression `~x`

. We reify the output of `l0`

with the term `b0`

using the following rule:

```
lamInter(l0, X, b0) :- lamDom(l0,X).
```

and state that `b0`

must be the negation of `l0`

's input with a second rule:

```
bool(b0,()) :- lamDom(l0,X), not bool(X,()).
```

But now the interpretation of `b0`

does not depend on the input `X`

of `l0`

. The solution is to keep track of the free variable `X`

of `b0`

like this:

```
bool((b0,(X)),()) :- lamDom(l0,X), not bool(X,()).
lamInter(l0, X, (b0,(X))) :- lamDom(l0,X).
```

In the next example you can see this in action:

### Builtins

We encountered most of the builtins along the way, but some of those are a bit more advanced so this section serves as an overview for the builtins. The n'th argument of the builtin is represented as $\$(t\_n,\; S\_n)\$$ for some translations we need a newly introduced symbol, which will be denoted by $\$r\$$

##### Simple Arithmetic

Given a binary arithmetic operation $\$\backslash odot\$$ out of +-*/. The translation is done as: $\$(t\_1\; \backslash odot\; t\_2,\; S\_1\; \backslash cup\; S\_2)\$$ The absolute value function also works the same way: $\$(|t\_1|,\; S\_1)\$$

##### Propositional Boolean Functions

**Or:**
Translated as $\$(r,\backslash \{\backslash \})\$$ with newly introduced rules:

```
bool(r,()) :- bool(t1,()), S1
bool(r,()) :- bool(t2,()), S2
```

**And:**
Translated as $\$(r,\backslash \{\backslash \})\$$ with newly introduced rules:

```
bool(r,()) :- bool(t1,()), bool(t2,()), S1, S2
```

**Not:**
Translated as $\$(r,\backslash \{\backslash \})\$$ with newly introduced rules:

```
bool(r,()) :- not bool(t1,()), S1
```

**Others:**
Other functions are just translated by converting the operator to a combination of the above operators.

#### Aggregates

These functions operate on sets.

**Count:**
The count function directly corresponds to the count aggregate in ASP.
It is translated as

`(t = X, S = {#count{Y : member(t_1,Y)} = X)}`

The declaration of `X`

as an intermediate variable is necessary as ASP only supports (in)equalities between aggregates and other terms and other operations onto the term could break this invariant.

**Min/Max/Sum:**
These three aggregates work completely analog to count, the only thing that changes is the name of the aggregate.

**SumBy:**
SumBy is the only aggregate which works slightly differently, as we now also have a function we have to apply on each element of the set. The only thing that really changes is the aggregate expression. Which now quantifies two variables instead of one: the element of the set (`X2`

) and the result of applying the function to this element (`X3`

). So the result of `sumBy`

applied on a function `l0`

and set `s0`

is represented by

```
t = X4 and S = { #sum{X3,X2:member((s0,()),X2),lamInter((l0,()),X2,X3)}=X4 }
```

#### Quantifiers

**Exists:**
The existential quantification is a bit more subtle than the aggregates. Consider the following theory:

The resulting Boolean can be defined as: There is a member `y`

of the set `{1..5}`

such that the evaluation of `x=5`

under `x=y`

is true. And this exactly what this rule defines:

```
//Translation of x=5
bool((b0,(X0)),()):-X0=5,member((s0,()),X0).
//Translation of the result
bool((b1,()),()):-bool((b0,(X0)),()),member((s0,()),X0).
```

Notice the `X0`

in the definition of `b0`

, this is required for the scoping of more complex existential bodies.