((a&&b)||c)==((a||c)&&(b||c))
Steven T. Hatton
((a \[And] b) \[Or] c) == ((a \[Or] c) \[And] (b \[Or] c))
This little function shows that the lhs and rhs have the same truth tables,
and are therefore equivalent:
TruthTable[s_, argc_] := Module[
{tt = Tuples[{True, False}, argc]},
{#, s @@ #} & /@ tt // TableForm
]
--
The Mathematica Wiki: http://www.mathematica-users.org/
Math for Comp Sci http://www.ifi.unizh.ch/math/bmwcs/master.html
Math for the WWW: http://www.w3.org/Math/
Peter Pein
> Why does Mathematica not determine that the following is true?
>
> ((a \[And] b) \[Or] c) == ((a \[Or] c) \[And] (b \[Or] c))
>
> This little function shows that the lhs and rhs have the same truth tables,
> and are therefore equivalent:
>
> TruthTable[s_, argc_] := Module[
> {tt = Tuples[{True, False}, argc]},
> {#, s @@ #} & /@ tt // TableForm
> ]
>
In[1]:= expr = ((a && b) || c) == ((a || c) && (b || c))
Out[1]= ((a && b) || c) == ((a || c) && (b || c))
In[2]:= LogicalExpand /@ expr
Out[2]= True
Andrzej Kozlowski
On 9 Nov 2005, at 17:45, Steven T. Hatton wrote:
> Why does Mathematica not determine that the following is true?
>
> ((a \[And] b) \[Or] c) == ((a \[Or] c) \[And] (b \[Or] c))
>
> This little function shows that the lhs and rhs have the same
> truth tables,
> and are therefore equivalent:
>
> TruthTable[s_, argc_] := Module[
> {tt = Tuples[{True, False}, argc]},
> {#, s @@ #} & /@ tt // TableForm
> ]
>
> --
> The Mathematica Wiki: http://www.mathematica-users.org/
> Math for Comp Sci http://www.ifi.unizh.ch/math/bmwcs/master.html
> Math for the WWW: http://www.w3.org/Math/
>
Because, (as I tried to explain in a reply to a recent posting of
yours) this is not the way == is used in Mathematica. The correct way
to show this is:
Implies[(a ∨ c) ∧ (b ∨ c),(a ∧ b) ∨ c]//FullSimplify
True
Implies[(a ∧ b) ∨ c,(a ∨ c) ∧ (b ∨ c)]//FullSimplify
True
Andrzej Kozlowski
Andrzej Kozlowski
Actually, there is at least one more way to do this, which you may
like better:
LogicalExpand[(a ∧ b) ∨ c]==LogicalExpand[(a ∨ c) ∧ (b ∨ c)]
True
But this one is actually less reliable.
Andrzej Kozlowski
Steven T. Hatton
> But Mathematica does:
>
> In[1]:= expr = ((a && b) || c) == ((a || c) && (b || c))
> Out[1]= ((a && b) || c) == ((a || c) && (b || c))
> In[2]:= LogicalExpand /@ expr
> Out[2]= True
However:
In[1]:= expr = ((a && b) || c) == (a || c) && (b || c);
LogicalExpand /@ expr
Out[1]:= ((a && b) || c) == (a || c) && (b || c)
I believe the reason Mathematica is having a hard time with this is because
the rules of combining logical operators cannot be expressed in terms of a
strict precedence hierarchy. I particular the distributive laws:
(P && (Q || R)) <=> ((P && Q) || (P && R))
(P || (Q && R)) <=> ((P || Q) && (P || R))
Steven T. Hatton
> On 9 Nov 2005, at 17:45, Steven T. Hatton wrote:
>
>> Why does Mathematica not determine that the following is true?
>>
>> ((a \[And] b) \[Or] c) == ((a \[Or] c) \[And] (b \[Or] c))
> Because, (as I tried to explain in a reply to a recent posting of
> yours) this is not the way == is used in Mathematica. The correct way
> to show this is:
The rules of logic are very tricky. For example:
Tautology <=> True
P && Tautology <=> P
P || Tautology <=> Tautology
!Tautology <=> Contradiction
Daniel Lichtblau
> Why does Mathematica not determine that the following is true?
>
> ((a \[And] b) \[Or] c) == ((a \[Or] c) \[And] (b \[Or] c))
>
> and are therefore equivalent:
>
> TruthTable[s_, argc_] := Module[
> {tt = Tuples[{True, False}, argc]},
> {#, s @@ #} & /@ tt // TableForm
> ]
>
Equal does not do logical manipulations on its operands. Nor will
LogicalExpand automatically thread over Equal. Probably a better way to
implement your biconditional (mentioned in another MathGroup post today,
with regard to this same example) would be
biconditional[p_, q_] := Implies[p,q] && Implies[q,p]
(suggested by Andrzej Kozlowski, I think)
or
biconditional[p_, q_] := Not[Xor[p,q]]
or logical expand in advance and use
biconditional[p_, q_] := (p&&q) || (!p&&!q)
These remain in the realm of logical operations rather than
"arithmetic-like" operators such as Equal. Depending on your purpose
this might be preferable. The fact that you use a truth table above
indicates to me that you probably would be better served by strictly
logical operations.
Daniel Lichtblau
Wolfram Research
Richard Fateman
are the same, is that they are in some senses different.
These look like logical statements and as such they look like they
are logically identical, but these are actually
programs with short-circuit evaluation.
Consider
c[] := (Print[C_called]; True)
a[] := (Print[A_called]; False)
b[] := (Print[B_called]; True)
(a[] && b[]) || c[]
(a[] || c[]) && (b[] || c[])
They are different PROGRAMS.
Similar arguments could be made for arithmetic, but usually
they are not used for program control. If they are used inside
programs, they should not be simplified.
How about
p[]*p[].... which is simplified to p[]^2.
What if p[]:=(count++; 1)
How many times does count get incremented?
So if p[]*p[] appears in the body of a program, it should
not be simplified.
(another example: Simplify [ something_simplifies_to_zero[]*hairy_mess[] ]
should we never bother to evaluate hairy_mess[] ???
Mathematica does evaluate it, so far as I can tell. Is this correct?
Unclear. if hairy_mess came out Infinity, the result would be indeterminate,
I suppose. )
Steven T. Hatton
want to volunteer his address to the spam harvesters.]
On Wednesday 09 November 2005 11:02 am, Daniel Lichtblau wrote:
> Steven T. Hatton wrote:
> > Why does Mathematica not determine that the following is true?
> >
> > ((a \[And] b) \[Or] c) == ((a \[Or] c) \[And] (b \[Or] c))
> >
> > This little function shows that the lhs and rhs have the same truth
> > tables, and are therefore equivalent:
> >
> > TruthTable[s_, argc_] := Module[
> > {tt = Tuples[{True, False}, argc]},
> > {#, s @@ #} & /@ tt // TableForm
> > ]
>
> Equal does not do logical manipulations on its operands.
That's part of what I'm trying to understand. Mathamatica AFAIK takes
expressions and transforms them into the simplest form possible, and then
does pattern patching. I suspect that it's not really "Equal" per se, that
does not do logical manipulations, but Mathematica in general. The rules for
manipulating logical expressions are not amenable to the precedence hierarchy
found in the arithmetic of real numbers. That is * distributes over +, but +
does not distribute over *; OTOH && distributes over ||, _and_ || distributes
over &&.
> Nor will
> LogicalExpand automatically thread over Equal. Probably a better way to
> implement your biconditional (mentioned in another MathGroup post today,
> with regard to this same example) would be
>
> biconditional[p_, q_] := Implies[p,q] && Implies[q,p]
> (suggested by Andrzej Kozlowski, I think)
>
> or
>
> biconditional[p_, q_] := Not[Xor[p,q]]
>
> or logical expand in advance and use
>
> biconditional[p_, q_] := (p&&q) || (!p&&!q)
>
> These remain in the realm of logical operations rather than
> "arithmetic-like" operators such as Equal. Depending on your purpose
> this might be preferable. The fact that you use a truth table above
> indicates to me that you probably would be better served by strictly
> logical operations.
I believe I will, in the end, use Implies, as Andrzej suggested, but I haven't
solved another part of the problem which seems more fundamental. I need a
way to persuade a binary operator to bind more loosely than the logical
operators. I just realized I could probably use the precedence of Implies as
the SyntaxForm argument, if I could get that to work.
To your knowledge, does that feature of the Utilities`Notation` package work?
The documentation discussing SyntaxForm seems to have some lacunae. Perhaps
I'm just not reading closely enough.
This is an example of what I've attempted:
In[2]:=
<<Utilities`Notation`
In[3]:=
InfixNotation[\[DoubleLeftRightArrow],Biconditional,
SyntaxForm\[Rule] "\[Implies]"]
In[4]:=
(a\[And]b)\[Or]c\[DoubleLeftRightArrow](a\[Or]c)\[And](b\[Or]c)
Out[4]=
(a&&b)||(c\[DoubleLeftRightArrow](a||c)&&(b||c))
In[5]:=
%//FullForm
Out[5]//FullForm=
Or[And[a,b],And[Biconditional[c,Or[a,c]],Or[b,c]]]
Perhaps there is some way to use the TagBox[__,SyntaxForm->"=>"] explicitly?
Steven
Steven T. Hatton
> A good reason for Mathematica to fail to show that these
> are the same, is that they are in some senses different.
>
>
> These look like logical statements and as such they look like they
> are logically identical, but these are actually
> programs with short-circuit evaluation.
>
>
> Consider
> c[] := (Print[C_called]; True)
> a[] := (Print[A_called]; False)
> b[] := (Print[B_called]; True)
> (a[] && b[]) || c[]
> (a[] || c[]) && (b[] || c[])
>
> They are different PROGRAMS.
Good observation. There should, however, be some way to tell Mathematica to
treat them as traditional symbolic logic statements. I don't believe that
LogicExpand will do that for me. I'm not sure what happens with Implies,
but my observation is that it does not handle all cases.
Daniel Lichtblau
> Peter Pein wrote:
>
>
>>But Mathematica does:
>>
>>In[1]:= expr = ((a && b) || c) == ((a || c) && (b || c))
>>Out[1]= ((a && b) || c) == ((a || c) && (b || c))
>>In[2]:= LogicalExpand /@ expr
>>Out[2]= True
>
>
>
> In[1]:= expr = ((a && b) || c) == (a || c) && (b || c);
> LogicalExpand /@ expr
> Out[1]:= ((a && b) || c) == (a || c) && (b || c)
>
> I believe the reason Mathematica is having a hard time with this
I do not know what you mean by "having a hard time". If you mean it
fails to alter the "right hand side", that may be due to operator
precedence not being quite as (I think) you had intended.
In[5]:= FullForm[expr]
Out[5]//FullForm= And[Equal[Or[And[a, b], c], Or[a, c]], Or[b, c]]
The head is And, and the right hand side is Or[b,c]. Your Equal is
inside the left hand side. Equal has higher precedence than the logical
operators And and Or, but lower than the arithmetic operators Plus and
Times. One reason may be an artifact of our own use of logical operators
and LogicalExpand. Specifically, Equal is used in equation solving, and
equation systems often need to be put into a convenient form for further
processing (Or of Ands. More on this below.)
To do what I think you had in mind, make the grouping explicit.
Out[6]= ((a && b) || c) == ((a || c) && (b || c))
In[7]:= Map[LogicalExpand, expr]
Out[7]= True
> is because
> the rules of combining logical operators cannot be expressed in terms of a
> strict precedence hierarchy. I particular the distributive laws:
>
> (P && (Q || R)) <=> ((P && Q) || (P && R))
> (P || (Q && R)) <=> ((P || Q) && (P || R))
These dual distributive laws do not preclude the existence of canonical
forms with a strict precedence between And and Or. Disjunctive Normal
Form (DNF) and Conjunctive Normal Form (CNF) come close to being
canonical. Application of the Quine-McCluskey algorithm to DNF can
provide a canonical form. LogicalExpand does not do this, but what it
gives is often reasonably close.
If instead you work with Not, And, and Xor, then you have an isomorphism
to a polynomial boolean algebra (work modulo 2, with all indeterminates
satisfying x^2==x). In this case the usual polynomial simplification
will be canonical. One reason one might wish to avoid going in this
direction is that logical expressions are often formed naturally from
Not, And, and Or. Conversion to Xor has the unfortunate effect of
blowing up the size.
Daniel Lichtblau
Wolfram Research
Steven T. Hatton
> Steven T. Hatton wrote:
> > I believe the reason Mathematica is having a hard time with this
>
> I do not know what you mean by "having a hard time". If you mean it
> fails to alter the "right hand side", that may be due to operator
> precedence not being quite as (I think) you had intended.
>
> In[5]:= FullForm[expr]
> Out[5]//FullForm= And[Equal[Or[And[a, b], c], Or[a, c]], Or[b, c]]
> The head is And, and the right hand side is Or[b,c]. Your Equal is
> inside the left hand side. Equal has higher precedence than the logical
> operators And and Or, but lower than the arithmetic operators Plus and
> Times.
No. I mean that you can build two distinct parse trees which when joined with
a biconditional connective evaluate to True. In order to compare statements
of symbolic logic, the program using parse trees would have to be able to
backtrack, and try alternative trees for each side of the expression until it
evaluated to a definite value, or had conclusively exhausted all
laternatives.
> One reason may be an artifact of our own use of logical operators
> and LogicalExpand. Specifically, Equal is used in equation solving, and
> equation systems often need to be put into a convenient form for further
> processing (Or of Ands. More on this below.)
I understand why equals groups as it does. It is being used in the sense of
programming, not in the sense of a biconditional. I believe Richard Fateman
explained, in part, why this is happening.
> To do what I think you had in mind, make the grouping explicit.
>
> Out[6]= ((a && b) || c) == ((a || c) && (b || c))
>
> In[7]:= Map[LogicalExpand, expr]
> Out[7]= True
>
> > is because
> > the rules of combining logical operators cannot be expressed in terms of
> > a strict precedence hierarchy. I particular the distributive laws:
> >
> > (P && (Q || R)) <=> ((P && Q) || (P && R))
> > (P || (Q && R)) <=> ((P || Q) && (P || R))
>
> These dual distributive laws do not preclude the existence of canonical
> forms with a strict precedence between And and Or. Disjunctive Normal
> Form (DNF) and Conjunctive Normal Form (CNF) come close to being
> canonical. Application of the Quine-McCluskey algorithm to DNF can
> provide a canonical form. LogicalExpand does not do this, but what it
> gives is often reasonably close.
I guess I never got around to posting my question about Karnaugh maps. But I
will now conclude that Mathematica does not have any built-in capability for
evaluating Karnaugh maps.
> If instead you work with Not, And, and Xor, then you have an isomorphism
> to a polynomial boolean algebra (work modulo 2, with all indeterminates
> satisfying x^2==x). In this case the usual polynomial simplification
> will be canonical. One reason one might wish to avoid going in this
> direction is that logical expressions are often formed naturally from
> Not, And, and Or. Conversion to Xor has the unfortunate effect of
> blowing up the size.
I found a notebook on the WRI site implementing some kind of logical
operations using ring theory, but I can't say I've studied it. While I was
poking around, I did find several sources which look helpful. Thanks for
reminding me about Quine. It's been a very long time since I thought about
this stuff in depth.
Steven
John Doty
> On Wednesday 09 November 2005 11:02 am, Daniel Lichtblau wrote:
>>Equal does not do logical manipulations on its operands.
>
>
> That's part of what I'm trying to understand. Mathamatica AFAIK takes
> expressions and transforms them into the simplest form possible, and then
> does pattern patching.
No, that's not what it does. There are a few transformations it does
automatically, but they don't add up to anything like a transformation
to "simplest form possible". There are expensive heuristic procedures,
Simplify[] and FullSimplify[] that attempt this, but they are not
invoked automatically and also cannot be guaranteed to find the
"simplest form possible".
Ordinary algebra in Mathematica defies most of your expectations also:
In[1]:= (a + 1)^2 == a^2 + 2*a + 1
Out[1]= (1 + a)^2 == 1 + 2*a + a^2
In[2]:= Expand[%]
Out[2]= (1 + a)^2 == 1 + 2*a + a^2
In[3]:= Simplify[%]
Out[3]= True
The main difference is that Simplify[] won't apply LogicalExpand[]
automatically. I suppose this would be hazardous if some symbols didn't
represent booleans. However:
In[10]:= Simplify[((a && b) || c) == ((a || c) && (b || c)),
TransformationFunctions -> {Automatic, LogicalExpand}]
Out[10]= True
-jpd
Steven T. Hatton
> Steven T. Hatton wrote:
>
>> On Wednesday 09 November 2005 11:02 am, Daniel Lichtblau wrote:
>
>>>Equal does not do logical manipulations on its operands.
>>
>>
>> That's part of what I'm trying to understand. Mathamatica AFAIK takes
>> expressions and transforms them into the simplest form possible, and then
>> does pattern patching.
>
> No, that's not what it does. There are a few transformations it does
> automatically, but they don't add up to anything like a transformation
> to "simplest form possible".
I should have said "most specific form available". That is, a symbol has
downvalues, and upvalues associated with it. These are listed in
descending order of specificity according to some mechanism for determining
specificity which I do not understand. The user can override this ordering
and assert the order of transformation rules if desired. I acknowledge
that specificity and simplicity are not necessarily the same thing.
> The main difference is that Simplify[] won't apply LogicalExpand[]
> automatically. I suppose this would be hazardous if some symbols didn't
> represent booleans. However:
>
> In[10]:= Simplify[((a && b) || c) == ((a || c) && (b || c)),
> TransformationFunctions -> {Automatic, LogicalExpand}]
>
> Out[10]= True
>
> -jpd
That looks useful, but following what Daniel Lichtblau posted, it looks like
LogicalExpand isn't the whole answer either. I believe I need a function
that performs Quine-McCluskey minimization in order to get a
'deterministic' biconditional.