The IDP Language¶
Overview¶
The IDP language is used to create knowledge bases. An IDP source file is made of the following blocks of code:
- vocabulary
specify the types, predicates, functions and constants used to describe the problem domain.
- theory
specify the definitions and constraints satisfied by any solutions.
- structure
(optional) specify the interpretation of some predicates, functions and constants.
- display
(optional) configure the user interface of the Interactive Consultant.
- main
(optional) executable procedure in the context of the knowledge base
The basic skeleton of an IDP knowledge base for the Interactive Consultant is as follows:
vocabulary {
// here comes the specification of the vocabulary
}
theory {
// here comes the definitions and constraints
}
structure {
// here comes the interpretation of some symbols
}
display {
// here comes the configuration of the user interface
}
Everything between //
and the end of the line is a comment.
Shebang¶
New in version 0.5.5
The first line of an IDP source file may be a shebang line, specifying the version of IDP-Z3 to be used. When a version is specified, the Interactive Consultant and Web IDE will be redirected to a server on the web running that version. The list of versions is available here. (The IDP-Z3 executable ignores the shebang.)
Example: #! IDP-Z3 0.5.4
Vocabulary¶
vocabulary V {
// here comes the vocabulary named V
}
The vocabulary block specifies the types, predicates, functions and constants used to describe the problem domain. If the name is omitted, the vocabulary is named V.
Each declaration goes on a new line (or are space separated).
Symbols begins with an alphabetic character or _
, followed by alphanumeric characters or _
.
Symbols can also be string literals delimited by '
, e.g., 'blue planet'
.
Types¶
IDP-Z3 supports built-in and custom types.
The built-in types are: 𝔹
, ℤ
, ℝ
, Date
, and Symbol
.
The equivalent ASCII symbols are Bool
, Int
, and Real
.
Boolean literals are true
and false
.
Number literals follow Python’s conventions.
Date literals follow ISO 8601 conventions, prefixed with #
(#yyyy-mm-dd
).
#TODAY
is also a Date literal.
The type Symbol
has one constructor for each symbol (i.e., function, predicate or constant) declared in the vocabulary.
The constructors are the names of the symbol, prefixed with `
Custom types are declared using the keyword type
, e.g., type color
.
Their name should be singular and capitalized, by convention.
Their extension can be defined in a structure, or directly in the vocabulary, by specifying:
a list of (ranges of) numeric literals, e.g.,
type someNumbers := {0,1,2}
ortype byte := {0..255}
a list of (ranges of) dates, e.g.,
type dates := {#2021-01-01, #2022-01-01}
ortype dates := {#2021-01-01 .. #2022-01-01}
a list of nullary constructors, e.g.,
type Color := {Red, Blue, Green}
a list of n-ary constructors; in that case, the enumeration must be preceded by
constructed from
, e.g.,type Color2 := constructed from {Red, Blue, Green, RGB(R: Byte, G: Byte, B: Byte)}
In the above example, the constructors of `Color
are : Red
, Blue
, Green
.
The constructors of `Color2
are : Red
, Blue
, Green
and RGB
.
Each constructor have an associated function (e.g., is_Red
, or is_RGB
) to test if a Color2 term was created with that constructor.
The RGB
constructor takes 3 arguments of type Byte
.
R
, G
and B
are accessor functions: when given a Color2 term constructed with RGB, they return the associated Byte.
(When given a Color2 not constructed with RGB, they may raise an error)
Functions¶
The functions with name MyFunc1
, MyFunc2
, input types T1
, T2
, T3
and output type T
, are declared by:
myFunc1, myFunc2 : T1 ⨯ T2 ⨯ T3 → T
Their name should not start with a capital letter, by convention.
The ASCII equivalent of ⨯
is *
, and of →
is ->
.
IDP-Z3 does not support partial functions.
Built-in functions¶
The following functions are built-in:
abs: Int → Int
(orabs: Float → Float
) yields the absolute value of an integer (or float) expression;arity: Symbol → Symbol
yields the arity of a symbol;input_domain : Symbol ⨯ ℤ → Symbol
yields the n-th input-domain of a symbol;output_domain: Symbol → Symbol
yields the output domain of a symbol.
Predicates¶
The predicates with name myPred1
, myPred2
and argument types T1
, T2
, T3
are declared by:
myPred1, myPred2 : T1 ⨯ T2 ⨯ T3 → 𝔹
Their name should not start with a capital letter, by convention.
The ASCII equivalent of →
is ->
, and of 𝔹
is Bool
.
Propositions and Constants¶
A proposition is a predicate of arity 0; a constant is a function of arity 0.
MyProposition : () → 𝔹
MyConstant: () → Int
Include another vocabulary¶
A vocabulary W may include a previously defined vocabulary V:
vocabulary W {
extern vocabulary V
// here comes the vocabulary named V
}
Theory¶
theory T:V {
// here comes the theory named T, on vocabulary named V
}
A theory is a set of constraints and definitions to be satisfied. If the names are omitted, the theory is named T, for vocabulary V.
Before explaining their syntax, we need to introduce the concept of term.
Mathematical expressions and Terms¶
A term is inductively defined as follows:
- Numeric literal
Numeric literals that follow the Python conventions are numerical terms of type
Int
orReal
.- Constructor
Each constructor of a type is a term having that type.
- Variable
a variable is a term. Its type is derived from the quantifier expression that declares it (see below).
- Function application
F(t_1, t_2,.., t_n)
is a term, whenF
is a function symbol of arityn
, andt_1, t_2,.., t_n
are terms. Each term must be of the appropriate type, as defined in the function declaration in the vocabulary. The resulting type of the function application is also defined in the function declaration. If the arity ofF
is 0, i.e., ifF
is a constant, thenF()
is a term.$(s)(t_1, t_2,.., t_n)
is a term, whens
is an expression of type Symbol that denotes a function of arityn
, andt_1, t_2,.., t_n
are terms.Please note that there are built-in functions (see Built-in functions).
- Negation
-
t
is a numerical term, whent
is a numerical term.- Arithmetic
t_1 ꕕ t_2
is a numerical term, whent_1
,t_2
are two numerical terms, andꕕ
is one of the following math operators+, -, * (or ⨯), /, ^, %
. Mathematical operators can be chained as customary (e.g.x+y+z
). The usual order of binding is used.- Parenthesis
(
t
) is a term, whent
is a term- Cardinality aggregate
#{v_1 in typeOfV_1, .., v_n in typeOfV_n : ϕ}
is a numerical term whenv_1 v_2 .. v_n
are variables, andϕ
is a sentence containing these variables.The term denotes the number of tuples of distinct values for
v_1 v_2 .. v_n
which makeϕ
true.- Arithmetic aggregate
ꕕ{v_1 in typeOfV_1, .., v_n in typeOfV_n : ϕ : t}
is a numerical term whenꕕ
issum
,v_1 v_2 .. v_n
are variables,ϕ
is a sentence, andt
is a term.The term denotes the sum of
t
for each distinct tuple of values forv_1 v_2 .. v_n
which makeϕ
true.- (if .. then .. else ..)
(if\ t_1\ then\ t_2\ else\ t_3)
is a term whent_1
is a sentence,t_2
andt_3
are terms of the same type.
Sentences and constraints¶
A constraint is a sentence followed by .
.
A sentence is inductively defined as follows:
- true and false
true
andfalse
are sentences.
- Predicate application
P(t_1, t_2,.., t_n)
is a sentence, whenP
is a predicate symbol of arityn
, andt_1, t_2,.., t_n
are terms. Each term must be of the appropriate type, as defined in the predicate declaration. If the arity ofP
is 0, i.e., ifP
is a proposition, thenP()
is a sentence.$(s)(t_1, t_2,.., t_n)
is a sentence, whens
is an expression of type Symbol that denotes a predicate of arityn
, andt_1, t_2,.., t_n
are terms.- Comparison
t_1 ꕕ t_2
is a sentence, whent_1
,t_2
are two numerical terms andꕕ
is one of the following comparison operators<, ≤, =, ≥, >, ≠
(or, using ascii characters:=<, >=, ~=
). Comparison operators can be chained as customary.- Negation
¬ϕ
is a sentence (or, using ascii characters:~ϕ
) whenϕ
is a sentence.- Logic connectives
ϕ_1 ꕕ ϕ_2
is a sentence whenϕ_1, ϕ_2
are two sentences andꕕ
is one of the following logic connectives∨,∧,⇒,⇐,⇔
(or using ascii characters:|, \&, =>, <=, <=>
respectively). Logic connectives can be chained as customary.- Parenthesis
(
ϕ
) is a sentence whenϕ
is a sentence.
- Enumeration
An enumeration (e.g.
p := {1;2;3}
) is a sentence. Enumerations follow the syntax described in structure.- Quantified formulas
Quantified formulas are sentences. They have one of the following forms, where
v_1, .., v_n
are variables,p, p_1, .., p_n
are types or predicates, andϕ
is a sentence involving those variables:∀ v_1, v_n: ϕ(v_1, v_n). ∀ v_1, v_n ∈ p: ϕ(v_1, v_n). ∀ (v_1, v_n) ∈ p: ϕ(v_1, v_n). ∀ v_1 ∈ p_1, v_n ∈ p_n: ϕ(v_1, v_n).
Alternatively, the existential quantifier,
∃
, can be used. Ascii characters can also be used:?
,!
, respectively. For example,! x, y in Int: f(x,y)=f(y,x).
A variable may only occur in the
ϕ
sentence of a quantifier declaring that variable. In the first form above, the type of each variable is inferred from their use inϕ
.When quantifying a formula of type
Symbol
, the expression must contain a “guard” to prevent arity or type error. A guard is a condition that can be resolved using the available enumerations. In the following example,symmetric
must be defined by enumeration.symmetric := {`edge} ∀s ∈ Symbol: symmetric(s) => (∀x, y : $(s)(x,y) ⇒ $(s)(y,x)).
An alternative is to use the introspection functions
arity, input_domain, output_domain
:∀s ∈ Symbol: arity(s)=2 ∧ input_domain(s,1)=input_domain(s,2) ⇒ (∀x ∈ $(input_domain(s,1)), y ∈ $(input_domain(s,2)) : $(s)(x,y) ⇒ $(s)(y,x)).
- “is (not) enumerated”
f(a,b) is enumerated
andf(a,b) is not enumerated
are sentences, wheref
is a function defined by an enumeration and applied to argumentsa
andb
. Its truth value reflects whether(a,b)
is enumerated inf
’s enumeration. If the enumeration has a default value, every tuple of arguments is enumerated.- “(not) in {1,2,3,4}”
f(args) in enum
andf(args) not in enum
are sentences, wheref
is a function applied to argumentsargs
andenum
is an enumeration. This can also be written using Unicode:f() ∈ {1,2,3}
orf() ∉ {1,2,3}
.- if .. then .. else ..
if t_1 then t_2 else t_3
is a sentence whent_1
,t_2
andt_3
are sentences.
Definitions¶
A definition defines concepts, i.e. predicates or functions, in terms of other concepts.
A definition consists of a set of rules, enclosed by {
and }
.
Rules have one of the following forms:
∀ v_1 ∈ T_1, v_n ∈ T_n: P(t_1, .., t_n) ← |phi|.
∀ v_1 ∈ T_1, v_n ∈ T_n: F(t_1, .., t_n) = t ← |phi|.
where P is a predicate symbol, F is a function symbol, t
, t_1, t_2,.., t_n
are terms that may contain the variables v_1 v_2 .. v_n
and ϕ
is a formula that may contain these variables.
P(t_1, t_2,.., t_n)
is called the head of the rule and ϕ
the body.
<-
can be used instead of ←
.
If the body is true
, the left arrow and body of the rule can be omitted.
Structure¶
structure S:V {
// here comes the structure named S, for vocabulary named V
}
A structure specifies the interpretation of some type, predicates and functions, by enumeration. If the names are omitted, the structure is named S, for vocabulary V.
A structure is a set of statement of the form <symbol> := <enumeration>
,
e.g., P := {1..9}
, where the enumeration can be:
- for nullary predicates (propositions)
true
orfalse
- for non-numeric types and unary predicates:
a set of rigid terms (numbers, dates, identifiers, or constructors applied to rigid terms), e.g.,
{red, blue, green}
.- for numeric types and unary predicates:
a set of numeric literals and ranges, e.g.,
{0,1,2}
,{0..255}
or{0..9, 90..99}
- for date types and unary predicates:
a set of date literals and ranges, e.g.,
{#2021-01-01, #2022-01-01}
or{#2021-01-01 .. #2022-01-01}
- for types:
a set of n-ary constructors, preceded by
constructed from
, e.g.,constructed from {Red, Blue, Green, RGB(R: Byte, G: Byte, B: Byte)}
(see more details in types)- for n-ary predicates:
a set of tuples of rigid terms, e.g.,
{(a,b), (a,c)}
.- for nullary functions:
a rigid term, e.g.
5
or#2021-01-01
, orred
orrgb(0,0,0)
- for n-ary functions:
a set of tuples and their associated values, e.g.,
{ (1,2)->3, (4, 5)->6 }
Additional notes:
the enumeration for a predicate specifies the tuples that make the predicate true; any other tuple make it false.
the enumeration for a function may be followed by
else <default>
, where<default>
is a default value (a rigid term), i.e., a value for the non-enumerated tuples, if any.parenthesis around a tuple can be omitted when the arity is 1, e.g.,
{1-2, 3->4}
a predicate may be enumerated using a CSV format, with one tuple per line, e.g., :
P := {
1 2
3 4
5 6
}
Main block¶
The main block consists of python-like statements to be executed by the IDP-Z3 executable or the Web IDE, in the context of the knowledge base. It takes the following form:
procedure main() {
// here comes the python-like code to be executed
}
The vocabularies, theories and structures defined in other blocks of the IDP source file are available through variables of the same name.
The following functions are available:
- model_check(theory, structure=None)
Returns string
sat
,unsat
orunknown
, depending on whether the theory has a model expanding the structure.theory
andstructure
can be lists, in which case their elements are merged. The structure is optional.For example,
print(model_check(T, S))
will printsat
if theory namedT
has a model expanding structure namedS
.- model_expand(theory, structure=None, max=10, complete=False)
Returns a list of models of the theory that are expansion of the structure.
theory
andstructure
can be lists, in which case their elements are merged. The structure is optional. The result is limited tomax
models (10 by default), or unlimited ifmax
is 0. The models can be asked to be complete or partial (i.e., in which “don’t care” terms are not specified).For example,
print(model_expand(T, S))
will print (up to) 10 models of theory namedT
expanding structure namedS
.- model_propagate(theory, structure=None)
Returns a list of assignments that are true in any expansion of the structure consistent with the theory.
theory
andstructure
can be lists, in which case their elements are merged. The structure is optional. Terms and symbols starting with ‘_’ are ignored.For example,
print(model_propagate(T, S))
will print the assignments that are true in any expansion of the structure namedS
consistent with the theory namedT
.- decision_table(theories, structures=None, goal_string=””, timeout=20, max_rows=50, first_hit=True)
Experimental. Returns the rows for a decision table that defines
goal_string
.goal_string
must be a predicate application defined in the theory.- pretty_print(…)
Prints its argument on stdout, in a readable form.
Problem class¶
The main block can also use instances of the Problem
class.
This is beneficial when several inferences must be made in a row (e.g., Problem(T,S).propagate().simplify().formula()
).
Instances of the Problem
class represent a collection of theory and structure blocks.
The class has the following methods:
- __init__(self, *blocks, extended=False)
Creates an instance of
Problem
for the list of blocks, e.g.,Problem(T,S)
.Use extended=True when the truth value of inequalities and quantified formula is of interest (e.g. for the Interactive Consultant).
- add(self, *blocks)
Adds a list of theory or structure blocks to the problem.
- assert_(self, code: str, value: Any)
Asserts that an expression has a value, e.g. problem.assert_(“p()”, True).
- copy(self)
Returns an independent copy of a problem.
- formula(self)
Returns a python object representing the logic formula equivalent to the problem. This object can be converted to a string using
str()
.- expand(self, max=10, complete=False)
Returns a list of models of the theory that are expansion of the known assignments. The result is limited to
max
models (10 by default), or unlimited ifmax
is 0. The models can be asked to be complete or partial (i.e., in which “don’t care” terms are not specified).- optimize(self, term, minimize=True, complete=False)
Returns the problem with its
assignments
property updated with values such that the term is minimized (or maximized ifminimize
isFalse
)term
is a string (e.g."Length(1)"
). The models can be asked to be complete or partial (i.e., in which “don’t care” terms are not specified).- symbolic_propagate(self)
Returns the problem with its
assignments
property updated with direct consequences of the constraints of the problem. This propagation is less complete thanpropagate()
.- propagate(self)
Returns the problem with its
assignments
property updated with values for all terms and atoms that have the same value in every model (i.e., satisfying structure of the problem). Terms and propositions starting with ‘_’ are ignored.- get_range(self, term:str)
Returns a copy of the problem, with its
assignments
property containing a description of the possible values of the term.- explain(self, consequence)
Returns the facts and laws to explain a consequence in the Problem.
The string
consequence
must be a key in theassignments
property of the Problem. The facts are a list of Assignment, and the laws are a list of Expression.- simplify(self)
Returns a simpler copy of the problem, with a simplified formula obtained by substituting terms and atoms by their known values.
- decision_table(self, goal_string=””, timeout=20, max_rows=50, first_hit=True)
Experimental. Returns the rows for a decision table that defines
goal_string
.goal_string
must be a predicate application defined in the theory. The problem must be created withextended=True
.
Differences with IDP3¶
Here are the main differences with IDP3, listed for migration purposes:
- min/max aggregates
IDP-Z3 does not support these aggregates (yet). See IEP 05
- Inductive definitions
IDP-Z3 does not support inductive definitions.
- Infinite domains
IDP-Z3 supports infinite domains:
Int, Real
. However, quantifications over infinite domains is discouraged.- if .. then .. else ..
IDP-Z3 supports if .. then .. else .. terms and sentences.
- LTC
IDP-Z3 does not support LTC vocabularies.
- Namespaces
IDP-Z3 does not support namespaces.
- Partial functions
IDP-Z3 does not support partial functions. The handling of division by 0 may differ. See IEP 07
- Programming API
IDP3 procedures are written in Lua, IDP-Z3 procedures are written in Python-like language.
- Qualified quantifications
IDP-Z3 does not support qualified quantifications, e.g.
!2 x[color]: p(x).
. (p. 11 of the IDP3 manual).- Structure
IDP-Z3 does not support
u
uncertain interpretations (p.17 of IDP3 manual). Function enumerations must have anelse
part. (see also IEP 04)- Type
IDP-Z3 does not support type hierarchies.
To improve performance, do not quantify over the value of a function.
Use p(f(x))
instead of ?y: f(x)=y & p(y)
.
Syntax summary¶
The following code illustrates the syntax of IDP-Z3. T denotes a type, c a constructor, p a proposition or predicate, f a constant or function. The equivalent ASCII-only encoding is shown on the right.
vocabulary V {
type T
type T := {c1, c2, c3}
type T := constructed from {c1, c2(T1, f:T2)}
type T := {1,2,3}
type T := {1..3}
// built-in types: 𝔹, ℤ, ℝ, Date, Symbol Bool, Int, Real, Date, Symbol
p : () → 𝔹 p: () -> Bool
p1, p2 : T1 ⨯ T2 → 𝔹 p1, p2: T1*T2 -> Bool
f: T → T f: T -> T
f1, f2: T → T f1, f2: T -> T
[this is the intended meaning of p]
p : () → 𝔹
extern vocabulary W
}
theory T:V {
(¬p1()∧p2() ∨ p3() ⇒ p4() ⇔ p5()) ⇐ p6(). (~p1()&p2() | p3() => p4() <=> p5()) <= p6().
p(f1(f2())).
f1() < f2() ≤ f3() = f4() ≥ f5() > f6(). f1() < f2() =< f3() = f4() >= f5() > f6().
f() ≠ c. f() ~= c.
∀x,y ∈ T: p(x,y). !x,y in T: p(x,y).
∀x ∈ p, (y,z) ∈ q: q(x,x) ∨ p(y) ∨ p(z). !x in p, (y,z) in q: q(x,x) | p(y) | p(z).
∃x ∈ Symbol: arity(x)=0 ∧ $(x)(). ?x in Symbol: arity(x)=0 & $(x)().
∃x ∈ $(input_domain(`p,1)): p(x). ?x in $(input_domain(`p,1)): p(x).
∃x: p(x). ?x: p(x).
f() in {1,2,3}.
f() = #{x∈T: p(x)}. f() = #{x in T: p(x)}.
f() = sum{x∈T: p(x): f(x)}. f() = sum{x in T: p(x): f(x)}.
if p1() then p2() else p3().
f1() = if p() then f2() else f3().
p := {1,2,3}
p(#2020-01-01) is enumerated.
p(#TODAY) is not enumerated.
{ p(1).
∀x∈T: p1(x) ← p2(x). !x in T: p1(x) <- p2(x).
f(1)=1.
∀x: f(x)=1 ← p(x). !x: f(x)=1 <- p(x).
}
[this is the intended meaning of the rule]
(p()).
}
structure S:V {
p := false
p := {1,2,3}
p := {0..9, 100}
p := {#2021-01-01}
p := {(1,2), (3,4)}
p := {
1 2
3 4
}
f := 1
f := {→1} f := {-> 1}
f := {1→1, 2→2} f := {1->1, 2->2}
f := {(1,2)→3} else 2 f := {(1,2)->3} else 2
}
display {
expand(`p).
hide(`p).
view() = expanded.
relevant(`p1, `p2).
goal(`p).
optionalPropagation.
}
procedure main() {
pretty_print(model_check (T,S))
pretty_print(model_expand (T,S))
pretty_print(model_propagate(T,S))
}
See also the Built-in functions.