Back
Close

Functional Modelling System

IngmarDasseville
5,124 views
Previous: Translation Next: Syntax

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:

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

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 (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.

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.

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

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

Quantifiers

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).
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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.

Create your playground on Tech.io
This playground was created on Tech.io, our hands-on, knowledge-sharing platform for developers.
Go to tech.io
codingame x discord
Join the CodinGame community on Discord to chat about puzzle contributions, challenges, streams, blog articles - all that good stuff!
JOIN US ON DISCORD
Online Participants