Dual operator design

[bvssvni]

A dual operator might be used on 1-avatars in rules:

(X, Z) :- (X, Y), (Y, Z), (X*, X).

This rule is the same as the two following rules:

(X, Z) :- (X, Y), (Y, Z), (C'(X), X).
(C'(X), Z) :- (C'(X), Y), (Y, Z), (X, C'(X)).

The dual operator is possible because X* and X occur twice in the rules.

The 1-avatar is inferred from the possible cases:

X          X*            1-avatar
------------------------------------
a          b'(a)         b
b'(a)      a

b'(a)      c'(b'(a))     c
c'(b'(a))  b'(a)

a          c'(b'(a))     c'(b'(..))
c'(b'(a))  a

a          a             ()

The self duality is excluded by usign + instead of *, e.g. X+.