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

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}
(74) 
_{Nov}
(85) 
_{Dec}
(42) 

2002 
_{Jan}
(30) 
_{Feb}
(6) 
_{Mar}
(34) 
_{Apr}
(53) 
_{May}
(30) 
_{Jun}
(25) 
_{Jul}
(17) 
_{Aug}
(12) 
_{Sep}
(4) 
_{Oct}

_{Nov}
(2) 
_{Dec}
(6) 
2003 
_{Jan}
(17) 
_{Feb}
(7) 
_{Mar}
(25) 
_{Apr}
(9) 
_{May}
(17) 
_{Jun}
(32) 
_{Jul}
(10) 
_{Aug}
(1) 
_{Sep}
(2) 
_{Oct}
(15) 
_{Nov}
(5) 
_{Dec}
(2) 
2004 
_{Jan}
(22) 
_{Feb}
(1) 
_{Mar}
(1) 
_{Apr}

_{May}
(14) 
_{Jun}
(7) 
_{Jul}
(18) 
_{Aug}
(3) 
_{Sep}

_{Oct}
(14) 
_{Nov}
(7) 
_{Dec}
(5) 
2005 
_{Jan}
(17) 
_{Feb}
(19) 
_{Mar}
(18) 
_{Apr}
(23) 
_{May}
(8) 
_{Jun}
(8) 
_{Jul}
(11) 
_{Aug}
(23) 
_{Sep}
(11) 
_{Oct}
(2) 
_{Nov}
(32) 
_{Dec}
(3) 
2006 
_{Jan}

_{Feb}
(14) 
_{Mar}
(3) 
_{Apr}
(5) 
_{May}
(37) 
_{Jun}
(9) 
_{Jul}
(5) 
_{Aug}
(37) 
_{Sep}
(54) 
_{Oct}
(28) 
_{Nov}
(12) 
_{Dec}
(8) 
2007 
_{Jan}
(28) 
_{Feb}
(2) 
_{Mar}
(15) 
_{Apr}
(6) 
_{May}
(9) 
_{Jun}
(11) 
_{Jul}
(11) 
_{Aug}
(7) 
_{Sep}
(4) 
_{Oct}
(24) 
_{Nov}
(6) 
_{Dec}
(3) 
2008 
_{Jan}
(3) 
_{Feb}
(3) 
_{Mar}
(12) 
_{Apr}
(13) 
_{May}
(13) 
_{Jun}
(2) 
_{Jul}
(11) 
_{Aug}
(25) 
_{Sep}
(3) 
_{Oct}
(12) 
_{Nov}

_{Dec}

2009 
_{Jan}
(11) 
_{Feb}
(4) 
_{Mar}
(2) 
_{Apr}
(13) 
_{May}
(16) 
_{Jun}
(36) 
_{Jul}
(45) 
_{Aug}
(8) 
_{Sep}
(47) 
_{Oct}
(8) 
_{Nov}
(3) 
_{Dec}
(6) 
2010 
_{Jan}
(25) 
_{Feb}
(5) 
_{Mar}
(21) 
_{Apr}
(19) 
_{May}
(2) 
_{Jun}
(10) 
_{Jul}
(8) 
_{Aug}
(1) 
_{Sep}
(9) 
_{Oct}
(6) 
_{Nov}
(2) 
_{Dec}
(1) 
2011 
_{Jan}
(4) 
_{Feb}

_{Mar}

_{Apr}
(25) 
_{May}
(11) 
_{Jun}
(1) 
_{Jul}

_{Aug}
(8) 
_{Sep}
(14) 
_{Oct}
(2) 
_{Nov}

_{Dec}

2012 
_{Jan}

_{Feb}
(1) 
_{Mar}
(9) 
_{Apr}
(18) 
_{May}

_{Jun}
(4) 
_{Jul}
(2) 
_{Aug}
(2) 
_{Sep}
(10) 
_{Oct}
(18) 
_{Nov}
(4) 
_{Dec}
(1) 
2013 
_{Jan}

_{Feb}
(5) 
_{Mar}
(1) 
_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(5) 
_{Sep}

