Functional Modelling System
Scoping
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:
Builtins
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 for some translations we need a newly introduced symbol, which will be denoted by
Simple Arithmetic
Given a binary arithmetic operation out of +-*/. The translation is done as: The absolute value function also works the same way:
Propositional Boolean Functions
Or: Translated as with newly introduced rules:
bool(r,()) :- bool(t1,()), S1
bool(r,()) :- bool(t2,()), S2
And: Translated as with newly introduced rules:
bool(r,()) :- bool(t1,()), bool(t2,()), S1, S2
Not: Translated as 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.
Aggregates
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.
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 }
Quantifiers
Exists: The existential quantification is a bit more subtle than the aggregates. Consider the following theory:
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
bool((b0,(X0)),()):-X0=5,member((s0,()),X0).
//Translation of the result
bool((b1,()),()):-bool((b0,(X0)),()),member((s0,()),X0).
Notice the X0
in the definition of b0
, this is required for the scoping of more complex existential bodies.