You can subscribe to this list here.
2003 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}
(1) 
_{Nov}

_{Dec}
(2) 

2004 
_{Jan}
(2) 
_{Feb}
(15) 
_{Mar}
(10) 
_{Apr}
(1) 
_{May}
(1) 
_{Jun}
(4) 
_{Jul}
(2) 
_{Aug}
(3) 
_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}
(3) 
2005 
_{Jan}
(3) 
_{Feb}
(17) 
_{Mar}
(6) 
_{Apr}
(13) 
_{May}
(17) 
_{Jun}
(53) 
_{Jul}
(36) 
_{Aug}
(29) 
_{Sep}
(17) 
_{Oct}
(21) 
_{Nov}
(37) 
_{Dec}
(25) 
2006 
_{Jan}

_{Feb}
(29) 
_{Mar}
(85) 
_{Apr}
(27) 
_{May}
(25) 
_{Jun}
(57) 
_{Jul}
(3) 
_{Aug}
(8) 
_{Sep}
(24) 
_{Oct}
(43) 
_{Nov}
(22) 
_{Dec}
(10) 
2007 
_{Jan}
(29) 
_{Feb}
(38) 
_{Mar}
(11) 
_{Apr}
(29) 
_{May}
(16) 
_{Jun}
(1) 
_{Jul}
(20) 
_{Aug}
(25) 
_{Sep}
(6) 
_{Oct}
(25) 
_{Nov}
(16) 
_{Dec}
(14) 
2008 
_{Jan}
(18) 
_{Feb}
(12) 
_{Mar}
(3) 
_{Apr}
(1) 
_{May}
(23) 
_{Jun}
(3) 
_{Jul}
(7) 
_{Aug}

_{Sep}
(16) 
_{Oct}
(27) 
_{Nov}
(16) 
_{Dec}
(7) 
2009 
_{Jan}
(1) 
_{Feb}
(12) 
_{Mar}

_{Apr}
(16) 
_{May}
(2) 
_{Jun}
(4) 
_{Jul}

_{Aug}
(4) 
_{Sep}
(7) 
_{Oct}
(12) 
_{Nov}
(8) 
_{Dec}

2010 
_{Jan}

_{Feb}

_{Mar}
(2) 
_{Apr}

_{May}

_{Jun}
(8) 
_{Jul}

_{Aug}
(11) 
_{Sep}

_{Oct}
(1) 
_{Nov}

_{Dec}
(1) 
2011 
_{Jan}
(14) 
_{Feb}
(20) 
_{Mar}
(3) 
_{Apr}
(1) 
_{May}
(1) 
_{Jun}
(23) 
_{Jul}
(1) 
_{Aug}
(3) 
_{Sep}
(5) 
_{Oct}
(19) 
_{Nov}
(1) 
_{Dec}
(5) 
2012 
_{Jan}
(19) 
_{Feb}
(4) 
_{Mar}

_{Apr}
(1) 
_{May}
(2) 
_{Jun}
(7) 
_{Jul}
(33) 
_{Aug}
(3) 
_{Sep}
(3) 
_{Oct}

_{Nov}

_{Dec}

2013 
_{Jan}

_{Feb}

_{Mar}
(3) 
_{Apr}
(48) 
_{May}
(1) 
_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

2014 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 





1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21
(1) 
22
(4) 
23

24

25

26

27

28

29

30


From: Tim Miller <tmiller@un...>  20110922 22:53:46

Hi Leo, That is definitely a violation of the standard, which allows only refnames. However, the parser is written as follows: inner_term:it LSQUARE expressionList:el RSQUARE:rsquare {: RESULT = factory_.createRefExpr(name(it), el, Boolean.FALSE, Boolean.TRUE); addLocAnn(RESULT, getLocation(it, rsquare)); :} This means that the grammar will allow the following: (A \cup B)[C] = A \cup B The CZT parser will report an error that a refname is expected for the generic instantiation when it calls name(it), and tries to cast the expression to a name. However, if this is for one of the dialects, you can easily add a new type of term to that dialect's schema, and then change the code body to create one of these terms. Tim On 22/09/11 18:39, Leo Freitas wrote: > Hi Tim, > > I am confused about the role of the "explicit" parameter in RefExpr. My understanding is that it is true when the user suplies the generics, and false otherwise. > That is because after type checking the ZExprList will contain (possibly nonmaximal) generics which the user don't want explicitly given on the terms. > > Is that right? Assuming it is, what about proofs / conjectures involving nonmaximal generics? Ex: > > \begin{theorem}{lNonMaxCup}[X] > \vdash? \forall C: \power~X @ \forall A, B: \power~C @ (\_ \cup \_)[C] (A,B) =A \cup B > \end{theorem} > > \begin{theorem}{catGen}[X] > \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ (\_\cat\_)[A] (s, t) = s \cat t > \end{theorem} > > In ZEves, these theorems could be written as > > \begin{theorem}{lNonMaxCup}[X] > \vdash? \forall C: \power~X @ \forall A, B: \power~C @ A \cup[C] B = A \cup B > \end{theorem} > > \begin{theorem}{catGen}[X] > \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ s \cat[A] t = s \cat t > \end{theorem} > > When the expressions are large, it's rather ugly to need to write the whole thing with mixfix false :(.... > > So the question is, is there a way to have explicit generics mixfix=true appl expr or ref expr? > That is crucial, otherwise, translating legacy proofs or indeed doing new proofs (e.g., ZEves > throws back at you nonmaximal or maximal generics in places)..... :( .... any ideas? > > Best, > Leo 
From: Leo Freitas <leo.freitas@ne...>  20110922 08:41:42

Hi Tim, I am confused about the role of the "explicit" parameter in RefExpr. My understanding is that it is true when the user suplies the generics, and false otherwise. That is because after type checking the ZExprList will contain (possibly nonmaximal) generics which the user don't want explicitly given on the terms. Is that right? Assuming it is, what about proofs / conjectures involving nonmaximal generics? Ex: \begin{theorem}{lNonMaxCup}[X] \vdash? \forall C: \power~X @ \forall A, B: \power~C @ (\_ \cup \_)[C] (A,B) =A \cup B \end{theorem} \begin{theorem}{catGen}[X] \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ (\_\cat\_)[A] (s, t) = s \cat t \end{theorem} In ZEves, these theorems could be written as \begin{theorem}{lNonMaxCup}[X] \vdash? \forall C: \power~X @ \forall A, B: \power~C @ A \cup[C] B = A \cup B \end{theorem} \begin{theorem}{catGen}[X] \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ s \cat[A] t = s \cat t \end{theorem} When the expressions are large, it's rather ugly to need to write the whole thing with mixfix false :(.... So the question is, is there a way to have explicit generics mixfix=true appl expr or ref expr? That is crucial, otherwise, translating legacy proofs or indeed doing new proofs (e.g., ZEves throws back at you nonmaximal or maximal generics in places)..... :( .... any ideas? Best, Leo 
From: Leo Freitas <leo.freitas@ne...>  20110922 06:03:24

Hi Tim, Thank you for this. At first, I didn't expect it to be a type error: it passed through both CZT, ZEves, and fuzz. And working out the types as you did is sensible, yes. I think my confusion came because of the (abstracted) example that I tried to create: \begin{gendef}[X,Y] w : Y \fun X \end{gendef} \begin{theorem}{postfixGen3}[X,Y] \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y] \end{theorem} This one works. But this one doesn't \begin{theorem}{postfixGen2}[X,Y] \vdash? \forall z: X \fun Y; w: Y \fun X @ z = w (\_~\inv)[X,Y] \end{theorem} And the reason I guess is because Y is fixed in the second for what in the first case it varies (e.g., first Y generic is not the same as second). Z is a lovely language for describing abstract thinking concisely. My goodness it's complicated to build tools for! Thanks, Leo On 22 Sep 2011, at 02:48, Tim Miller wrote: > On 21/09/11 19:05, Leo Freitas wrote: >> c) PUZZLE >> >> \begin{gendef}[X,Y] >> w : Y \fun X >> \end{gendef} >> >> \begin{theorem}{postfixGen3}[X,Y] >> \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y] >> \end{theorem} >> >> ApplExpr(LHS="w", RHS="_\inv[X,Y]", MF=false) >> >> (e.g., mistakenly we forgot to put \inv on the LHS, yet no error is raised!) >> >> Shouldn't we have an error here either when applying w to inv or when comparing it to z? >> > Do you mean a type error? I don't think so. If we consider the types, we > have (substituting in unique generic parameters to avoid confusion): > > \_ \inv: P (P(A x B) x P(B x A)) % (A x B) \fun (B x A) > w : P(C x D) > z : P(E x F) > > The expression w (\_~\inv)[E,F] is a function application. The type of > (\_ \inv)[E,F] is P (P(E x F) x P(F x E))) from the explicit > instantiation. Therefore, the type of the refexpr "w" is inferred as > P(P(E x F) x P(F x E) x Var), where C is instantiated by P(P(E x F) x > P(F x E)) and D is not instantiated (yet), so is given a variable type > Var. The equality z = w(\_\inv)[E,F] allows us to infer that Var = F, so > the type of w is fully instantiated. > > Confused? :) > > Tim > >  > All the data continuously generated in your IT infrastructure contains a > definitive record of customers, application performance, security > threats, fraudulent activity and more. Splunk takes this data and makes > sense of it. Business sense. IT sense. Common sense. > http://p.sf.net/sfu/splunkd2dcopy1 > _______________________________________________ > CZTDevel mailing list > CZTDevel@... > https://lists.sourceforge.net/lists/listinfo/cztdevel 
From: Tim Miller <tmiller@un...>  20110922 01:48:27

On 21/09/11 19:05, Leo Freitas wrote: > c) PUZZLE > > \begin{gendef}[X,Y] > w : Y \fun X > \end{gendef} > > \begin{theorem}{postfixGen3}[X,Y] > \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y] > \end{theorem} > > ApplExpr(LHS="w", RHS="_\inv[X,Y]", MF=false) > > (e.g., mistakenly we forgot to put \inv on the LHS, yet no error is raised!) > > Shouldn't we have an error here either when applying w to inv or when comparing it to z? > Do you mean a type error? I don't think so. If we consider the types, we have (substituting in unique generic parameters to avoid confusion): \_ \inv: P (P(A x B) x P(B x A)) % (A x B) \fun (B x A) w : P(C x D) z : P(E x F) The expression w (\_~\inv)[E,F] is a function application. The type of (\_ \inv)[E,F] is P (P(E x F) x P(F x E))) from the explicit instantiation. Therefore, the type of the refexpr "w" is inferred as P(P(E x F) x P(F x E) x Var), where C is instantiated by P(P(E x F) x P(F x E)) and D is not instantiated (yet), so is given a variable type Var. The equality z = w(\_\inv)[E,F] allows us to infer that Var = F, so the type of w is fully instantiated. Confused? :) Tim 
From: Leo Freitas <leo.freitas@ne...>  20110921 09:06:12

