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
Previous: Translation Next: Syntax


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.
s := {1..5}.
? s (\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