The IDP Language

Overview

The IDP language is used to create knowledge bases. An IDP program 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 program 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 has the following built-in types: 𝔹, , , Symbol. The equivalent ASCII symbols are Bool, Int, and Real.

Custom types can be defined by specifying a range of numeric literals, or a list of constructors (of arity 0). Their name should be capitalized, by convention.

type Side := {1..4}
type Color := {red, blue, green}

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 `

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.

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 or Real.

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, when \(F\) is a function symbol of arity \(n\), and \(t_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 of \(F\) is 0, i.e., if \(F\) is a constant, then \(F()\) is a term.

Negation

-\(t\) is a numerical term, when \(t\) is a numerical term.

Arithmetic

\(t_1 ꕕ t_2\) is a numerical term, when \(t_1\), \(t_2\) are two numerical terms, and \(ꕕ\) is one of the following math operators \(+, -, *, /, \hat{}, \%\). Mathematical operators can be chained as customary (e.g. \(x+y+z\)). The usual order of binding is used.

Parenthesis

(\(t\)) is a term, when \(t\) is a term

Cardinality aggregate

\(\#\{v_1 in typeOfV_1, .., v_n in typeOfV_n : \phi\}\) is a numerical term when \(v_1 v_2 .. v_n\) are variables, and \(\phi\) 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 \(\phi\) true.

Arithmetic aggregate

\(ꕕ\{v_1 in typeOfV_1, .., v_n in typeOfV_n : \phi : t\}\) is a numerical term when \(ꕕ\) is \(sum\), \(v_1 v_2 .. v_n\) are variables, \(\phi\) is a sentence, and \(t\) is a term.

The term denotes the sum of \(t\) for each distinct tuple of values for \(v_1 v_2 .. v_n\) which make \(\phi\) true.

(if .. then .. else ..)

\((if\ t_1\ then\ t_2\ else\ t_3)\) is a term when \(t_1\) is a sentence, \(t_2\) and \(t_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 and false are sentences.

Predicate application

\(P(t_1, t_2,.., t_n)\) is a sentence, when \(P\) is a predicate symbol of arity \(n\), and \(t_1, t_2,.., t_n\) are terms. Each term must be of the appropriate type, as defined in the predicate declaration. If the arity of \(P\) is 0, i.e., if \(P\) is a proposition, then \(P()\) is a sentence.

Comparison

\(t_1 ꕕ t_2\) is a sentence, when \(t_1\), \(t_2\) are two numerical terms and \(ꕕ\) is one of the following comparison operators \(<, ≤, =, ≥, >, ≠\) (or, using ascii characters: \(=<, >=, \sim=\)). Comparison operators can be chained as customary.

Negation

\(\lnot\) \(\phi\) is a sentence (or, using ascii characters: \(\sim \phi\)) when \(\phi\) is a sentence.

Logic connectives

\(\phi_1 ꕕ \phi_2\) is a sentence when \(\phi_1, \phi_2\) are two sentences and \(ꕕ\) is one of the following logic connectives \(\lor, \land, \Rightarrow, \Leftarrow, \Leftrightarrow\) (or using ascii characters: \(|, \&, =>, <=, <=>\) respectively). Logic connectives can be chained as customary.

Parenthesis

(\(\phi\)) is a sentence when \(\phi\) 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 these two forms, where \(v_1, .., v_n\) are variables and \(\phi\) is a sentence:

\[ \begin{align}\begin{aligned}\exists v_1 in typeOfV_1, .., v_n in typeOfV_n: \phi\\\forall v_1 in typeOfV_1, .., v_n in typeOfV_n: \phi\end{aligned}\end{align} \]

Alternatively, ascii characters can be used: ?, !, respectively. For example, !x in Int, y in Int: f(x,y)=f(y,x). A variable may only occur in the \(\phi\) sentence of a quantifier declaring that variable.

When quantifying a formula of type Symbol, the expression must contain a “guard” to prevent arity or type error. A guard is a predicate over Symbol that is defined by an enumeration in the same theory block. In the following example, symmetric must be defined by enumeration.

!`p in Symbol: symmetric(`p) => (!x, y : `p(x,y) => `p(y,x)).
“is (not) enumerated”

\(f(a,b)\ is\ enumerated\) and \(f(a,b)\ is\ not\ enumerated\) are sentences, where \(f\) is a function defined by an enumeration and applied to arguments \(a\) and \(b\). Its truth value reflects whether \((a,b)\) is enumerated in \(f\)’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\) and \(f(args)\ not\ in\ enum\) are sentences, where \(f\) is a function applied to arguments \(args\) and \(enum\) is an enumeration.

if .. then .. else ..

\(if\ t_1\ then\ t_2\ else\ t_3\) is a sentence when \(t_1\), \(t_2\) and \(t_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:

\[ \begin{align}\begin{aligned}&\forall v_1[typeOfV_1] .. v_n[typeOfV_n] : P(t_1, .., t_n) \leftarrow \phi.\\&\forall v_1[typeOfV_1] .. v_n[typeOfV_n] : F(t_1, .., t_n)=t \leftarrow \phi.\end{aligned}\end{align} \]

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 \(\phi\) is a formula that may contain these variables. \(P(t_1, t_2,.., t_n)\) is called the head of the rule and \(\phi\) the body. <- can be used instead of ‘\(\leftarrow\)’. 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 predicates and functions, by enumeration. If the names are omitted, the structure is named S, for vocabulary V.

A structure is a set of enumerations, having one of the following forms:

P := { (el_1^1, el_1^2,... el_1^n),
       (el_2^1, el_2^2,... el_2^n),
      ..
    }

P := {
el_1^1 el_1^2 ... el_1^n
el_2^1 el_2^2 ... el_2^n
}

F := { (el_1^1, el_1^2,... el_1^n) → el_1,
       (el_2^1, el_2^2,... el_2^n) -> el_2,
       ..
     } else el
Z := el

where \(P\) is a predicate of arity \(n\), \(F\) is a function of arity \(n\), and \(el_i^j\) are constructors or numeric literals.

The first statement enumerates the tuples of terms that make the predicate \(P\) true. Parentheses can be omitted when the arity is 1.

The second statement enumerates \(P\) using tab-delimited format: one row per line.

The third statement specifies the value \(el_i^n\) for the function \(F\) applied to the tuple of \(el_i^j\) arguments. The element after \(else\) specifies the function value for the non-enumerated tuples of arguments. This default value is optional; when omitted, the value of the function for the non-enumerated tuples, if any, is unspecified.

The fourth statement assigns the value \(el\) to the symbol \(Z\) (of arity 0).

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 program are available through variables of the same name.

The following functions are available:

model_check(theory, structure=None)

Returns string sat, unsat or unknown, depending on whether the theory has a model expanding the structure. theory and structure can be lists, in which case their elements are merged. The structure is optional.

For example, print(model_check(T, S)) will print sat if theory named T has a model expanding structure named S.

model_expand(theory, structure=None, max=10, complete=False)

Returns a list of models of the theory that are expansion of the structure. theory and structure can be lists, in which case their elements are merged. The structure is optional. The result is limited to max models (10 by default), or unlimited if max 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 named T expanding structure named S.

model_propagate(theory, structure=None)

Returns a list of assignments that are true in any expansion of the structure consistent with the theory. theory and structure 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 named S consistent with the theory named T.

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.

print(…)

Prints the arguments on stdout

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)

Creates an instance of Problem for the list of blocks, e.g., Problem(T,S)

add(self, block)

Adds a theory or structure block to the problem.

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 if max 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 if minimize is False) 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 than propagate().

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.

simplify(self)

Returns the problem with a simplified formula of the problem, by substituting terms and atoms by their values specified in a structure or obtained by propagation.

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.

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.

N-ary constructors

IDP-Z3 does not support n-ary constructors, e.g., RGB(Int, Int, Int). See IEP 06

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 an else part. (see also IEP 04)

Type

Type enumerations must be done in the vocabulary block (not in the structure block). 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. 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 := {c1, c2}
    type T := {1,2,3}
    type T := {1..3}
    // built-in types: 𝔹, ℤ, ℝ, Symbol        Bool, Int, Real, 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 ∈ T: p(x).                             !x in T: 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(1) is enumerated.
    p(5) 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 := {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() {
    print(model_check    (T,S))
    print(model_expand   (T,S))
    print(model_propagate(T,S))
}