Functional Modelling System


Open Source Your Knowledge, Become a Contributor

Technology knowledge has to be shared and made accessible for free. Join the movement.

Create Content


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


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:


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 (t1,S1) and (t2,S2), the sum of these two can be represented as (t1+t2,S1S2).


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.

Representation of Booleans
#printASP 1.

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.


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={}.

Representation of Sets
#printASP 1.
#noOpt 1.
(\x -> true) {1,2,3}.


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

Representation of Functions
#printASP 1.
//Setting the inliner directive to 0 prevents the translator from inlining f (which would simplify the full expression to "true")
#inline 0.
let f x := true in f 4.

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:


This can be seen in the following example:

Representation of Uninterpreted Sets
#printASP 1.
s :: subset of {1..5}.
sum s = 4.

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:

Representation of Uninterpreted Elements
#printASP 1.
s :: element of {1..5}.
s = 4.


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:


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.

Representation of Uninterpreted Functions
#printASP 1.
f/1 :: function to {1..5}.
f "a" = f "b".
Open Source Your Knowledge: become a Contributor and help others learn. Create New Content