[SMT-LIB] Multiarity XOR, IFF

[Grundy, Jim D]

Well - I'm not a huge fan of the multiarity operators, but at the end of
the day
it doesn't really matter, so long as the standard makes clear what they
mean, and
it does (had I bothered to read the right part of it).

I think we figured (iff a b c) was being allowed because it can save
significant space
in the input over (iff a b) and (iff b c) when b is large - but you can
always get
around than by using a let expression.

I would say that if you were going to alow multiarity iff to mean a
conjunction of iffs then if would make as much sence to allow multiarity
= meaning a conjunction of =s, which the standard doesn't currently
allow.

One can debate about what the standard should have been, but since it is
reasonable the way it is I don't see a compelling case for change.

All the best

Jim  

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On
Behalf Of Sava Krstic
Sent: Wednesday, November 07, 2007 9:18 AM
To: Clark Barrett
Cc: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] Multiarity XOR, IFF

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
> 
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib