Back
Close

Functional Modelling System

IngmarDasseville
5,138 views

Translation

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

Representation

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:

a(1).
b(3).
c(4).

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

Booleans

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.
1=1.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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.

Sets

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

Functions

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

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:

{member(s2,X):member(s,X)}.

This can be seen in the following example:

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

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

Functions

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:

1<={lamInter((l0,()),X2,X1):member((s0,()),X1)}<=1:-lamDom((l0,()),X2).

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