Open Source Your Knowledge, Become a Contributor

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

Create Content


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:

Scoping Example
#printASP 1.
let f := (\x -> ~x) in
f (1=1) & f (2=3).


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 (tn,Sn) for some translations we need a newly introduced symbol, which will be denoted by r

Simple Arithmetic

Given a binary arithmetic operation out of +-*/. The translation is done as: (t1t2,S1S2) The absolute value function also works the same way: (|t1|,S1)

Propositional Boolean Functions

Or: Translated as (r,{}) with newly introduced rules:

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

And: Translated as (r,{}) with newly introduced rules:

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

Not: Translated as (r,{}) 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.


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.

Count Aggregate
#printASP 1.
count {1..5} = 5.

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 }
#printASP 1.
let f x := x / 2 in sumBy f {1..3} = 2.


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

Existential Quantification
#printASP 1.
? {1..5} (\x -> x = 5).

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

//Translation of the result

Notice the X0 in the definition of b0, this is required for the scoping of more complex existential bodies.

Open Source Your Knowledge: become a Contributor and help others learn. Create New Content