_{Oct}

_{Nov}

_{Dec}

2014 
_{Jan}

_{Feb}
(3) 
_{Mar}

_{Apr}

_{May}
(1) 
_{Jun}
(2) 
_{Jul}
(2) 
_{Aug}
(9) 
_{Sep}

_{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
(9) 
20
(1) 
21

22

23

24

25

26

27

28

29

30
(1) 
31

From: Tjark Weber <tw333@ca...>  20090130 02:14:01

Hi, I have just committed a very first version of HolSmtLib, a new library for calling SMT solvers from HOL. To use it, you must have the SMT solver Yices 1.0.18 (available from http://yices.csl.sri.com/) installed. The "yices" executable must be in a directory that is included in your shell path. Usage examples:  load "HolSmtLib"; open HolSmtLib; (* output omitted *) > val it = () : unit  YICES_ORACLE ``(a ==> b) /\ (b ==> a) ==> (a=b)``; (* output omitted *) > val it =  (a ==> b) /\ (b ==> a) ==> (a = b) : thm  YICES_ORACLE ``(f (f (f a)) = a) /\ (f (f (f (f (f a)))) = a) ==> (f a = a)``; <<HOL message: inventing new type variable names: 'a>> (* output omitted *) > val it =  (f (f (f a)) = a) /\ (f (f (f (f (f a)))) = a) ==> (f a = a) : thm Beware! Currently there are severe restrictions:  Uninterpreted functions, equality, and the usual Boolean connectives only  no support for arithmetic, arrays, bit vectors, quantifiers, lambda terms, etc.  No proof reconstruction (oracle only).  No counterexamples for unprovable formulas.  No support for other SMT solvers. I hope to add these and other features over time. Please feel free to try it out! Feedback is of course very welcome. Regards, Tjark 
From: Michael Norrish <Michael.N<orrish@ni...>  20090120 04:58:12

Konrad Slind wrote: > Last I looked (mid90's) Isabelle used an Earleystyle > fullCFG parser, augmented with precedences. This kind of parsing is > totally flexible, although slow (n^3) on ambiguous inputs. I suppose > the precedence levels cut down on the ambiguity. However, because we > sometimes/often use really big terms, I would prefer a linear > parser. Yeah, me too. We could still go to LR without doing the generalised parsing bit, and that would keep us linear time. There are also tools like ANTLR that apparently use LL style parsing successfully. It might be interesting to see what their underlying engine does. > Precedence level based restructuring of grammars to eliminate > ambiguity works well for fixed grammars, e.g. for arithmetic > expressions with binary and unary minus, but the HOL grammar is > extensible and I'm not aware of any automatic ambiguity eliminator > for grammars (ambig. is wellknown to be undecidable). > However, would it be possible to have another pass at the Absyn > level (after the first pass of parsing) which would attempt to > resolve binary/prefix operators with the same name? Somewhat adhoc > but at least it lets us keep the investment in our current parser > technology. Hmm. I can't see how to distinguish normal application of unary subtraction, and partial application of binary subtraction. But, if you were willing to always write the latter as (\y. x  y), then it would indeed be easy given our existing setup to magically change bare occurrences of x into unary_minus x at the Absyn stage. Unfortunately, that's not really the problem. The issue arises before, at the concrete syntax to Absyn stage, where we have to know how to reduce phrases. For example, x + f y turns into APP (APP(+,x), APP(f,y)) I don't how to simultaneously have f x  y turn into APP(APP(,APP(f,x)),y) when x + y has to turn into APP(APP(+,x),APP(,y)) At the concrete level, the terms look similar, same last two tokens etc. At the Absyn level, the trees have to be of quite different shapes. Actually, after playing around with this for a bit, it may be possible to have prefix operators that are the same as infixes because the parser can see if there is a phrase to the left of the operator... Stay tuned :) Michael. 
From: Konrad Slind <slind@cs...>  20090119 22:58:09

Hi Michael, Last I looked (mid90's) Isabelle used an Earleystyle fullCFG parser, augmented with precedences. This kind of parsing is totally flexible, although slow (n^3) on ambiguous inputs. I suppose the precedence levels cut down on the ambiguity. However, because we sometimes/often use really big terms, I would prefer a linear parser. Precedence level based restructuring of grammars to eliminate ambiguity works well for fixed grammars, e.g. for arithmetic expressions with binary and unary minus, but the HOL grammar is extensible and I'm not aware of any automatic ambiguity eliminator for grammars (ambig. is wellknown to be undecidable). However, would it be possible to have another pass at the Absyn level (after the first pass of parsing) which would attempt to resolve binary/prefix operators with the same name? Somewhat adhoc but at least it lets us keep the investment in our current parser technology. Konrad. On Jan 19, 2009, at 3:36 PM, Michael Norrish wrote: > Peter Vincent Homeier wrote: > >> I would agree with Markus Kuhn, in that it seems most natural to >> make unary minus and binary minus the same symbol, distinguished by >> the parser, rather than at some lower level of lexing. If you think >> of it, they really are the same operation; it's like "5" is an >> abbreviation for "05". I find no cognitive dissonance with this >> approach. > > Yes. I should have said upfront that the symbol needs to be > different because our parsing technology can't cope with it as both an > infix and a prefix operator, as Anthony has found. We use precedence > parsing instead. > > There are only really two advantages to precedence parsing. First, it > was easy to implement. A little more significantly, we get to write > things like > > p y ==> !x. R x y > > In Isabelle, they use precedence levels in a similar way to us (so > that ! is at a weaker, less binding, level than ==>), but cannot parse > the above. Instead, they have to write > > p y ==> (!x. R x y) > > (though the implication symbol would actually be > for them) > > I believe this is because the precedence levels lead to the creation > of the obvious CFG, which is then turned into an LR machine of some > sort. In the case of a grammar with ==> and ! the grammar would be > > T ::= !<var>. T  T0 > T0 ::= T1 ==> T0  T1 > T1 ::= <leaf form>  ( T ) > > You'll note that this grammar does not admit the first formula above, > the one without the parentheses. > > If we were to adopt better LR parsing technology, I'd want to figure > out the rule for creating the 'right' grammar, the one that admits our > string properly. It's not entirely trivial. In the simple case > above, you might think it could be > > T ::= !<var>. T  T0 > T0 ::= T1 ==> T  T1 > T1 ::= <leaf form>  ( T ) > > but this is then ambiguous on ``p ==> q`` because you can double back > to T from T0 before finally going straight to T1. Maybe it's > > T ::= !<var>. T  T0 > T0 ::= T1 ==> T0  T1  T1 ==> !<var>. T > T1 ::= <leaf form>  ( T ) > > This isn't obviously ambiguous anyway. > > If you have prefix operators (like !) and suffix operators (like type > annotation) at arbitrary precedence levels through the grammar, I > don't know now, and couldn't figure out when I was reimplementing the > parsing for Taupo1, what the right construction was. And so, in the > interests of some backwards compatibility with the existing HOL > syntax, I went for precedence parsing. > > I don't think I tried that hard to figure out what the algorithm was > because thinking about it a bit now does suggest one possible idea. > But then I'd need to implement a new parsing engine. > > But perhaps we could just go Isabelle's route and stick in more > parentheses. > > Michael. > >  >  > This SF.net email is sponsored by: > SourcForge Community > SourceForge wants to tell your story. > http://p.sf.net/sfu/sfspreadtheword > _______________________________________________ > Holdevelopers mailing list > Holdevelopers@... > https://lists.sourceforge.net/lists/listinfo/holdevelopers 
From: Michael Norrish <Michael.N<orrish@ni...>  20090119 22:36:52

Peter Vincent Homeier wrote: > I would agree with Markus Kuhn, in that it seems most natural to > make unary minus and binary minus the same symbol, distinguished by > the parser, rather than at some lower level of lexing. If you think > of it, they really are the same operation; it's like "5" is an > abbreviation for "05". I find no cognitive dissonance with this > approach. Yes. I should have said upfront that the symbol needs to be different because our parsing technology can't cope with it as both an infix and a prefix operator, as Anthony has found. We use precedence parsing instead. There are only really two advantages to precedence parsing. First, it was easy to implement. A little more significantly, we get to write things like p y ==> !x. R x y In Isabelle, they use precedence levels in a similar way to us (so that ! is at a weaker, less binding, level than ==>), but cannot parse the above. Instead, they have to write p y ==> (!x. R x y) (though the implication symbol would actually be > for them) I believe this is because the precedence levels lead to the creation of the obvious CFG, which is then turned into an LR machine of some sort. In the case of a grammar with ==> and ! the grammar would be T ::= !<var>. T  T0 T0 ::= T1 ==> T0  T1 T1 ::= <leaf form>  ( T ) You'll note that this grammar does not admit the first formula above, the one without the parentheses. If we were to adopt better LR parsing technology, I'd want to figure out the rule for creating the 'right' grammar, the one that admits our string properly. It's not entirely trivial. In the simple case above, you might think it could be T ::= !<var>. T  T0 T0 ::= T1 ==> T  T1 T1 ::= <leaf form>  ( T ) but this is then ambiguous on ``p ==> q`` because you can double back to T from T0 before finally going straight to T1. Maybe it's T ::= !<var>. T  T0 T0 ::= T1 ==> T0  T1  T1 ==> !<var>. T T1 ::= <leaf form>  ( T ) This isn't obviously ambiguous anyway. If you have prefix operators (like !) and suffix operators (like type annotation) at arbitrary precedence levels through the grammar, I don't know now, and couldn't figure out when I was reimplementing the parsing for Taupo1, what the right construction was. And so, in the interests of some backwards compatibility with the existing HOL syntax, I went for precedence parsing. I don't think I tried that hard to figure out what the algorithm was because thinking about it a bit now does suggest one possible idea. But then I'd need to implement a new parsing engine. But perhaps we could just go Isabelle's route and stick in more parentheses. Michael. 
From: Anthony Fox <acjf3@ca...>  20090119 15:23:21

This is the situation with words, where word_2comp and word_sub are both "" (and "~" is word_1comp). However, at the moment, this means that you have:  ``$ 5w``; <<HOL message: more than one resolution of overloading was possible>> <<HOL message: inventing new type variable names: 'a>> > val it = ``$ 5w`` : term  `` 5w``; on line 6, characters 25: missing left argument to  ! Uncaught exception: ! HOL_ERR which isn't ideal. Anthony. On 19 Jan 2009, at 14:59, Peter Vincent Homeier wrote: > I would agree with Markus Kuhn, in that it seems most natural to > make unary minus and binary minus the same symbol, distinguished by > the parser, rather than at some lower level of lexing. If you > think of it, they really are the same operation; it's like "5" is > an abbreviation for "05". I find no cognitive dissonance with > this approach. > > Peter > > On Mon, Jan 19, 2009 at 8:51 AM, Ian Grant <Ian.Grant@...> > wrote: > I asked a local expert about this and his reply might be useful: > > Begin forwarded message: > > Date: Mon, 19 Jan 2009 12:12:58 +0000 > From: Markus Kuhn <Markus.Kuhn@...> > To: Ian Grant <Ian.Grant@...> > Subject: Re: Fw: [Holdevelopers] opinions about Unicode unary > (numeral) negation? > > > Ian Grant wrote on 20090119 11:27 UTC: > > This can't be true can it? If it is I'll go back 7 bit ASCII just to > > make a point. From: Michael Norrish <Michael.Norrish@...> > > > As far as I can tell, Unicode doesn't explicitly define a > symbol for > > > unary negation (though it quite happily defines a subtraction > > > symbol, so that people can distinguish hyphens from subtraction). > > That is correct, and I think that unification of binary and unary > minus > is the right thing to do for typography. Hyphen and minus are clearly > distinct glyphs, whereas binary and unary minus are clearly the same > glyph, just used in different contexts. > > It is already difficult enough for people to pick the right symbol on > keyboards if there are already hyphen, nobreak hyphen, en dash, em > dash, minus, and it would just increase the likelyhood of people using > (and reading) the wrong homoglyph if more were to be added, such as > UNARY MINUS. It would be a true debugging nightmare. > > [However, a bit of a mess has emerged, in that for some symbols, > Unicode > tries to disambiguate between binaryoperator and other symbols, and > therefore has added duplicates of a few that I consider the same > symbol > (e.g. UP TACK versus PERPENDICULAR). Different Unicode contributors > had different ideas about whether the spacing around an operator > should be > included in the glyph or should be encoded as an extra space; the > TeXinfluenced STIX project might be to blame mostly.] > > I've never used HOL, and the UTF8 bytes used in Michael's email were > substituted by underscores before they arrived here, so I don't fully > understand what is being suggested here. In all computer languages > that I've used so far, the distinction between binary and unary > minus is > clear from the parsing grammar of numerical expressions. (C & friends > have no problem with parsing even ab. :) Note that Unicode > (Latin1) has also > a logical not sign __, and that is (thanks to EBCDIC legacy) > already found > on the UK PC keyboard layout. Unicode has lots of other minus > related symbols > if you really need to chose a new notation that uses clearly > different glyphs > for binary and unary minus, e.g. > > $ grep MINUS ~mgk25/proj/uniset/UnicodeData.txt  perl ne > '@a=split/;/; print "U+$a[0] $a[1]\n"' > U+002D HYPHENMINUS > U+00B1 PLUSMINUS SIGN > U+02D7 MODIFIER LETTER MINUS SIGN > U+0320 COMBINING MINUS SIGN BELOW > U+2052 COMMERCIAL MINUS SIGN > U+207B SUPERSCRIPT MINUS > U+208B SUBSCRIPT MINUS > U+2212 MINUS SIGN > U+2213 MINUSORPLUS SIGN > U+2216 SET MINUS > U+2238 DOT MINUS > U+2242 MINUS TILDE > U+2296 CIRCLED MINUS > U+229F SQUARED MINUS > U+2756 BLACK DIAMOND MINUS WHITE X > U+293C TOP ARC CLOCKWISE ARROW WITH MINUS > U+2A29 MINUS SIGN WITH COMMA ABOVE > U+2A2A MINUS SIGN WITH DOT BELOW > U+2A2B MINUS SIGN WITH FALLING DOTS > U+2A2C MINUS SIGN WITH RISING DOTS > U+2A3A MINUS SIGN IN TRIANGLE > U+2A41 UNION WITH MINUS SIGN > U+2A6C SIMILAR MINUS SIMILAR > U+FE63 SMALL HYPHENMINUS > U+FF0D FULLWIDTH HYPHENMINUS > U+E002D TAG HYPHENMINUS > > (not to forget that combining characters can be used to produce > infinitely many more minusrelated symbols.) > > Markus > (now a member of the British Standards committee looking after the > ISO 3111 standard for mathematical notation, soon to be > republished as > ISO 800002, which might even include a Unicode mapping table.) > >  > Markus Kuhn, Computer Laboratory, University of Cambridge > http://www.cl.cam.ac.uk/~mgk25/  CB3 0FD, Great Britain > > >  >  > This SF.net email is sponsored by: > SourcForge Community > SourceForge wants to tell your story. > http://p.sf.net/sfu/sfspreadtheword > _______________________________________________ > Holdevelopers mailing list > Holdevelopers@... > https://lists.sourceforge.net/lists/listinfo/holdevelopers > > > >  > "In Your majesty ride prosperously > because of truth, humility, and righteousness; > and Your right hand shall teach You awesome things." (Psalm 45:4) >  >  > This SF.net email is sponsored by: > SourcForge Community > SourceForge wants to tell your story. > http://p.sf.net/sfu/sf > spreadtheword_______________________________________________ > Holdevelopers mailing list > Holdevelopers@... > https://lists.sourceforge.net/lists/listinfo/holdevelopers 
From: Peter Vincent Homeier <palantir@tr...>  20090119 14:59:54

I would agree with Markus Kuhn, in that it seems most natural to make unary minus and binary minus the same symbol, distinguished by the parser, rather than at some lower level of lexing. If you think of it, they really are the same operation; it's like "5" is an abbreviation for "05". I find no cognitive dissonance with this approach. Peter On Mon, Jan 19, 2009 at 8:51 AM, Ian Grant <Ian.Grant@...> wrote: > I asked a local expert about this and his reply might be useful: > > Begin forwarded message: > > Date: Mon, 19 Jan 2009 12:12:58 +0000 > From: Markus Kuhn <Markus.Kuhn@...> > To: Ian Grant <Ian.Grant@...> > Subject: Re: Fw: [Holdevelopers] opinions about Unicode unary (numeral) > negation? > > > Ian Grant wrote on 20090119 11:27 UTC: > > This can't be true can it? If it is I'll go back 7 bit ASCII just to > > make a point. From: Michael Norrish <Michael.Norrish@...> > > > As far as I can tell, Unicode doesn't explicitly define a symbol for > > > unary negation (though it quite happily defines a subtraction > > > symbol, so that people can distinguish hyphens from subtraction). > > That is correct, and I think that unification of binary and unary minus > is the right thing to do for typography. Hyphen and minus are clearly > distinct glyphs, whereas binary and unary minus are clearly the same > glyph, just used in different contexts. > > It is already difficult enough for people to pick the right symbol on > keyboards if there are already hyphen, nobreak hyphen, en dash, em > dash, minus, and it would just increase the likelyhood of people using > (and reading) the wrong homoglyph if more were to be added, such as > UNARY MINUS. It would be a true debugging nightmare. > > [However, a bit of a mess has emerged, in that for some symbols, Unicode > tries to disambiguate between binaryoperator and other symbols, and > therefore has added duplicates of a few that I consider the same symbol > (e.g. UP TACK versus PERPENDICULAR). Different Unicode contributors > had different ideas about whether the spacing around an operator should be > included in the glyph or should be encoded as an extra space; the > TeXinfluenced STIX project might be to blame mostly.] > > I've never used HOL, and the UTF8 bytes used in Michael's email were > substituted by underscores before they arrived here, so I don't fully > understand what is being suggested here. In all computer languages > that I've used so far, the distinction between binary and unary minus is > clear from the parsing grammar of numerical expressions. (C & friends > have no problem with parsing even ab. :) Note that Unicode (Latin1) > has also > a logical not sign __, and that is (thanks to EBCDIC legacy) already found > on the UK PC keyboard layout. Unicode has lots of other minusrelated > symbols > if you really need to chose a new notation that uses clearly different > glyphs > for binary and unary minus, e.g. > > $ grep MINUS ~mgk25/proj/uniset/UnicodeData.txt  perl ne '@a=split/;/; > print "U+$a[0] $a[1]\n"' > U+002D HYPHENMINUS > U+00B1 PLUSMINUS SIGN > U+02D7 MODIFIER LETTER MINUS SIGN > U+0320 COMBINING MINUS SIGN BELOW > U+2052 COMMERCIAL MINUS SIGN > U+207B SUPERSCRIPT MINUS > U+208B SUBSCRIPT MINUS > U+2212 MINUS SIGN > U+2213 MINUSORPLUS SIGN > U+2216 SET MINUS > U+2238 DOT MINUS > U+2242 MINUS TILDE > U+2296 CIRCLED MINUS > U+229F SQUARED MINUS > U+2756 BLACK DIAMOND MINUS WHITE X > U+293C TOP ARC CLOCKWISE ARROW WITH MINUS > U+2A29 MINUS SIGN WITH COMMA ABOVE > U+2A2A MINUS SIGN WITH DOT BELOW > U+2A2B MINUS SIGN WITH FALLING DOTS > U+2A2C MINUS SIGN WITH RISING DOTS > U+2A3A MINUS SIGN IN TRIANGLE > U+2A41 UNION WITH MINUS SIGN > U+2A6C SIMILAR MINUS SIMILAR > U+FE63 SMALL HYPHENMINUS > U+FF0D FULLWIDTH HYPHENMINUS > U+E002D TAG HYPHENMINUS > > (not to forget that combining characters can be used to produce > infinitely many more minusrelated symbols.) > > Markus > (now a member of the British Standards committee looking after the > ISO 3111 standard for mathematical notation, soon to be republished as > ISO 800002, which might even include a Unicode mapping table.) > >  > Markus Kuhn, Computer Laboratory, University of Cambridge > http://www.cl.cam.ac.uk/~mgk25/ <http://www.cl.cam.ac.uk/%7Emgk25/>;  CB3 > 0FD, Great Britain > > > >  > This SF.net email is sponsored by: > SourcForge Community > SourceForge wants to tell your story. > http://p.sf.net/sfu/sfspreadtheword > _______________________________________________ > Holdevelopers mailing list > Holdevelopers@... > https://lists.sourceforge.net/lists/listinfo/holdevelopers >  "In Your majesty ride prosperously because of truth, humility, and righteousness; and Your right hand shall teach You awesome things." (Psalm 45:4) 
From: Ian Grant <Ian.G<rant@cl...>  20090119 13:51:58

I asked a local expert about this and his reply might be useful: Begin forwarded message: Date: Mon, 19 Jan 2009 12:12:58 +0000 From: Markus Kuhn <Markus.Kuhn@...> To: Ian Grant <Ian.Grant@...> Subject: Re: Fw: [Holdevelopers] opinions about Unicode unary (numeral) negation? Ian Grant wrote on 20090119 11:27 UTC: > This can't be true can it? If it is I'll go back 7 bit ASCII just to > make a point. From: Michael Norrish <Michael.Norrish@...> > > As far as I can tell, Unicode doesn't explicitly define a symbol for > > unary negation (though it quite happily defines a subtraction > > symbol, so that people can distinguish hyphens from subtraction). That is correct, and I think that unification of binary and unary minus is the right thing to do for typography. Hyphen and minus are clearly distinct glyphs, whereas binary and unary minus are clearly the same glyph, just used in different contexts. It is already difficult enough for people to pick the right symbol on keyboards if there are already hyphen, nobreak hyphen, en dash, em dash, minus, and it would just increase the likelyhood of people using (and reading) the wrong homoglyph if more were to be added, such as UNARY MINUS. It would be a true debugging nightmare. [However, a bit of a mess has emerged, in that for some symbols, Unicode tries to disambiguate between binaryoperator and other symbols, and therefore has added duplicates of a few that I consider the same symbol (e.g. UP TACK versus PERPENDICULAR). Different Unicode contributors had different ideas about whether the spacing around an operator should be included in the glyph or should be encoded as an extra space; the TeXinfluenced STIX project might be to blame mostly.] I've never used HOL, and the UTF8 bytes used in Michael's email were substituted by underscores before they arrived here, so I don't fully understand what is being suggested here. In all computer languages that I've used so far, the distinction between binary and unary minus is clear from the parsing grammar of numerical expressions. (C & friends have no problem with parsing even ab. :) Note that Unicode (Latin1) has also a logical not sign __, and that is (thanks to EBCDIC legacy) already found on the UK PC keyboard layout. Unicode has lots of other minusrelated symbols if you really need to chose a new notation that uses clearly different glyphs for binary and unary minus, e.g. $ grep MINUS ~mgk25/proj/uniset/UnicodeData.txt  perl ne '@a=split/;/; print "U+$a[0] $a[1]\n"' U+002D HYPHENMINUS U+00B1 PLUSMINUS SIGN U+02D7 MODIFIER LETTER MINUS SIGN U+0320 COMBINING MINUS SIGN BELOW U+2052 COMMERCIAL MINUS SIGN U+207B SUPERSCRIPT MINUS U+208B SUBSCRIPT MINUS U+2212 MINUS SIGN U+2213 MINUSORPLUS SIGN U+2216 SET MINUS U+2238 DOT MINUS U+2242 MINUS TILDE U+2296 CIRCLED MINUS U+229F SQUARED MINUS U+2756 BLACK DIAMOND MINUS WHITE X U+293C TOP ARC CLOCKWISE ARROW WITH MINUS U+2A29 MINUS SIGN WITH COMMA ABOVE U+2A2A MINUS SIGN WITH DOT BELOW U+2A2B MINUS SIGN WITH FALLING DOTS U+2A2C MINUS SIGN WITH RISING DOTS U+2A3A MINUS SIGN IN TRIANGLE U+2A41 UNION WITH MINUS SIGN U+2A6C SIMILAR MINUS SIMILAR U+FE63 SMALL HYPHENMINUS U+FF0D FULLWIDTH HYPHENMINUS U+E002D TAG HYPHENMINUS (not to forget that combining characters can be used to produce infinitely many more minusrelated symbols.) Markus (now a member of the British Standards committee looking after the ISO 3111 standard for mathematical notation, soon to be republished as ISO 800002, which might even include a Unicode mapping table.)  Markus Kuhn, Computer Laboratory, University of Cambridge http://www.cl.cam.ac.uk/~mgk25/  CB3 0FD, Great Britain 
From: Anthony Fox <acjf3@ca...>  20090119 11:08:12

Perhaps "small hyphenminus" (0xFE63) for numeric negation. I'm not particularly keen on "superscript minus" here. Anthony. On 19 Jan 2009, at 10:59, Michael Norrish wrote: > "Tjark Weber" <tw333@...> wrote: >> On Mon, 20090119 at 14:53 +1100, Michael Norrish wrote: >>> At the moment, HOL uses ~ (tilde) for boolean and numeric negation >>> in >>> ASCIIworld, and this works OK (the tilde is consistent with SML). >>> However, with Unicode enabled, it then uses ¬ for both purposes too. > >> Changing the latter (i.e., supporting different syntax for different >> (overloaded) functions in Unicode) is not an option? > > The API isn't quite there yet, but this will be an option. The > question was > more "which symbol should we use?" (¬ is clearly not right). > > Michael > > > >  > This SF.net email is sponsored by: > SourcForge Community > SourceForge wants to tell your story. > http://p.sf.net/sfu/sfspreadtheword > _______________________________________________ > Holdevelopers mailing list > Holdevelopers@... > https://lists.sourceforge.net/lists/listinfo/holdevelopers 
From: Michael Norrish <michael.norrish@ni...>  20090119 10:59:27

"Tjark Weber" <tw333@...> wrote: > On Mon, 20090119 at 14:53 +1100, Michael Norrish wrote: >> At the moment, HOL uses ~ (tilde) for boolean and numeric negation in >> ASCIIworld, and this works OK (the tilde is consistent with SML). >> However, with Unicode enabled, it then uses ¬ for both purposes too. > Changing the latter (i.e., supporting different syntax for different > (overloaded) functions in Unicode) is not an option? The API isn't quite there yet, but this will be an option. The question was more "which symbol should we use?" (¬ is clearly not right). Michael 
From: Tjark Weber <tw333@ca...>  20090119 09:40:40

On Mon, 20090119 at 14:53 +1100, Michael Norrish wrote: > At the moment, HOL uses ~ (tilde) for boolean and numeric negation in > ASCIIworld, and this works OK (the tilde is consistent with SML). > However, with Unicode enabled, it then uses ¬ for both purposes too. Changing the latter (i.e., supporting different syntax for different (overloaded) functions in Unicode) is not an option? Regards, Tjark 
From: Michael Norrish <Michael.N<orrish@ni...>  20090119 03:54:11

As far as I can tell, Unicode doesn't explicitly define a symbol for unary negation (though it quite happily defines a subtraction symbol, so that people can distinguish hyphens from subtraction). At the moment, HOL uses ~ (tilde) for boolean and numeric negation in ASCIIworld, and this works OK (the tilde is consistent with SML). However, with Unicode enabled, it then uses ¬ for both purposes too. It seems silly to have things like ¬2 (along with boolean things like ¬p ∧ q). One possibility would be to have a superscript minus (⁻) as a prefix operator to serve as numeric negation. Things in Unicode land might then look like [int_sub]  x  y = x + ⁻y (This may or may not look good depending on your font. On my Mac Emacs, it looks good; but in Thunderbird, it only looks OK because the layout puts in some strange extra space after the symbol. On my Linux Emacs, it also looks good.) Any other suggestions? Michael. 