Project

Namespaces

Public Vars

polix.negate

Policy negation through AST transformation.

Provides pure transformation of policy ASTs to their logical negations. Negation enables computing what would contradict a policy, useful for generating counter-examples and reasoning about policy violations.

Constraint-level negation is handled by polix.operators/negate-constraint. This namespace handles policy-level (AST) transformations:

  • De Morgan’s laws for :and / :or
  • Quantifier swapping (:forall ↔ :exists)
  • Double negation elimination
  • Delegation to operator negation for comparisons

Non-invertible expressions produce ::complex marker nodes.

complex-marker

(complex-marker original-node reason)

Creates a complex marker node for non-invertible expressions.

Complex markers indicate that the expression cannot be meaningfully negated and should be treated as opaque during further processing.

complex?

(complex? node)

Returns true if the node is a complex marker.

double-negate

(double-negate ast)

Applies double negation to an AST.

Useful for testing that negation is self-inverse. Note that double negation may not produce an identical AST due to simplifications like :not elimination, but should be logically equivalent.

has-complex?

(has-complex? ast)

Returns true if the AST contains any complex (non-invertible) markers.

Traverses the entire AST tree to check for complex nodes.

negate

(negate node)

Negates an AST node, returning the negated AST.

Recursively transforms the AST according to negation rules:

  • Function calls: De Morgan for :and/:or, unwrap :not, delegate operators
  • Quantifiers: swap :forall ↔ :exists with negated body
  • Literals/accessors: cannot be negated, produce complex markers

Returns a new AST node representing the negation.

Examples (showing logical equivalence, not exact AST structure):

;; Comparison operators
(negate (parse [:= :doc/role "admin"]))
;; equivalent to: [:!= :doc/role "admin"]

;; De Morgan's laws
(negate (parse [:and [:= :doc/x 1] [:= :doc/y 2]]))
;; equivalent to: [:or [:!= :doc/x 1] [:!= :doc/y 2]]

;; Quantifier swapping
(negate (parse [:forall [u :doc/users] [:= :u/active true]]))
;; equivalent to: [:exists [u :doc/users] [:!= :u/active true]]