[SMT-LIB] Multiarity XOR, IFF

[Sava Krstic]

XOR is addition modulo two. The set {0,1} has the algebraic structure of 
a _field_, where XOR is the addition and AND is the multiplication. This 
pair of operations satisfies all algebraic laws that PLUS and TIMES of 
rationals (or reals) satisfy. Multiarity XOR is commonly seen in 
cryptography (check, for example, "secret sharing" on wikipedia) and 
certainly at other places in computer science, so I would suggest that 
SMT-LIB allow it.

The IFF seems problematic. Algebraically, it's just as "good" as 
XOR---these are the only abelian group operations on {0,1}---but has 
anyone ever seen expressions like "IFF a b c" or "a IFF b IFF c" to mean 
  "(a IFF b) IFF c"?  On the other hand, chains like "a IFF b IFF c" are 
commonly seen with the meaning that a, b, c are all equivalent, in 
complete analogy with expressions chains like "a = b = c". I would 
suggest that multiarity IFF either be disallowed, or allowed (together 
with multiarity equality!) with the "all equal" meaning.

Sava

Clark Barrett wrote:
>>>(Personally,
>>>I'm not sure it really makes sense to have multiarity xor and iff at
>>>all).
>>>
>>
>>Why not?  Would you then say that it does not make sense to have  
>>multiarity AND and OR connectives either? If not, what would be the  
>>difference? The current standard treats them all the same by virtue  
>>of their associativity.
> 
> 
> I have no problem with multiarity AND and OR.  These come up in real
> applications and are (I believe) well-understood.  The reason I am less
> comfortable with multiarity XOR and IFF is that I've never seen them come
> up in practice and (as evidenced by this discussion) I believe there is little
> or no intuition behind their current meanings.
> 
> That said, I think that changing the semantics would be even more confusing: if
> (iff a b c) really means (and (iff a b) (iff b c)) then I'd rather see it
> spelled out than hidden behind a multiarity iff.
> 
> To summarize, here is what I would suggest (in order of preference):
> 
> 1. Restrict XOR and IFF to be binary operators
> 2. Leave the semantics as they are but add some clarification in the standard
> 3. Change the semantics
> 
> -Clark
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>