Hi, I got puzzled by postfix ApplExpr types. The Std says (after syntactic transformations) there are two cases: mixfix and !mixfix. a) mixfix true: okay, as expected \begin{theorem}{postfixGen}[X,Y] \vdash? \forall q : X \fun Y; f : Y \fun X @ q = f\inv \end{theorem} Here, in (f\inv) we have an ApplExpr(LHS="_ \inv", RHS="f", MF=true) (e.g., syntactic transformation puts \inv in the LHS of ApplExpr) b) mixfix false: okay, as expected \begin{theorem}{postfixGen2}[X,Y] \vdash? \forall g: X \fun Y; h: Y \fun X @ h = (\_~\inv)[X,Y] g \end{theorem} ApplExpr(LHS="_ \inv[X,Y]", RHS="g", MF=true) (e.g., one MUST explicitly put the postfix on the LHS) c) PUZZLE \begin{gendef}[X,Y] w : Y \fun X \end{gendef} \begin{theorem}{postfixGen3}[X,Y] \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y] \end{theorem} ApplExpr(LHS="w", RHS="_\inv[X,Y]", MF=false) (e.g., mistakenly we forgot to put \inv on the LHS, yet no error is raised!) Shouldn't we have an error here either when applying w to inv or when comparing it to z? ======== context This came across as a result of translating posfix expressions to CZT ZEvesEclipse , which handles generics slightly different: CZT : (_ NAME _)[X,Y] ZEves: (_ NAME[X,Y] _) That means when we have ZEves terms like A \cup[X] B we get in trouble and need it to be something like (\_ \cup \_)[X] (A,B) which both CZT and ZEves are happy with. Now, when handling postifix I got f \inv[X,Y] then at some point mistakenly translated it to f (\_ \inv)[X,Y] instead of (\_ \inv)[X,Y] f hence the test case (c) above appeared and the puzzle... ====== Could somebody shed any light, pls? Best, Leo 