Relax circular elimination check #7

New Issue

patrick · 2018-04-13T01:02:32+02:00

patrick commented

2018-04-13 01:02:32 +02:00

When using #show statements, there is a check to prevent circularly defined predicates from being eliminated when they are requested to be hidden.

The reason is that for a program

forall X (r(X) <-> p(X) and q(X))
forall X (p(X) <-> q(X))
forall X (q(X) <-> p(X))

just #showing r(X) and p(X) is possible by replacing all occurrences of the now hidden predicate q(X) by its definition p(X):

forall X (r(X) <-> p(X) and p(X))
forall X (p(X) <-> p(X))

This doesn’t work when attempting only to #show r(X). This is because p(X) has a circular definition and cannot be eliminated by substitution.

However, this check is too strict. If the program looked as follows:

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

then only #showing r(X) should be allowed. This is because no formula other than the definitions of p(X) and q(X) refer to hidden predicates, and both of these rules would be hidden anyway after eliminating p(X) and q(X). Hence, it’s valid to print the following output in this case:

forall X (r(X) <-> X in 1..5)

As of now, anthem fails in such cases, complaining about the seeming circular dependency.

When using `#show` statements, there is a check to prevent circularly defined predicates from being eliminated when they are requested to be hidden. The reason is that for a program forall X (r(X) <-> p(X) and q(X)) forall X (p(X) <-> q(X)) forall X (q(X) <-> p(X)) just `#show`ing `r(X)` and `p(X)` is possible by replacing all occurrences of the now hidden predicate `q(X)` by its definition `p(X)`: forall X (r(X) <-> p(X) and p(X)) forall X (p(X) <-> p(X)) This doesn’t work when attempting only to `#show` `r(X)`. This is because `p(X)` has a circular definition and cannot be eliminated by substitution. However, this check is too strict. If the program looked as follows: forall X (r(X) <-> X in 1..5) forall X (p(X) <-> q(X)) forall X (q(X) <-> p(X)) then only `#show`ing `r(X)` should be allowed. This is because no formula other than the definitions of `p(X)` and `q(X)` refer to hidden predicates, and both of these rules would be hidden anyway after eliminating `p(X)` and `q(X)`. Hence, it’s valid to print the following output in this case: forall X (r(X) <-> X in 1..5) As of now, anthem fails in such cases, complaining about the seeming circular dependency.

patrick self-assigned this 2018-04-13 01:02:32 +02:00

patrick added the

bug

label 2018-04-13 01:02:32 +02:00

patrick added this to the anthem 0.2.0 milestone 2018-04-23 00:23:07 +02:00

patrick removed this from the anthem 0.2.0 milestone 2019-01-13 16:43:29 +01:00

Sign in to join this conversation.