Detect integer variables and predicate parameters #2

New Issue

patrick · 2018-04-13T00:12:35+02:00

patrick commented

2018-04-13 00:12:35 +02:00

In order to apply simplifications that only apply to integer variables, these need to be detected first.

If a parameter of a predicate p/n is described by an integer variable (in all occurrences) in the definition of p/n, then this parameter is integer as well, denoted by

int(<predicate>/<arity>@<parameter index>)

Difficulties

Cyclic Dependencies

How to handle cases such as:

forall X (p(X) <-> X in 1..5 and q(X))
forall X (q(X) <-> X in 1..5 and p(X))

Whether p/1 and q/1 have integer parameters cannot be easily determined because of the cyclic dependency.

Placeholders

In cases such as:

forall X (p(X) <-> X in 1..5 and ext(X))

where ext is declared #external, we cannot conclude the domain of X.

Constants

When programs include constants (syntactically, 0-ary functions), we cannot assume them to be integer:

forall X (border(X) <-> X = 1 or X = n)

because n could be set to a noninteger value.

Comparisons

Let’s say that we have comparisons in our formula:

forall X (p(X) <-> X = 2 or X = 5)

Here, we can easily conclude that X is integer. In the following case, X is not integer:

forall X (p(X) <-> X = 2 or X = error)

However, with inequalities, this gets more complicated:

forall X (p(X) <-> X = 2 and X != error)

In this case, the inequality strictly doesn’t turn X into an integer variable. However, detecting such negations is complicated, because they might also occur at a higher level up the syntax tree.

Functions

Generally, functions can return any type of objects. Hence, it’s not safe to assume that X is an integer variable in cases like the following one:

forall X (p(X) <-> q(X) and X + f(X) < 5)

Comparisons

At first, it seems like comparisons of the form A < B imply that A and B are arithmetic expressions returning an integer.

However, this may not be true in some cases. Consider the following part of what could be a game description:

#external currentScore(1).
nextScore(X + 1) :- currentScore(X), X < 100.
nextScore(100) :- currentScore(X), X >= 100.

Let’s assume that currentScore(error) is set to handle situations where some illegal action was taken. Then, X would not be an integer variable, and integer simplifications would be incorrect to apply. However, the program is valid, because there would simply be no nextScore atom in the output in case currentScore/1 is not present with an integer argument.

In order to apply simplifications that only apply to integer variables, these need to be detected first. If a parameter of a predicate `p/n` is described by an integer variable (in all occurrences) in the definition of `p/n`, then this parameter is integer as well, denoted by int(<predicate>/<arity>@<parameter index>) ### Difficulties #### Cyclic Dependencies How to handle cases such as: forall X (p(X) <-> X in 1..5 and q(X)) forall X (q(X) <-> X in 1..5 and p(X)) Whether `p/1` and `q/1` have integer parameters cannot be easily determined because of the cyclic dependency. #### Placeholders In cases such as: forall X (p(X) <-> X in 1..5 and ext(X)) where `ext` is declared `#external`, we cannot conclude the domain of `X`. #### Constants When programs include constants (syntactically, 0-ary functions), we cannot assume them to be integer: forall X (border(X) <-> X = 1 or X = n) because `n` could be set to a noninteger value. #### Comparisons Let’s say that we have comparisons in our formula: forall X (p(X) <-> X = 2 or X = 5) Here, we can easily conclude that `X` is integer. In the following case, `X` is not integer: forall X (p(X) <-> X = 2 or X = error) However, with inequalities, this gets more complicated: forall X (p(X) <-> X = 2 and X != error) In this case, the inequality strictly doesn’t turn `X` into an integer variable. However, detecting such negations is complicated, because they might also occur at a higher level up the syntax tree. #### Functions Generally, functions can return any type of objects. Hence, it’s not safe to assume that `X` is an integer variable in cases like the following one: forall X (p(X) <-> q(X) and X + f(X) < 5) #### Comparisons At first, it seems like comparisons of the form `A < B` imply that `A` and `B` are arithmetic expressions returning an integer. However, this may not be true in some cases. Consider the following part of what could be a game description: #external currentScore(1). nextScore(X + 1) :- currentScore(X), X < 100. nextScore(100) :- currentScore(X), X >= 100. Let’s assume that `currentScore(error)` is set to handle situations where some illegal action was taken. Then, `X` would not be an integer variable, and integer simplifications would be incorrect to apply. However, the program is valid, because there would simply be no `nextScore` atom in the output in case `currentScore/1` is not present with an integer argument.

patrick added this to the anthem 0.1.9 milestone 2018-04-13 00:12:35 +02:00

patrick self-assigned this 2018-04-13 00:12:35 +02:00

patrick added the

enhancement

label 2018-04-13 00:12:35 +02:00

patrick changed title from ~~Detect integer variables and predicates~~ to Detect integer variables and predicate parameters

2018-04-13 14:05:34 +02:00

patrick commented

2018-04-21 17:14:51 +02:00

Implemented by hypothetically making variables noninteger and checking whether this leads to trivially true or false statements, from which it can be concluded that the variables must be integer.

patrick closed this issue

2018-04-21 17:14:51 +02:00

Sign in to join this conversation.