Group Abstract

Message Boards

WOLFRAM COMMUNITY

3.5K Views

5 Replies

2 Total Likes

View groups...

Follow this post

Share this post:

GROUPS:

Mathematics Wolfram Language

Can you please tell me if this is a bug in quantifiers?

patrikfrnka

Posted 8 years ago

Consider the following code: In[1]:= l1={3,3,3} Out[1]= {3,3,3} In[2]:= l2={1,2,3} Out[2]= {1,2,3} In[4]:= ForAll[x,MemberQ[l1,x],Exists[y,MemberQ[l2,y],x==y]] Out[4]= True In[3]:= Exists[z,MemberQ[l2,z],ForAll[u,MemberQ[l1,u],z==u]] Out[3]= False In[5]:= Exists[z,MemberQ[l2,z_],ForAll[u,MemberQ[l1,u],z==u]] Out[5]= True "WHY z HAVE TO BE SET TO PATTERN z_ TO GET RIGHT RESULT?" Attachments:

Consider the following code:

In[1]:= l1={3,3,3}
    Out[1]= {3,3,3}
    In[2]:= l2={1,2,3}
    Out[2]= {1,2,3}
    In[4]:= ForAll[x,MemberQ[l1,x],Exists[y,MemberQ[l2,y],x==y]]
    Out[4]= True
    In[3]:= Exists[z,MemberQ[l2,z],ForAll[u,MemberQ[l1,u],z==u]]
    Out[3]= False
    In[5]:= Exists[z,MemberQ[l2,z_],ForAll[u,MemberQ[l1,u],z==u]]
    Out[5]= True

"WHY z HAVE TO BE SET TO PATTERN z_ TO GET RIGHT RESULT?"

POSTED BY: patrikfrnka

5 Replies

Sort By:

Gianluca Gorni

Gianluca Gorni, University of Udine

Posted 8 years ago

`MemberQ` is probably a programming construct, and it is not suitable to logic manipulation. `MemberQ[{1},z]` evaluates immediately to `False` inside `Exists`: Exists[z, MemberQ[{1}, z]] This is a way around the problem: X = {3, 3, 3}; Y = {1, 2, 3}; ForAll[x, Or @@ Thread[x == X], Exists[y, Or @@ Thread[y == Y], x == y]] // Reduce Exists[z, Or @@ Thread[z == Y], ForAll[u, Or @@ Thread[u == X], z == u]] // Reduce

MemberQ is probably a programming construct, and it is not suitable to logic manipulation. MemberQ[{1},z] evaluates immediately to False inside Exists:

Exists[z, MemberQ[{1}, z]]

This is a way around the problem:

X = {3, 3, 3};
Y = {1, 2, 3};
ForAll[x, Or @@ Thread[x == X],
  Exists[y, Or @@ Thread[y == Y], x == y]] // Reduce
Exists[z, Or @@ Thread[z == Y],
  ForAll[u, Or @@ Thread[u == X], z == u]] // Reduce

POSTED BY: Gianluca Gorni

Daniel Lichtblau

Daniel Lichtblau, Wolfram Research

Posted 8 years ago

POSTED BY: Daniel Lichtblau

patrikfrnka

Posted 8 years ago

Hello Everyone! Quantifiers are here again. Finally GOOD solution is here to share, so see notebook for full details :) Shortly: xE[x_, a_, c_] := Block[{i, ce}, For[i = 1, i <= Length[a], i++,(main result) ce = With[{x = a[[i]]}, c]; If[ce, Return[ce], , Print["uuups!!!"]]];(Print["xE False"];) Return[ce]] SetAttributes[xE, HoldAll] patrikfrnka@seznam.cz Attachments:

Hello Everyone! Quantifiers are here again. Finally GOOD solution is here to share, so see notebook for full details :) Shortly:

xE[x_, a_, c_] := 
 Block[{i, ce}, For[i = 1, i <= Length[a], i++,(*main result*)
   ce = With[{x = a[[i]]}, c];
   If[ce, Return[ce], , Print["uuups!!!"]]];(*Print["xE False"];*)
  Return[ce]]

SetAttributes[xE, HoldAll]

patrikfrnka@seznam.cz

POSTED BY: patrikfrnka

patrikfrnka

Posted 8 years ago

POSTED BY: patrikfrnka

patrikfrnka

Posted 8 years ago

Thank you very much for YOUR TIME! I've found documentation about evaluation, so... maybe I'll help myself soon. I'm trying to write elegantly DFA minimalization in Mathematica. There I need some construction to make iteration on set of states: s[i+1]:=s[i] u { p e States\| E q e States \| E a e Sigma \| d[p][a]=q } (HOPE YOU UNDERSTAND this "PSEUDOCODE" - d is transition function) I've attached a sample how far I get yet...:) Thanks for your OPTIONAL suggestions PF Attachments:

POSTED BY: patrikfrnka

Reply to this discussion

Reply Preview

Attachments

Remove Add a file to this post

Follow this discussion

or Discard

Feedback