=Paper=
{{Paper
|id=Vol-1645/paper_7
|storemode=property
|title=Labelled Variables in Logic Programming: Foundations
|pdfUrl=https://ceur-ws.org/Vol-1645/paper_7.pdf
|volume=Vol-1645
|authors=Roberta Calegari,Enrico Denti,Agostino Dovier,Andrea Omicini
|dblpUrl=https://dblp.org/rec/conf/cilc/CalegariDDO16
}}
==Labelled Variables in Logic Programming: Foundations==
https://ceur-ws.org/Vol-1645/paper_7.pdf
Labelled Variables in Logic Programming:
Foundations
Roberta Calegari1 , Enrico Denti1 , Agostino Dovier2 , and Andrea Omicini1
1
Dipartimento di Informatica, Scienza e Ingegneria (DISI)
Alma Mater Studiorum–Università di Bologna, Italy
{roberta.calegari, enrico.denti, andrea.omicini}@unibo.it
2
Dipartimento di Scienze Matematiche, Informatiche e Fisiche
Università degli Studi di Udine, Italy
agostino.dovier@uniud.it
Abstract. We define a new notion of truth for logic programs ex-
tended with labelled variables, interpreted in non-Herbrand domains.
There, usual terms maintain their Herbrand interpretations, whereas
diverse domain-specific computational models depending on the local
situation of the computing device can be expressed via suitably-tailored
labelled models. After some introductory examples, we define the theo-
retical model for labelled variables in logic programming (LVLP). Then,
we present both the fixpoint and the operational semantics, and discuss
their correctness and completeness, as well as their equivalence.
1 Introduction
To face the challenges of today’s pervasive systems – inherently complex, dis-
tributed, situated, and intelligent [14] – suitable models and technologies are re-
quired to effectively support distributed situated intelligence. Once it is extended
to capture the many different domains where situated intelligence is required,
logic programming (LP) has the potential to work at the core of such models and
technologies based on its declarative representation and inferential capabilities.
Along this line, in this paper we present a logic programming extension based
on labelled variables [8, 10], the Labelled Variables model in Logic Programming
(LVLP). There, diverse computational models can be tailored to the local needs
of situated components by means of suitable labelled variables systems, and
work together against the common LP background. In fact, whereas logic-based
approaches are natural candidates for intelligent systems, a pure LP approach
seems not to fit well the needs of situated systems. Instead, a hybrid approach
makes it possible in principle to exploit LP for what it is most suited for – sym-
bolic computation –, while possibly delegating other aspects – such as situated
computations – to other languages, or to other levels of computation.
Most other works in this area – such as [1, 2, 9, 16, 17] – primarily focus onto
specific scenarios and sorts of systems—e.g. modal logic, deductive systems, fuzzy
systems, etc. Instead, our model aims at providing a general-purpose framework
and mechanism which, while seamlessly rooted in the LP landscape, could fit
several relevant context-specific systems.
Calegari, Denti, Dovier & Omicini
2 Context, Motivation & Examples
In nowadays complex and pervasive scenario, where software engineering, pro-
gramming languages, and distributed artificial intelligence meet, logic-based lan-
guages have the potential to play a prominent role both as intelligence providers
and technology integrators [15]. Typical LP features – such as programs as logic
theories, computation as deduction, and programming with relations and infer-
ence – make logic languages a natural choice for building intelligent components.
Nevertheless, diverse computational models tailored to the local needs of situated
systems can be required in order to capture different paradigms and languages
of the distributed environment.
Along this line, we introduce the notion of label to tag logic variables, and
the associated computational model for their elaboration, which proceeds along
with the resolution procedure without being strictly subject to the standard LP
rules. Generally speaking, labels provide a customisable computational model,
which can be charged of the domain-specific – and possibly not declarative –
part of the computation, and bound to the standard LP computation.
Before formally defining (Section 3) the Labelled Variables model in Logic
Programming (LVLP), we informally discuss some examples to give the flavour
of our approach. For instance, in a WordNet-like scenario [18], representing a
network of semantically-related words, labels (unlike standard LP) offer a way
to split the representation onto two different levels, each one with its own compu-
tational model: logic variables stand for individual objects in the domain, while
labels can be exploited to represent the network of related words.
Following our prototype syntax, X^label is a labelled variable denoting a
logic variable X labelled with label —where label is a term in the set of admis-
sible labels defined by the user. In a LVLP clause, the list of the labelled variables
precedes the remaining part of the body. Given the following LVLP program:
wordnet_fact ([ ‘ dog ’ ,‘ domestic dog ’ ,‘ canis ’ ,‘ pet ’ ,‘ mammal ’ ,‘ vertebrate ’ ]).
wordnet_fact ([ ‘ cat ’ , ‘ domestic cat ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’ ]).
wordnet_fact ([ ‘ fish ’ , ‘ aquatic vertebrates ’ , ‘ vertebrate ’ ]).
wordnet_fact ([ ‘ frog ’ , ‘ toad ’ , ‘ anauran ’ , ‘ batrachian ’ ]).
animal ( X ) : - X ^[ ‘ pet ’] , X = ‘ minnie ’.
animal ( X ) : - X ^[ ‘ fish ’] , X = ‘ nemo ’.
animal ( X ) : - X ^[ ‘ cat ’] , X = ‘ vmolly ’.
animal ( X ) : - X ^[ ‘ dog ’] , X = ‘ frida ’.
animal ( X ) : - X ^[ ‘ frog ’] , X = ‘ cra ’.
the following query, looking for a pet animal, generates four solutions:
? - X ^[ ‘ pet ’] , animal ( X ).
yes . X / ‘ minnie ’
[ X ^[ ‘ dog ’ , ‘ domestic dog ’ , ‘ canis ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’ ]] ;
yes . X / ‘ minnie ’
[ X ^[ ‘ cat ’ , ‘ domestic cat ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’ ]] ;
yes . X / ‘ molly ’
[ X ^[ ‘ cat ’ , ‘ domestic cat ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’ ]] ;
yes . X / ‘ frida ’
[ X ^[ ‘ dog ’ , ‘ domestic dog ’ , ‘ canis ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’ ]]
Labelled Variables in Logic Programming: Foundations
Looking instead for a less specific vertebrate produces five solutions:
? - X ^[ vertebrate ] , animal ( X ).
yes . X = ‘ minnie ’
X ^[ ‘ dog ’ , ‘ domestic dog ’ , ‘ canis ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’] ;
yes . X = ‘ minnie ’
X ^[ ‘ cat ’ , ‘ domestic cat ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’] ;
yes . X = ‘ molly ’
X ^[ ‘ cat ’ , ‘ domestic cat ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’] ;
yes . X = ‘ frida ’
X ^[ ‘ dog ’ , ‘ domestic dog ’ , ‘ canis ’ , ‘ pet ’ , ‘ mammal ’ , ‘ vertebrate ’] ;
yes . X = ‘ nemo ’
X ^[ ‘ fish ’ ,‘ aquatic vertebrates ’ , ‘ vertebrate ’]
A relevant aspect of LVLP is that labels are not subject to the single-assignment
assumption: each time two labelled variables unify, their labels are processed and
combined according to a user-defined function that embeds the desired computa-
tional model, and the resulting label is associated to the unified variable. Thus,
the LP model per se is left untouched, whereas diverse computational models
can be defined next to it, possibly influencing the result of a logic computation
by restricting the set of admissible solutions according to each specific domain.
For instance, let us consider the case in which the knowledge base consists
of a collection of ingredients, each featuring properties such as calories count,
amount of proteins, fat, etc. There, labels could be used to describe the weight,
calories and category of the food, as in the program below:
meat ( M ) : - M ^[100 g , 156 cal , [ a l t e rn a t i v e M e a t s ]] , M =[ ‘ tofu meatballs ’ ].
meat ( M ) : - M ^[100 g , 145 cal , [ curedMeats ]] , M =[ ‘ Parma ham ’ ].
meat ( M ) : - M ^[100 g , 210 cal , [ curedMeats ]] , M =[ ‘ ham ’ ].
meat ( M ) : - M ^[200 g , 220 cal , [ whiteMeats ]] , M =[ ‘ chicken ’ ].
vegetable ( V ) : - V ^[100 g , 35 cal , [ vegetables ]] , V =[ ‘ carrots ’ ].
vegetable ( V ) : - V ^[ 50 g , 10 cal , [ vegetables ]] , V =[ ‘ salad ’ ].
bread ( B ) : - B ^[100 g , 265 cal , [ whiteBread ]] , B =[ ‘ bread with poolish ’ ].
bread ( B ) : - B ^[100 g , 240 cal , [ integralBread ]] , B =[ ‘ whole grain bread ’ ].
recipe ( R ) : - R ^, meat ( Meat ) , vegetable ( Vegetable ) , R =[ Meat , Vegetable ].
recipe ( R ) : - R ^, Meat ^[ any , any , [ curedMeats ]] , bread ( Bread ) , meat ( Meat ) ,
vegetable ( Vegetable ) , R =[ Bread , Meat , Vegetable ].
Labels (with representing the any label) make it possible, for instance, to ask
for a meal with an upper bound of calories, with a given tolerance. Assuming,
e.g., that the label-combining function accounts for a 10% tolerance, a possible
query asking for a recipe with 200(±20) calories could be the following:
? - R ^[ any , 200 cal , any ] , recipe ( R ).
yes . R / [ ‘ tofu meatballs ’ , ‘ carrots ’]
R ^[200 g , 191 cal , [ alternativeMeats , vegetables ]] ;
yes . R / [ ‘ tofu meatballs ’ , ‘ salad ’]
R ^[200 g , 166 cal , [ alternativeMeats , vegetables ]] ;
yes . R / [ ‘ Parma ham ’ , ‘ carrots ’]
R ^[200 g , 180 cal , [ curedMeats , vegetables ]] ;
yes . R / [ ‘ ham ’ , ‘ salad ’]
R ^[150 g , 220 cal , [ curedMeats , vegetables ]]
Calegari, Denti, Dovier & Omicini
Comparing the labels of R in the query and in the answers should make it clear
how avoiding single assignment in the labels (not in the logic variable) makes
the language more expressive, without harming the logic computation.
Multiple matching criteria could also be applied simultaneously—for in-
stance, combining calories with a specific food category:
? - R ^[ any , 180 cal , [ a l t e r n a t i v e M e a t s ]] , recipe ( R ).
yes . R / [ ‘ tofu meatballs ’ ,‘ carrots ’]
R ^[200 g , 191 cal , [ alternativeMeats , vegetables ]] ;
yes . R / [ ‘ tofu meatballs ’ ,‘ salad ’]
R ^[150 g , 166 cal , [ alternativeMeats , vegetables ]]
All “standard” domains for logic languages (like the CLP ones [4]) are also
supported. For instance, labels could be used to represent the integer interval
over which the logic variable values span: accordingly, the label syntax could take
the form X^[min,max ], and a simple interval program could look as follows:
interval ( X ): - X ^[ -1 ,4].
interval ( X ): - X ^[6 ,10].
The unification of two variables labelled with an interval would then result in a
variable labelled with the intersection of the intervals. Accordingly, the following
simple query generates two solutions:
? - X ^[2 ,7] , interval ( X ).
yes .
X ^[2 ,4] ;
yes .
X ^[6 ,7]
In addition, the expressiveness of LVLP makes it possible to easily move from
the domain of integer intervals to more complex domains, like for instance the
domain of integers with a neighbourhood, as in the following program:
neighbourhood ( X ): - X ^[ -1 ,4] , X =3.
neighbourhood ( X ): - X ^[6 ,10] , X =8.
There, constant values unify with labelled variables if they belong to the interval
in the label. Accordingly, the following query would result in just one solution:
? - X ^[2 ,7] , neighbourhood ( X ).
yes . X / 3
X ^[2 ,4]
given that the second clause would set X out of the interval in the query.
3 The Labelled Variables Model in Logic Programming
3.1 The model
Let C be the set of constants, with c1 , c2 ∈ C being two generic constants.
Let V be the set of variables, with v1 , v2 ∈ V being two generic variables. Let
F ∈ H be the set of function symbols, with f1 , f2 ∈ F being two generic
Labelled Variables in Logic Programming: Foundations
function symbols. f ∈ F is assigned to an arity ar (f ) > 0 that states the
number of arguments. Let T ⊆ H be the set of terms, with t1 , t2 ∈ T being
two generic terms. Terms can be either simple (constant, variable) or compound
(when containing a f ∈ F, ar (f ) > 0). Let H be the Herbrand universe and
HB be the Herbrand base.
A Labelled Variables Model in Logic Programming is defined as follows.
– A set B = {β1 , . . . , βn } of basic labels that are the basic entities of the
domain of labels.3
– A set L ⊆ ℘(B) of labels, where each ` ∈ L is a subset of B, namely a set
of basic labels (e.g., ` = {β1 , β3 , β6 }). A “singleton” label {β} where β ∈ B
will be identified simply by β in the following for the sake of simplicity.
– A set of variables V , where v ∈ V is the generic variable.
– A labelling which is a set of pairs hvi , `i i, associating the label `i to the
variable vi . A “singleton” labelling {hv, `i} – a labelled variable – will be
identified simply by hv, `i in the following for the sake of simplicity.
– A (label-)combining function fL , synthesising a new label from two given
ones
fL : L × L −→ L
We require that fL be associative, commutative, and idempotent (briefly,
ACI), namely that fL (`1 , fL (`2 , `3 )) = fL (fL (`1 , `2 ), `3 ), fL (`1 , `2 ) =
fL (`2 , `1 ), fL (`, `) = `. As discussed later, in some cases (e.g., incompatibil-
ity), the output of fL can be the empty set ∅ which is a signal for “wrong”.
3.2 Programs, clauses, unification
In a labelled variables logic program a rule is represented as
Head ← Labellings, Body.
where Head is an atomic formula, Labellings is the list of Variable/Label asso-
ciations in the clause and Body is a list of atomic formulas. This can be read
declaratively as Head if Body given Labellings.
The unification of two labelled variables is represented by the extended tuple
(true/false, θ, `), where true/false represents the existence of an answer, θ rep-
resents the most general substitution, and ` represents the new label associated
to the unified variables defined by the (label-)combining function fL .
More generally, considering all the variables of the goal, the solution is repre-
sented by the extended tuple (true/false, Θ, A), where true/false represents the
existence of an answer, Θ represents the most general substitutions for all such
variables, and A represents the corresponding label-variable associations.
3
In this paper we require that B is finite and it is not a real restriction for the
applications we discuss. An infinite set of basic labels can be considered anyway, as
soon as we can guarantee a sort of solution compactness of the extended unification
algorithms involved.
constant c2 variable v2 labelled variable hv2 , `2 i compound term s2
constant if c1 = c2 true, {v2 /c1 } if fC (c1 , `2 ) = true false
c1 then true then true, {v1 /c2 }, `1
else false else false
variable true, {v1 /c2 } true, {v1 /v2 } true, {v1 /v2 }, `2 if v1 does not occur in s2
v1 then true, {v1 /s2 }
else false
labelled variable if fC (c2 , `1 ) = true true, {v1 /v2 }, `1 if fL (`1 , `2 ) 6= ∅ if v1 does not occur in s2 and
hv1 , `1 i then true, {v1 /c2 }, `1 then true, {v1 /v2 }, fL (`1 , `2 ) fL (`1 , fL (`2 , ..., fL (`n−1 , `n )...)) 6= ∅
else false else false where `2 , ...`n are labels
of variables in s2
Calegari, Denti, Dovier & Omicini
then true, {v1 /s2 },
fL (`1 , fL (`2 , ..., fL (`n−1 , `n )...))
else false
compound term false if v2 does not occur in s1 if v2 does not occur in s1 and if s1 and s2
s1 then true, {v2 /s1 } fL (`1 , fL (`2 , ..., fL (`n−1 , `n )...)) 6= ∅ have same functor and arity
else false where `2 , ...`n are labels and arguments
of variables in s1 (recursively) unify
then true, {v2 /s1 }, then true
fL (`1 , fL (`2 , ..., fL (`n−1 , `n )...)) else false
else false
Table 1. Unification rules in LVLP
Labelled Variables in Logic Programming: Foundations
3.3 Compatibility
The tuple (true/false, Θ, A) represents the solution of the labelled variables
program. The implicit assumption is that the LP computation, whose answer is
given by Θ, and of the label computation, whose answer is given by A, can be
read independently from each other from the domain expert’s viewpoint.
This is as to say that, in principle, any computed label-variable association
is “acceptable” in the domain—for instance, if LP computes over numbers and
labels over colors, each number/color association might be equally valid.
For some application scenarios, however, this might not necessarily be the
case: if the LP and label computations somehow capture different views over
the same domain (or two interconnected domains), some label-variable associ-
ation could actually be unacceptable from the domain expert’s viewpoint—for
instance, in the above example even numbers could not be red, or alike.
In order to formalise such a notion of acceptability, let us introduce the
compatibility function fC as:
fC : H × L −→ {true, false}
In particular, given a a ground term t ∈ H and label ` ∈ L :
true there exists at least an element of the domain which
the interpretations of t and ` both refer to the same
fC (t, `) = entity
false otherwise
Example 1 discusses an application scenario where variables are labelled with
their admissible numeric interval, formalising the fL and fC functions accord-
ingly.
Example 1. Let us suppose that the LP variables in a certain applica-
tion scenario span over some integer domains and that they are labelled
with their admissible numeric interval. In this case, the combining func-
tion fL , which embeds the scenario-specific label semantics, is supposed
to intersects intervals: accordingly, fL is defined so that, given two labels
`1 = {β11 , . . . , β1n } and `2 = {β21 , . . . , β2m }, the resulting label `3 is the
intersection of `1 and `2 , as:
`3 = fL (`1 , `2 ) = fL ({β11 , . . . β1n }, {β21 , . . . β2m }) =
{(β11 ∩ β21 ), · · · , (β11 ∩ β2m ), . . . , (β1n ∩ β21 ), · · · , (β1n ∩ β2m )}
In such a scenario, the LP computation aims to compute numeric values,
while the label computation aims to compute admissible numeric intervals
for the LP variables.
In principle, the solution tuple (true/false, Θ, A) could describe situ-
ations such as (true, X = 3, h3, [4, 5]i), since the LP computation and the
label computation proceed without interfering with each other. However, if
Calegari, Denti, Dovier & Omicini
numeric intervals are interpreted as the boundaries for acceptable values of
LP variables, such label-variable associations could appear to be inconsis-
tent to the domain expert’s eyes. So, a reasonable behaviour for the LVLP
system should allow the domain expert to embed his/her knowledge, cap-
turing such incompatibility so that the system can reject this solution.
This is what the compatibility function fC is for: its purpose is to check
whether the ground term t ∈ H is compatible with the interval represented
by label ` = [A..B], ` ∈ L. It could be defined so as to return false for
solutions where the computed LP values do not belong to the numeric
interval computed by the corresponding label computation, thus capturing
the connection among the two universes.
Summing up, the result of a labelled variables program can be written as:
(true/false ∧ fC (Θ, A), Θ, A)
meaning that the truth value potentially computed by the LP computation can
be restricted – i.e., forced to false – by the fC (Θ, A). In turn, this is a convenient
shortcut for the conjunction of all fC (t, `) ∀(t, `) couples, where ` and t are,
respectively, such that the label-variable association hv, `i ∈ A and the substitu-
tion v/t ∈ Θ. Of course, in case of independent domains, fC (t, `) is true for any
t and any `.
Table 1 reports the unification rules for two generic terms: to lighten the no-
tation, undefined elements in the tuple are omitted—i.e., labels or substitutions
that have no sense in a particular situation.
4 Semantics
Labels domains are expected to support tests and operations on labels, in order
to guarantee the basic theoretical results of logic programming, such as the
equivalence of denotational and operational semantics.
In the following, in Subsection 4.1 we define the denotational (fixpoint) se-
mantics in the context of labels domain (under reasonable requests for fL ), while
in Subsection 4.2 we discuss the operational semantics of the model describing
an abstract state machine.
4.1 Fixpoint Semantics
Let us call X = (H , L) a labelled variable logic programming domain and let us
define the notion of X -interpretation I as a set of pairs of the form
p(t1 , . . . , tn ), [`1 , . . . , `n ]
where p(t1 , . . . , tn ) is a ground atom and `1 , . . . , `n are labels s.t. for i = 1, . . . , n
the term ti is compatible with the label `i , i.e. fC (ti , `i ) = true. Truthness
of fC is based on the LVLP domain X . With a slight abuse of notation, we
Labelled Variables in Logic Programming: Foundations
Vn
write X |= [ht1 , `1 i, . . . , htn , `n i] iff i=1 fC (ti , `i ) = true.
VnWe also write X |=
(p(t1 , . . . , tn ), [`1 , . . . , `n ]) if p is a predicate symbol and i=1 fC (ti , `i ) = true.
We denote as Λ the part of clause body that stores labelling associations.
Without loss of generality we assume that there is exactly one label association
for each variable in the head. We define the function feL that in a sense extends
fL and takes as argument a rule
r = h ← Λ, b1 , . . . , bn
and n + 1 lists of labels. The rule r is used here to identify multiple occur-
rences of the variables. Let us assume the variables in h are x1 , . . . , xm , and
consider one of them, say xi . If xi occurs in h (and hence in Λ) and in (some of)
b1 , . . . , bn then the corresponding labels `, `1,i , . . . , `n,i for xi are retrieved from
Λ (if xi does not occur in bj simply we do not consider such contribution). Then
`0i = fL (`, fL (`1,i , . . . , fL (`n−1,i , `n,i ) . . . )) is computed and the pair hxi , `0 i is
returned. This is done for all variables x1 , . . . , xm occurring in the head h and
the list [`01 , . . . , `0m ] is returned.
The denotational semantics we are presenting is based on the one-step con-
sequence functions T P defined as:
T P (I) = h p(e
t), `e i :
r = p(ex) ← Λxe | b1 , . . . , bn (1)
where r is a fresh renaming of a rule of P,
v is a valuation on H such that v(e x) = e
t, (2)
Vn
i=1 ∃ ei s.t. hv(bi ), `ei i ∈ I,
` (3)
Vn
X |= Λet ∧ i=1 fC v(bi ), `i , e (4)
` = fL r, Λet , `1 , · · · , `n
e e e e (5)
where Λet = v(Λxe) = [ht1 , `1 i, . . . , htn , `m i] if Λxe = [hx1 , `1 i, . . . , hxm , `m i]. It is
Vn
worth noting that the condition i=1 fC v(bi ), `ei (line 4) is always satisfied
when TP is used “bottom-up” starting from I = ∅.
In the following some examples are discussed. Note that, in the LVLP the
equality operator is represented by =/2 and its behaviour is summarised by
Table 1 (unification rules). One label association is possibly null in that might
be the any label, defined as the neutral element of fL , henceforth represented
as in the following. As a consequence, any standard (i.e. non labelled) LP
variable is interpreted as labelled with . For such reasons, the =/2 in LVLP can
be defined as:
X = Y : −[< X, >, < Y, >], X =LP Y
where =LP is the standard =/2 LP operator.
Calegari, Denti, Dovier & Omicini
Example 2. Now let us consider the labelled variables program P:
r (0). r (1). r (2). r (3). r (4).
r (5). r (6). r (7). r (8). r (9).
q (Y , Z ) : - Y ^[2 ,4] , Z ^[3 ,8] , Y =Z , r ( Y ) , r ( Z ).
p (X ,Y , Z ) : - X ^[0 ,3] , Y ^, Z ^, X =Y , q (Y , Z ).
Let us consider the interpretation I0 = ∅. Then:
I1 = T P (I0 ) = hr(0), []i, . . . , hr(9)[]i
Let us apply TP to I1 :
I2 = T P (I1 ) = I1 ∪ hq(3, 3), [[3, 4], [3, 4]]i, hq(4, 4), [[3, 4], [3, 4]]i
and now TP to I2 :
I3 = T P (I2 ) = I2 ∪ hp(3, 3, 3), [[3], [3], [3]]i
which is also the least fixpoint of TP .
The above example shows the similarities between labelled logic programming
on a domain X (briefly, LVLP(X )) and CLP (X ). It would be sufficient, e.g., to
replace [hY, [2, 4]i, hZ, [3, 8]i] with Y in 2..4, Z in 3..8. However, this is not true for
other domains of labels, as in Example 3.
Example 3. In the WordNet case presented in Section 2, labels are words
describing the variable object. The combination of two different labels (com-
bining function) returns a new label only if the two labels have a lexical
relation, fail otherwise. The decision is based on the WordNet network [18].
WordNet is a large lexical database of English. Nouns, verbs, adjectives
and adverbs are grouped into sets of cognitive synonyms (synsets). Synsets
are interlinked by means of conceptual-semantic and lexical relations. The
resulting network of meaningfully related words and concepts can be navi-
gated. WordNet superficially resembles a thesaurus, in that it groups words
together based on their meanings.
Here, the knowledge base locally stores some WordNet groups (a dy-
namic consultation to WordNet could be implemented, instead). Let be
program P represented by the following facts—where wordnet fact is a
simulated wordnet synset, while animal(Name) is a predicate describing an
animal’s name:
wordnet_fact ([ ‘ dog ’ ,‘ domestic dog ’ ,‘ canis ’ ,‘ pet ’ ,‘ mammal ’ ]).
wordnet_fact ([ ‘ cat ’ , ‘ domestic cat ’ , ‘ pet ’ , ‘ mammal ’ ]).
wordnet_fact ([ ‘ fish ’ ,‘ aquatic vertebrates ’ , ‘ vertebrate ’ ]).
wordnet_fact ([ ‘ frog ’ ,‘ toad ’ , ‘ anauran ’ , ‘ batrachian ’ ]).
pet_name ( ‘ minnie ’ ).
fish_name ( ‘ nemo ’ ).
animal ( X ) : - X ^[ ‘ pet ’] , pet_name ( X ).
animal ( X ) : - X ^[ ‘ fish ’] , fish_name ( X ).
Labelled Variables in Logic Programming: Foundations
The combining function fL is supposed to find and return a word-
net synset compatible with both labels. For instance, if `1 =
pet and `2 = ‘domestic cat0 , the new generated label `3 will be
[‘cat0 , ‘domestic cat0 , ‘pet0 , ‘mammal0 ]. The compatibility function fC in
this scenario is always true, since any animal name is considered compatible
with any animal group.
In order to show the construction of TP , let us consider the interpretation
I0 = ∅. Then, the subsequent step I1 can be computed as:
I1 = T P (I0 ) = hpet name(‘minnie0 ), []i, hfish name(‘nemo0 ), []i
Now, let us apply TP to I1 to compute I2 :
I2 = T P (I1 ) = I1 ∪
hanimal(‘minnie0 ), [[‘dog 0 , ‘domestic dog 0 , ‘canis0 , ‘pet0 , ‘mammal0 ]]i,
hanimal(‘minnie0 ), [[‘cat0 , ‘domestic cat0 , ‘pet0 , ‘mammal0 ]]i,
hanimal(‘nemo0 ), [[‘fish 0 , ‘aquatic vertebrates0 , ‘vertebrate0 ]]i
which is also the least fixpoint of TP .
In order to guarantee soundness and completeness of TP in the following we
demonstrate that it is a monotonic and continuous mapping on partial orders.
Definition 1. An interpretation I is a model of a program P if for each rule
r = p(ex) ← Λxe | b1 , . . . , bn of P and each valuation v of the variables in r on H
(let us denote with e t = v(e x)) it holds that
– if for i = 1, . . . , n there are hv(bi ), `ei i ∈ I
– such that X |= fC (v(bi ), `ei ) and
– X |= Λet , then it must be
– p(e t), feL r, Λet , `e1 , · · · , `en ∈ I.
Proposition 1. Given a LVLP program P and a LVLP domain X , TP is (1)
monotonic and (2) continuos and (3) TP (I) ⊆ I iff I is a model of P .
Proof. (1) Let I and J be two interpretations such that I ⊆ J. We need to prove
that TP (I) ⊆ TP (J). If a = h p(e
t), `e i ∈ TP (I) it means that there is a clause
r ∈ P , a valuation v on H for the variables in r and n elements hv(bi ), `ei i ∈ I
satisfying the remaining conditions. Since I ⊆ J they belong to J as well. Then
a ∈ TP (J).
(2) Let usSconsider aS chain of interpretations I0 ⊆ I1 ⊆ . . . . We need to prove
∞ ∞
that: TP k=0 kI = k=0 TP (Ik ).
S∞
(⊆) Let a = h p(t), ` i ∈ TP
e e
i=0 Ik . This means that there is a clause r ∈ P ,
S∞
a valuation v on H for the variables in r and n elements hv(bi ), `ei i ∈ k=0 Ik
satisfying the remaining conditions. This means that there are j1 , . . . , jn such
that for i = 1, . . . , n hv(bi ), `ei i ∈ Iji . Let j = max{j1 , . . . , jn }, since I0 ⊆ I1 ⊆
Calegari, Denti, Dovier & Omicini
··· ⊆
S∞Ij we have that all hv(bi ), `ei i ∈ Ij . Thus a ∈ TP (Ij+1 ) and henceforth
a ∈ k=0 TP (Ik ).
S∞
(⊇) Let a = h p(e t), `e i ∈ k=0 TP (Ik ). This means
S∞ that there is j such that
a ∈ TP (Ij ). Then, due to monotonicity, a ∈ TP k=0 Ik .
(3) Let TP (I) ⊆ I and let r = p(e x) ← Λxe , b1 , . . . , bn be a generic clause of P ,
and v be a generic valuation on H of all the variables of r. If we assume that
hv(bi ), `ei i ∈ I for i = 1, . . . , n, and that X |= fC (v(bi ), `ei ) and X |= Λet , then
the pair h = v(p(e e ∈ TP (I) by definition of TP —and `e is the same of the
x), `)
definition of model. Since TP (I) ⊆ I then h ∈ I, therefore (since r and v are
chosen in general) I is a model of P .
On the other hand, if I is a model of P we prove that TP (I) ⊆ I. Let
a = h p(e t), `e i ∈ TP (I). This means that there is a rule r = p(e x) ← Λxe , b1 , . . . , bn
of P and a valuation v of the variables in r on H such that fori = 1, . . . , n
there are v(bi ), `ei ∈ I and X |= Λet and `e = feL r, Λet , `e1 , · · · , `en ). such that
X |= fC (v(bi ), `ei ). Since I is a model, and X |= fC (v(bi ), `ei ) then a ∈ I. t
u
S
Let be TP ↑ ω defined as usual: TP ↑ ω = {TP ↑ k : k ≥ 0}. Then:
Corollary 1. There is a notion of least model which is TP ↑ ω.
Proof. Immediate from Knaster-Tarksi theorem, Kleene’s fixpoint Theorem, and
Proposition 1. t
u
4.2 Operational Semantics
In this section we define the operational interpretation of labels: our approach is
inspired by the methodology introduced for Constraint Logic Programming [4,
12, 13], namely we define the LVLP abstract state machine based on that sug-
gested by Colmerauer for Prolog III. It resembles a push-down automaton [11]
whose stack is updated whenever a program rule is applied. We define a labelled-
machine state σ as the triplet:
σ = ht0 t1 ...tn , W, Λi
where
– t0 t1 ...tn is the list of terms (goals)
– W is the current list of variables bindings
– Λ is the set of the current labelling associations on W .
An inference step for the machine consists of making a transition from the state
σ to a state σ 0 by applying a program rule. Considering the rule (m ≥ 0)
s0 ← Λ0 , s1 , s2 , . . . , sm
where Λ0 is the set of the labellings of the rule, if the following conditions hold:
– ∃ mgu θ such that θ(t0 ) = θ(s0 ) and
Labelled Variables in Logic Programming: Foundations
– feθL (Λ, θ(Λ0 )) 6= ∅
the rule is applied (fail otherwise). The function feθL is a generalisation of the
combining function fL in that takes as arguments two vectors of labelling asso-
ciations. If xi occurs both in Λ and θ(Λ0 ) with labels ` and `0 , `00 = fL (`, `0 ) is
first calculated, then, if fC (θ(xi ), `00 ) = true the labelling association hxi , `00 i is
returned. The new state becomes:
σ 0 = hθ(s1 , . . . , sm , t1 , . . . , tn ), W 0 = W ◦ θ, Λ00 = feθL (Λ, θ(Λ0 ))i
where ◦ applies the classical composition of substitutions.
A solution is found when a final state is reached. The final state has the form:
σf = (, Wf , Λf )
where is the empty sequence, Wf is the final list of variables and bindings,
Λf is the corresponding labelling associations set. A sequence of applications of
inference steps is said a derivation. A derivation is successful if it ends in a final
state, failing if it ends in a non-final state where no inference step is possible.
Proposition 2. Let p(e x) be an atom, v a valuation on H such that v(e x) =
t where e
e t are ground terms, and `e a list of labels. Then there is a successful
derivation for hp(e
t), v, hv(e e iff hp(e
x), `ii e ∈ TP ↑ ω.
t), `i
Proof (In the following we provide a proof sketch, deferring the full proof to a
future paper for the sake of brevity).
(→). We prove the proposition by induction on the length k of the derivation.
If k = 0 the result holds trivially.
For the inductive case, let us suppose that there is a successful derivation
for hp(e t), v, hv(e
x), `ii
e of k + 1 steps. Let us focus on the first step: there is a
0
rule r: s0 ← Λ , s1 , s2 , . . . , sm such that θ(p(e t)) = θ(s0 ) leading to the new
state σ = hθ(s1 , s2 , . . . , sm ), v ◦ θ, Λ00 = feθL (Λ, θ(Λ0 )i, where fC (Λ00 ) = true, that
admits a successful derivation of k steps.
Consider now the states σ1 , . . . , σm defined as σi = hθ(si ), v ◦ θ, Λ00i i where
Λi is the restriction of Λ00 to the variables in si . Since σ admits a successful
00
derivation of k + 1 steps, each σi should admit a successful derivation of at most
k steps.
If for all i ∈ {1, . . . , m}, θ(si ) is ground, then, by inductive hypothesis we
have that hθ(si ), `i i ∈ TP ↑ ω where `i = π2 (Λ00i ), and hence that there are hi s
such that hθ(si ), `i i ∈ TP ↑ hi . Since Tp is monotonic, all of them belong to
TP ↑ h where h = maxi=1,...,m hi . Then, by applying TP considering the rule
r, since we already know that Λ00 = feθL (Λ, θ(Λ0 )), and fC (Λ00 ) = true, we have
that hp(e e ∈ TP ↑ h + 1, hence to TP ↑ ω.
t), `i
If for some i, θ(si ) is not ground, the above property holds for any ground
instantiation of the remaining variables and again the results follows.
(←). Now, let us analyse the converse direction. If hp(e e ∈ TP ↑ ω this means
t), `i
that there is a k ≥ 0 such that hp(e e ∈ TP ↑ k.
t), `i
Calegari, Denti, Dovier & Omicini
Let us prove by induction on k. Again, if k = 0 the result holds trivially.
Let us suppose now that hp(e e ∈ TP ↑ k + 1. This means (by definition of
t), `i
TP ) that there is a rule r: s0 ← Λ0 , s1 , s2 , . . . , sm such that s0 = p(e x) and
there is a valuation u on H such that u(s0 ) = p(e t) and that, in particular,
hs1 , `1 i, . . . , hsm , `m i ∈ TP ↑ k (and fL can be computed and fC is true on these
arguments). By inductive hypothesis, for i ∈ {1, . . . , m} there is a derivation,
say, of hi steps for σi = hu(si ), v ◦ u, hu(si ), `i ii
Since fC is true on such arguments Pmand fL can be computed, the same holds
for TP : so, we have a derivation of i=1 hi + 1 steps for hp(e
t), v ◦ u ◦ θ, he
t, `ii.
e
This completes the proof of the inductive step. t
u
5 Conclusions & Future Work
The primary result of this paper is the definition of the LVLP theoretical frame-
work, where different domain-specific computational models can be expressed via
labelled variables, capturing suitably-tailored labelled models. The framework is
aimed at extending LP to face the challenges of today’s pervasive systems, by
providing the models and technologies required to effectively support distributed
situated intelligence, while maintaining the features of a declarative program-
Fig. 1. Envisioning tuProlog / LVLP middleware for distributed (labelled) LP
Labelled Variables in Logic Programming: Foundations
ming paradigm. We also present the fixpoint and operational semantics, discuss
correctness, completeness, and equivalence.
Beside completing our LVLP prototype [3], currently implemented over
tuProlog [5], a focal point of our forthcoming activity is the design and im-
plementation of a full-fledged middleware for tuProlog and LVLP, which could
be exploited to test the effectiveness of distributed LP (and its extensions) in
real-world pervasive intelligence scenarios—a sketch of the forthcoming middle-
ware is reported in Fig. 1.
Future work will be devoted to a more complete proof of the result sketched
in Subsection 4.1 as well as to the deeper exploration and better understanding
of the consequences of applying labels to formulas, as suggested by Gabbay
[8]. Other research lines will possibly include the further development of the
Labelled tuProlog [5] prototype, as well as the application of the LVLP framework
to different scenarios and approaches—such as probabilistic LP [17], the many
CLP approaches [4], distributed ASP reasoning [7], and action languages [6].
Acknowledgements. Agostino Dovier is partially supported by INdAM-GNCS
2015 and 2016 projects.
References
1. Alsinet, T., Chesñevar, C.I., Godo, L., Simari, G.R.: A logic programming frame-
work for possibilistic argumentation: Formalization and logical properties. Fuzzy
Sets and Systems 159(10), 1208–1228 (May 2008), http://dx.doi.org/10.1016/
j.fss.2007.12.013
2. Barany, V., ten Cate, B., Kimelfeld, B., Olteanu, D., Vagena, Z.: Declarative proba-
bilistic programming with Datalog. In: Martens, W., Zeume, T. (eds.) 19th Interna-
tional Conference on Database Theory (ICDT 2016). LIPIcs, vol. 48, pp. 7:1–7:19.
Dagstuhl, Germany (2016), http://dx.doi.org/10.4230/LIPIcs.ICDT.2016.7
3. Calegari, R., Denti, E., Omicini, A.: Labelled variables in logic programming: A
first prototype in tuProlog. In: Bellodi, E., Bonfietti, A. (eds.) AI*IA 2015 DC
Proceedings. CEUR Workshop Proceedings, vol. 1485, pp. 25–30. AI*IA, Ferrara,
Italy (23–24 Sep 2015), http://ceur-ws.org/Vol-1485/proceedings.pdf#page=
30
4. Cohen, J.: Constraint Logic Programming languages. Communications of the ACM
33(7), 52–68 (Jul 1990), http://dx.doi.org/10.1145/79204.79209
5. Denti, E., Omicini, A., Ricci, A.: Multi-paradigm Java-Prolog integration in
tuProlog. Science of Computer Programming 57(2), 217–250 (Aug 2005), http:
//dx.doi.org/10.1016/j.scico.2005.02.001
6. Dovier, A., Formisano, A., Pontelli, E.: Autonomous agents coordination: Action
languages meet CLP(FD) and Linda. Theory and Practice of Logic Programming
13(2), 149–173 (Sep 2013), http://dx.doi.org/10.1017/S1471068411000615
7. Dovier, A., Pontelli, E.: Present and future challenges for ASP systems. In: Erdem,
E., Lin, F., Schaub, T. (eds.) Logic Programming and Nonmonotonic Reason-
ing. 10th International Conference, LPNMR 2009, Potsdam, Germany, September
14-18, 2009. Proceedings, pp. 622–624. Springer (2009), http://dx.doi.org/10.
1007/978-3-642-04238-6_70
Calegari, Denti, Dovier & Omicini
8. Gabbay, D.M.: Labelled Deductive Systems, Volume 1. Clarendon Press, Oxford
Logic Guides 33 (Sep 1996)
9. Hofstedt, P.: Multiparadigm Constraint Programming Languages. Cognitive Tech-
nologies, Springer (2011), http://dx.doi.org/10.1007/978-3-642-17330-1
10. Holzbaur, C.: Metastructures vs. attributed variables in the context of extensible
unification. In: Bruynooghe, M., Wirsing, M. (eds.) Programming Language Imple-
mentation and Logic Programming, Lecture Notes in Computer Science, vol. 631,
pp. 260–268. Springer (1992), http://dx.doi.org/10.1007/3-540-55844-6_141,
4th International Symposium (PLILP’92) Leuven, Belgium, August 26–28, 1992
Proceedings
11. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory,
Languages, and Computation. Pearson / Addison-Wesley, 3rd edn. (2007)
12. Imbert, J.L., Cohen, J., Weeger, M.D.: An algorithm for linear constraint solving:
Its incorporation in a Prolog meta-interpreter for CLP. The Journal of Logic Pro-
gramming 16(3), 235–253 (1993), http://dx.doi.org/10.1016/0743-1066(93)
90044-H
13. Jaffar, J., Maher, M.J.: Constraint Logic Programming: A survey. The Journal
of Logic Programming 19–20(Supplement 1), 503–581 (May–Jul 1994), http://
dx.doi.org/10.1016/0743-1066(94)90033-7, Special Issue: Ten Years of Logic
Programming
14. Mariani, S., Omicini, A.: Coordinating activities and change: An event-driven ar-
chitecture for situated MAS. Engineering Applications of Artificial Intelligence 41,
298–309 (May 2015), http://dx.doi.org/10.1016/j.engappai.2014.10.006
15. Omicini, A., Zambonelli, F.: MAS as complex systems: A view on the role of
declarative approaches. In: Leite, J.A., Omicini, A., Sterling, L., Torroni, P. (eds.)
Declarative Agent Languages and Technologies, Lecture Notes in Computer Sci-
ence, vol. 2990, pp. 1–17. Springer (May 2004), http://dx.doi.org/10.1007/
978-3-540-25932-9_1, 1st International Workshop (DALT 2003), Melbourne,
Australia, 15 Jul. 2003. Revised Selected and Invited Papers
16. Russo, A.: Generalising propositional modal logic using labelled deductive sys-
tems. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, Applied
Logic Series, vol. 3, pp. 57–73. Springer (1996), http://dx.doi.org/10.1007/
978-94-009-0349-4_2
17. Skarlatidis, A., Artikis, A., Filippou, J., Paliouras, G.: A probabilistic logic pro-
gramming event calculus. Theory and Practice of Logic Programming 15(Special
Issue 02 (Probability, Logic and Learning)), 213–245 (3 2015), http://dx.doi.
org/10.1017/S1471068413000690
18. WordNet: Home page. http://wordnet.princeton.edu