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$$ and a set of ASP-bodies $$ 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$$ and $$ S=\{\}$$
• $$ t=X$$ and $$ S=\{c(X)\}$$
• $$ t=X+Y$$ and $$ S=\{a(X),b(Y)\}$$

This already shows how the translation of a general sum can be done: Given two translated terms $$ (t_1,S_1)$$ and $$ (t_2,S_2)$$, the sum of these two can be represented as $$ (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$$ is considered to be true iff $$ 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,())$$ and $$ 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,())$$ and $$ 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,())$$ and $$ 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$$ and $$ 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.