# Functional Modelling System

## Translation

In this chapter we will investigate the relation between the language and the underlying ASP translation.

### Representation

In general, every term in the lambda language can be represented in ASP as a combination of an ASP-term t$t$ and a set of ASP-bodies S$S$. So given that these facts are already true:

```
a(1).
b(3).
c(4).
```

The following are all valid representations for the number 4:

- t=4$t=4$ and S={}$S=\{\}$
- t=X$t=X$ and S={c(X)}$S=\{c(X)\}$
- t=X+Y$t=X+Y$ and S={a(X),b(Y)}$S=\{a(X),b(Y)\}$

This already shows how the translation of a general sum can be done: Given two translated terms (t1,S1)$({t}_{1},{S}_{1})$ and (t2,S2)$({t}_{2},{S}_{2})$, the sum of these two can be represented as (t1+t2,S1∪S2)$({t}_{1}+{t}_{2},{S}_{1}\cup {S}_{2})$.

#### Booleans

Integers are builtin as terms in ASP but Boolean values are not. To work around this, we introduced a predicate `bool`

which takes two arguments. Then, a Boolean term t$t$ is considered to be true iff bool(t,())$bool(t,())$ holds.

This can be seen by running the following example.

**Note:** You can see the translation of any theory by using the directive `#printASP 1`

at the top of a file.

The translation of the term `1=1`

was represented by t=(b0,())$t=(b0,())$ and S={}$S=\{\}$, leading to the rule `bool((b0,()),()):- 1=1`

.

#### Sets

Just like Booleans, sets are not natively supported in ASP as terms. A system analoguous to Booleans is used to represent them. A set can be represented by any term `t`

. Then, a term `t2`

is a member of set `t`

iff `member(t,t2)`

is true.

In the next example the set `{1,2,3}`

is represented by t=(s0,())$t=(s0,())$ and S={}$S=\{\}$.

#### Functions

Functions are the most complex data type because, in general, they have an infinite input domain, but they still need to fit into finite ASP structures. For this we need to introduce 2 predicates `lamInter`

which represents the interpretation of the function and `lamDom`

which represents the relevant input domain of the function.

A function can be represented by any term `t`

. Then, `lamDom(t,t2)`

is true for any relevant argument for the function `t2`

and `lamInter(t,t2,t3)`

is true for exactly one image `t3`

of `t2`

under `t`

.

In the next example the function `f`

is represented by t=(l0,())$t=(l0,())$ and S={}$S=\{\}$. The relevant domain of `f`

consists of the singleton `{4}`

and the interpretation of the function applied to anything is `(b0,())`

which represents `true`

### Declarations of uninterpreted symbols

Uninterpreted symbols are defined using choice rules, allowing for different interpretations in different models.

#### Subsets and elements

Subsets are the most straightforward ones to translate. Given a set `s`

we can declare `s2`

to be a subset of `s`

by the choice rule:

```
{member(s2,X):member(s,X)}.
```

This can be seen in the following example:

Cardinality constraints can be put upon the choice rule to make sure s2 contains only 1 element:

```
{member(s2,X):member(s,X)} == 1.
```

A constant `c`

declared as an element of `s`

can now be represented as t=X$t=X$ and S=member(s2,X)$S=member(s2,X)$. This can be seen in the following example:

#### Functions

In the next example the function `f`

is represented by `(l0,())`

. The `lamDom`

predicate works as always and contains `"a"`

and `"b"`

. The codomain of the function is 1..5 represented by the set `(s0,())`

. So the only special rule is the choice rule:

```
1<={lamInter((l0,()),X2,X1):member((s0,()),X1)}<=1:-lamDom((l0,()),X2).
```

This rule specifies that for each element `X2`

in the domain of `f`

exactly one member of `(s0,())`

needs to be chosen as interpretation for the function.