[SMT-LIB] Multiarity XOR, IFF

[Cesare Tinelli]

Hi Jim,

On Nov 7, 2007, at 9:36 AM, Grundy, Jim D wrote:

> 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.
>
The standard *does* allow a multiarity = (with arity starting at 2).
See, e.g., pages 36 and 37 of the standard.
The semantics of (= a b c) is meant to be (and (= a b) (= b c)), as  
one would expect.
But that too, regrettably, is not explicitly spelled out. The reason  
is simply that, as in the XOR and IFF case, it was supposed to be  
defined in Subsection 6.1 of the document, which is however still  
missing.
I take the blame and apologize for not having completed that section  
yet.
It is in my to-do list. I guess it's really time to increase its  
priority :)


Cesare


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