Screenshot instructions:
Windows
Mac
Red Hat Linux
Ubuntu
Click URL instructions:
Rightclick on ad, choose "Copy Link", then paste here →
(This may not be possible with some types of ads)
You can subscribe to this list here.
2007 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(73) 
_{Sep}
(57) 
_{Oct}
(138) 
_{Nov}
(91) 
_{Dec}
(99) 

2008 
_{Jan}
(91) 
_{Feb}
(53) 
_{Mar}
(37) 
_{Apr}
(125) 
_{May}
(176) 
_{Jun}
(23) 
_{Jul}
(135) 
_{Aug}
(119) 
_{Sep}
(26) 
_{Oct}
(38) 
_{Nov}
(46) 
_{Dec}
(11) 
2009 
_{Jan}
(4) 
_{Feb}
(2) 
_{Mar}
(5) 
_{Apr}
(15) 
_{May}
(4) 
_{Jun}
(18) 
_{Jul}
(1) 
_{Aug}
(4) 
_{Sep}
(17) 
_{Oct}
(9) 
_{Nov}
(14) 
_{Dec}
(11) 
2010 
_{Jan}
(9) 
_{Feb}
(6) 
_{Mar}
(1) 
_{Apr}
(1) 
_{May}
(4) 
_{Jun}
(3) 
_{Jul}

_{Aug}
(10) 
_{Sep}
(7) 
_{Oct}
(7) 
_{Nov}
(36) 
_{Dec}
(23) 
2011 
_{Jan}
(2) 
_{Feb}
(1) 
_{Mar}
(1) 
_{Apr}
(11) 
_{May}
(5) 
_{Jun}
(17) 
_{Jul}
(2) 
_{Aug}
(26) 
_{Sep}
(14) 
_{Oct}
(51) 
_{Nov}
(39) 
_{Dec}
(7) 
2012 
_{Jan}
(24) 
_{Feb}
(7) 
_{Mar}
(9) 
_{Apr}
(2) 
_{May}
(9) 
_{Jun}
(7) 
_{Jul}
(3) 
_{Aug}
(1) 
_{Sep}
(8) 
_{Oct}
(12) 
_{Nov}
(1) 
_{Dec}

2013 
_{Jan}

_{Feb}

_{Mar}

_{Apr}
(35) 
_{May}
(28) 
_{Jun}
(14) 
_{Jul}
(10) 
_{Aug}
(3) 
_{Sep}
(6) 
_{Oct}

_{Nov}
(1) 
_{Dec}

2014 
_{Jan}

_{Feb}

_{Mar}

_{Apr}
(4) 
_{May}
(3) 
_{Jun}
(2) 
_{Jul}
(2) 
_{Aug}
(2) 
_{Sep}
(1) 
_{Oct}
(3) 
_{Nov}
(5) 
_{Dec}
(8) 
2015 
_{Jan}
(3) 
_{Feb}
(2) 
_{Mar}

_{Apr}

_{May}
(1) 
_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}
(1) 
2016 
_{Jan}
(5) 
_{Feb}
(10) 
_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}
(5) 
2017 
_{Jan}
(2) 
_{Feb}
(2) 
_{Mar}
(5) 
_{Apr}
(1) 
_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 






1

2

3

4

5

6

7

8

9
(2) 
10

11

12

13
(4) 
14

15

16

17

18

19

20

21
(1) 
22

23
(1) 
24
(3) 
25

26

27

28

29

30

From: Gabriel Dos Reis <gdr@cs...>  20110424 20:49:14

Bill Page <bill.page@...> writes:  Gaby,   Thank you. That's very interesting to me. I just built OpenAxiom from  trunk and I get:   page@...:~/openaxiombuild$ openaxiom   OpenAxiom: The Open Scientific Computation Platform  Version: OpenAxiom 1.4.020110420  Built on Sunday April 24, 2011 at 13:29:12    Issue )copyright to view copyright notices.  Issue )summary for a summary of useful system commands.  Issue )quit to leave OpenAxiom and return to shell.      (1) > )sh MappingCategory  The )show system command is used to display information about types  or partial types. For example, )show Integer will show  information about Integer .   MappingCategory is not the name of a known type constructor. If  you want to see information about any operations named  MappingCategory , issue  )display operations MappingCategory   If I try Hyperdoc I get:   (1) >  >> System error:  The value _ is not of type CHARACTER.   and Hyperdoc crashes. Maybe somehow MappingCategory is not known to  the interpreter? I wonder what MappingCategory exports? MappingCategory isn't known to Hyperdoc yet. Although MappingCategory was added on 20110210, I did not get around to make an Hyperdoc entry for it. (In fact I needed for some internal project and forgot to provide the complete feature for the publically available OpenAxiom.) That should be fixed in the new few days.   But your example code does compile for me: and you can test it in the interpreter too :) f: MyFunction INT := myFunction * f 90 [...]  Is this a temporary problem? Am I missing something? temporary problem; thanks for reporting back.  Gaby 
From: Bill Page <bill.page@ne...>  20110424 20:39:06

Gaby, Thank you. That's very interesting to me. I just built OpenAxiom from trunk and I get: page@...:~/openaxiombuild$ openaxiom OpenAxiom: The Open Scientific Computation Platform Version: OpenAxiom 1.4.020110420 Built on Sunday April 24, 2011 at 13:29:12  Issue )copyright to view copyright notices. Issue )summary for a summary of useful system commands. Issue )quit to leave OpenAxiom and return to shell.  (1) > )sh MappingCategory The )show system command is used to display information about types or partial types. For example, )show Integer will show information about Integer . MappingCategory is not the name of a known type constructor. If you want to see information about any operations named MappingCategory , issue )display operations MappingCategory If I try Hyperdoc I get: (1) > >> System error: The value _ is not of type CHARACTER. and Hyperdoc crashes. Maybe somehow MappingCategory is not known to the interpreter? I wonder what MappingCategory exports? But your example code does compile for me: (1) > )sys cat MyFunction.spad )abbrev domain MYFUN MyFunction MyFunction(T: Type): Public == Private where Public == MappingCategory(T,T) with myFunction: ((T,T) > T) > % Private == add Rep == Mapping(T,T,T) myFunction f == per f elt(f,x) == (rep f)(x,x) (1) > )co MyFunction.spad Compiling OpenAxiom source code from file /home/page/MyFunction.spad using Spad compiler. MYFUN abbreviates domain MyFunction  initializing NRLIB MYFUN for MyFunction compiling into NRLIB MYFUN Adding $ modemaps Adding T$ modemaps compiling exported myFunction : (T,T) > T > % MYFUN;myFunction;M$;1 is replaced by f Time: 0.01 SEC. compiling exported elt : (%,T) > T Time: 0 SEC. (time taken in buildFunctor: 0) ;;; *** MyFunction REDEFINED ;;; *** MyFunction REDEFINED Time: 0 SEC. Cumulative Statistics for Constructor MyFunction Time: 0.01 seconds finalizing NRLIB MYFUN Processing MyFunction for Browser database: >>MyFunction((myFunction (% (Mapping T$ T$ T$)))): Not documented!!!! >>MyFunction(constructor): Not documented!!!! >>MyFunction: Missing Description ; compiling file "/home/page/MYFUN.NRLIB/code.lsp" (written 24 APR 2011 04:35:11 PM): ; compiling (/VERSIONCHECK 2) ; compiling (PUT (QUOTE MYFUN;myFunction;M$;1) ...) ; compiling (DEFUN MYFUN;myFunction;M$;1 ...) ; compiling (DEFUN MYFUN;elt;$2T$;2 ...) ; file: /home/page/MYFUN.NRLIB/code.lsp ; in: DEFUN MYFUN;elt;$2T$;2 ; (DEFUN BOOT::MYFUN;elt;$2T$;2 (BOOT::f BOOT::x BOOT::$) ; (BOOT::SPADCALL BOOT::x BOOT::x BOOT::f)) ; > PROGN EVALWHEN ; ==> ; (SBIMPL::%DEFUN 'BOOT::MYFUN;elt;$2T$;2 ; (SBINT:NAMEDLAMBDA BOOT::MYFUN;elt;$2T$;2 ; (BOOT::f BOOT::x BOOT::$) ; (BLOCK BOOT::MYFUN;elt;$2T$;2 ; (BOOT::SPADCALL BOOT::x BOOT::x BOOT::f))) ; NIL 'NIL (SBC:SOURCELOCATION)) ; ; caught STYLEWARNING: ; The variable $ is defined but never used. ; compiling (DEFUN MyFunction ...) ; compiling (DEFUN MyFunction; ...) ; compiling (MAKEPROP (QUOTE MyFunction) ...); ; compilation unit finished ; caught 1 STYLEWARNING condition ; /home/page/MYFUN.NRLIB/code.fasl written ; compilation finished in 0:00:00.178  MyFunction is now explicitly exposed in frame frame791 MyFunction will be automatically loaded when needed from /home/page/MYFUN.NRLIB/code.fasl (1) > Is this a temporary problem? Am I missing something? page@...:~/openaxiombuild$ cd ../openaxiomsrc page@...:~/openaxiomsrc$ svn info Path: . URL: https://openaxiom.svn.sf.net/svnroot/openaxiom/trunk Repository Root: https://openaxiom.svn.sf.net/svnroot/openaxiom Repository UUID: f499efd599370410b36ad3739c31ded8 Revision: 2080 Node Kind: directory Schedule: normal Last Changed Author: dosreis Last Changed Rev: 2080 Last Changed Date: 20110424 12:14:17 0400 (Sun, 24 Apr 2011) page@...:~/openaxiomsrc$ sbcl version SBCL 1.0.40.0.debian Regards, Bill Page. On Sun, Apr 24, 2011 at 10:16 AM, Gabriel Dos Reis <gdr@...> wrote: > ... > There is an nary MappingCategory category constructor in OpenAxiom. > I just did not get around to fix the instantiation of Mapping ot use it. > Is that what you had in mind? Yes I plan to fix related issues. > > The attached works for me. > >  Gaby > > )abbrev domain MYFUN MyFunction > MyFunction(T: Type): Public == Private where > Public == MappingCategory(T,T) with > myFunction: ((T,T) > T) > % > Private == add > Rep == Mapping(T,T,T) > myFunction f == per f > elt(f,x) == (rep f)(x,x) > > 
From: Gabriel Dos Reis <gdr@cs...>  20110424 14:16:32

Bill Page <bill.page@...> writes:  Maybe the OpenAxiom list is an appropriate place to discuss  foundational issues like this since it seems to have lesser priority  in other variants of Axiom.   One thing that has bothered me a bit lately when writing Axiom code is  the use of elt and/or apply to "simulate" a domain which in my opinion  really ought to inherit such properties from some category to which  Mapping should also belong, call it MapCat or some such. The main idea  is that members of some domain, aside from other properties, behave  like functions. There is a concept of "evaluation", i.e. applying a  function f (as a member of this domain) to members of some other  domain to yield a member form a third domain. E.g.   f in Mapping(B,A)   Then we could write   MyFunDom(): Join(MapCat(B,A), ...) ==   and   if R has MapCat(B,A) then ...   etc.   Gaby, I recall that some time ago you made some changes to the way  OpenAxiom compiles Mapping, perhaps in this direction?. Are there  plans to do further work on this? Do you see any way to reduce the  amount of adhocracy in how this is done in Axiom? Maybe MapCat or  equiv. should export apply? Does it make sense that another similar  function 'elt' exists and has similar semantics? There is an nary MappingCategory category constructor in OpenAxiom. I just did not get around to fix the instantiation of Mapping ot use it. Is that what you had in mind? Yes I plan to fix related issues. The attached works for me.  Gaby )abbrev domain MYFUN MyFunction MyFunction(T: Type): Public == Private where Public == MappingCategory(T,T) with myFunction: ((T,T) > T) > % Private == add Rep == Mapping(T,T,T) myFunction f == per f elt(f,x) == (rep f)(x,x) 
From: Bill Page <bill.page@ne...>  20110423 22:55:44

Maybe the OpenAxiom list is an appropriate place to discuss foundational issues like this since it seems to have lesser priority in other variants of Axiom. One thing that has bothered me a bit lately when writing Axiom code is the use of elt and/or apply to "simulate" a domain which in my opinion really ought to inherit such properties from some category to which Mapping should also belong, call it MapCat or some such. The main idea is that members of some domain, aside from other properties, behave like functions. There is a concept of "evaluation", i.e. applying a function f (as a member of this domain) to members of some other domain to yield a member form a third domain. E.g. f in Mapping(B,A) Then we could write MyFunDom(): Join(MapCat(B,A), ...) == and if R has MapCat(B,A) then ... etc. Gaby, I recall that some time ago you made some changes to the way OpenAxiom compiles Mapping, perhaps in this direction?. Are there plans to do further work on this? Do you see any way to reduce the amount of adhocracy in how this is done in Axiom? Maybe MapCat or equiv. should export apply? Does it make sense that another similar function 'elt' exists and has similar semantics? Bill Page. 
From: Gabriel Dos Reis <gdr@cs...>  20110421 18:12:10

"Prof. Dr. Johannes Grabmeier" <johannes@...> writes:  thanks Waldek for your quick answer, indeed, in generalizing code I had added to a category   if R has characteristic() = 2 then 1. you are abusing the `has' notation :) 2. it is wellknown that the Spad compiler (from all AXIOM flavors) is currently limited in the kind of predicates it can handle at the category level. Some students who took my class on abstract interpretation worked on that issue in 20082009, but they never finished the implementation. :/   xor: (%, %) > %   ++ xor(b,c) = b+c  componentwise in R   oplus: (%, %) > %   ++ xor(b,c) = b+c  componentwise in R   which caused the problem when compiling a domain for this category.   If neccessary, I can send you all the code, actually, it is quite a bit.    I guess this kind of attribute is not allowed. 
From: Gabriel Dos Reis <gdr@cs...>  20110413 21:31:21

Waldek Hebisch <hebisch@...> writes:  Gabriel Dos Reis wrote:  >  > Waldek Hebisch <hebisch@...> writes:  >  >  Gabriel Dos Reis wrote:  >  >  >  > Bill Page <bill.page@...> writes:  >  >  >  > [...]  >  >  >  >  >=A0However defining 'x/0' does not  >  >  > really change properties of field: normal field axioms only  >  >  > say what happens when you divide by nonzero element.  >  > =20  >  >  If the inverse of 0 is 0 then the domain should not even be a Group  >  >  let alone a Field.  >  >  >  > I am not sure that is the real issue.  >  >  >  > The real problem is if you take that axiom, what parts of the usual  >  > classical theorems remain true and to what extent?  >  > Anybody wants to make the function  >  >  >  > x +> exp(1/x^2)  >  >  >  > discontinue at x=?  >   >  A little nitpick: precise traditional definition of such function  >  is 'exp(1/x^2) for x ~= 0, 0 for x = 0'. This definition does  >  not depend on what happens with '1/x' at x = 0.  >  > The operational keyword is *discontinue*.  >  > If you make 1/0 = 0 then, by definition, the function  >  > x +> exp(1/x^2)  >  > is defined everywhere, including at 0 where it takes the value 1, not 0.  > And that definition is just as precise as it can get.  >  >  > How much of Real Analysis do you have to redefine?  >   >  If you mean Analysis in informal sense then basicaly nothing. If  >  > I mean the body of knowledge accumulated under the heading of  > Real Analysis.  >  >  you mean some set of theorems encoded in mechanically checkable  >  formal language, then the problem is essentially of translation  >  between closely related formal languages: practice has shown  >  that seemingly trival differences may cause trouble. OTOH  >  > I'm not just looking at the practice  because I don't want to equate  > "unfamiliar" with "wrong". As a scholar, I want to look at the  > logical consequences.  >   1) I believe that '1/0 = 0' can be used as part of faithful  formalization of Real Analysis. In fact, if you are  interested in elementary part (meaning no sets, no sequences, ...)  and use logic with total functions than there seem to be  no good alternative.  2) As practicioner of Real Analysis I am not interested in conseqences  of '1/0 = 0'  as I wrote I believe that they do not affect  important matters (in particular system remains consistent).  Of course you may have different opinion. And you are entitled to your belief :) And clearly there are at least as many interests as mathematicians. As a trained differential geometer using formal systems to "algebraize" topological and differential concepts, I am interested in the consequences of the various formal axioms. For example, if I take a system that tries to formalize (as an algebraic construction) the notion of limit [1] and come to some formal rules where I can do lim(f/g) = lim(f)/lim(g), it is not obvious a priori that the axiom 1/0 = 0 is entirely inconsequential. One might wish it is inconsequential, but that is only a wish or a belief and we hope our computation algebra systems do not engage in wishful thinking. [1] Michael Beeson and Freek Wiedij "The meaning of infinity in calculus and computer algebra systems" http://dx.doi.org/10.1016/j.jsc.2004.12.002   Coming back to 'exp(1/x^2)': with '1/0 = 0' this function  formally is discontinuous. Informal reaction is that Formal computer systems do not have "informal reactions". If that expression is buried deep in some intermediary computation that a human does not readily have access to, it is unlikely that one would "informal" react in a timely manner to assess whether that formal or informal continuity would affect the rest of the computation or not.  you either have wrong definition or ask wrong question  (note that informally uniteresting question is a kind of  wrong question). The point is that sometimes you do not  care what happens at zero and then '1/0 = 0' "works",  sometimes you care, then one has to do definition via  cases. and I think I asked # what parts of the usual classical theorems remain true and to what # extent?  >  apparently at least one such set of theorems (that of Isablelle/HOL)  >  already uses this convention, so you will have to "patch"  >  existing theorems when you want different convention.  >   >  > The notion that "it is done in Isabelle/HOL therefore it must be right"  >  > has to be tempered with the fact that Isabelle/HOL is a=20  >  > *logical framework* in which one develops logics. What is often left  >  > underappreciated is that there are many logics used to prove this and  >  > that theorem, but we don't have yet a coherent set of logics to  >  > handle all that has been accomplished in computational mathematics.  >  > Of course, if you are into Calculemus, you already know this.  >  >  >   >  As I wrote in another message: there is no _logical_ problem  >  with 1/0 being 0.  >  > I don't think I ever suggested there is a fundamental logical problem  > with 1/0  0. However, what I do suggest is that I've not yet seen a  > single logical framework that contains all the "conventions" (that make  > some proofs go through nicely, even if they are not conventional)  > in a single place that handles Real Analysis. I've seen bits and pieces.   I do not think you will find a single logical framework that directly  contains all popular conventins. Notice that I am not talking about notation conventions, but definitional conventions. I do not know how you measure "popular conventions", but I would go with the conventions in Bourbaki adaquately amended by Geddes et al, as a start.  IMHO various conventions are more  like macros in programing languages: they are created to fit  single problem (or domain) and are too specialised to work in  general. I have the odacity to believe that the definitional conventions by Bourbaki is more that just "macros in programming languages" created to fit single problem or domain and are too specialised to work in general :)  Logical framework may (and probably should) contain  a preprocessor to expand statements into canonical form. One  can imagine predefined "macro files" with conventions for  various domains.   Let me add that IMHO when talking about logical framework for  some part of mathematics like Real Analysis one needs mechanical  checking (people are resonably good at inventing and writing  down proofs, but formal checking is too tedious for them). absolutely.  And doing Real Analysis really means doing all mathematics. I would not go as far as saying "all mathematics". Bourbaki left a good part of geometry from its treatment of Real Analysis.  AFAICS current checking systems are limited. One problem  is that to give short proof one needs large volume of  preexisting knowledge (theorems). Connected problem is  that proofs encoded in procedural systems are hard to  read for even for specialists. Some people seem to believe  that if we keep encoding existing theorems in existing  systems then eventually system will have enough "base  knowledge" to allow writing real research results. :)  I somewhat doubt this: IMHO proof checking systems  should process mathematics in smarter ways. we all agree; getting there, however, is distinctly nontrivial. Our conventional practice of mathematics is highly ambiguous  it always amazes me that we manage to get through. I learnt quite a few things from an experiment conducted with colleagues: mechanization of the operational semantics of some advanced object oriented programming language features. I learnt quite a few things from that experiment http://parasol.tamu.edu/~gdr/C++/layout/popl11.pdf http://gallium.inria.fr/~tramanan/cpp/objectlayout/ * Technologies available in modern PA/ATP systems are quite advanced  compared to the bad press they occasionaly get. But we have a long way to go. * Proof intended for machines is no proof intended for humans. :)  It seems  that when dealing with logic current systems are  more capable than humans. But humans works at many levels:  pragmatics (what is doable and what is intersting),  procedural, logical. Also, people seems to be better  at searching/recalling relevant existing knowledge. Sure. 
From: Waldek Hebisch <hebisch@ma...>  20110413 20:44:21

Gabriel Dos Reis wrote: > > Waldek Hebisch <hebisch@...> writes: > >  Gabriel Dos Reis wrote: >  > >  > Bill Page <bill.page@...> writes: >  > >  > [...] >  > >  >  >=A0However defining 'x/0' does not >  >  > really change properties of field: normal field axioms only >  >  > say what happens when you divide by nonzero element. >  > =20 >  >  If the inverse of 0 is 0 then the domain should not even be a Group >  >  let alone a Field. >  > >  > I am not sure that is the real issue. >  > >  > The real problem is if you take that axiom, what parts of the usual >  > classical theorems remain true and to what extent? >  > Anybody wants to make the function >  > >  > x +> exp(1/x^2) >  > >  > discontinue at x=? >  >  A little nitpick: precise traditional definition of such function >  is 'exp(1/x^2) for x ~= 0, 0 for x = 0'. This definition does >  not depend on what happens with '1/x' at x = 0. > > The operational keyword is *discontinue*. > > If you make 1/0 = 0 then, by definition, the function > > x +> exp(1/x^2) > > is defined everywhere, including at 0 where it takes the value 1, not 0. > And that definition is just as precise as it can get. > >  > How much of Real Analysis do you have to redefine? >  >  If you mean Analysis in informal sense then basicaly nothing. If > > I mean the body of knowledge accumulated under the heading of > Real Analysis. > >  you mean some set of theorems encoded in mechanically checkable >  formal language, then the problem is essentially of translation >  between closely related formal languages: practice has shown >  that seemingly trival differences may cause trouble. OTOH > > I'm not just looking at the practice  because I don't want to equate > "unfamiliar" with "wrong". As a scholar, I want to look at the > logical consequences. > 1) I believe that '1/0 = 0' can be used as part of faithful formalization of Real Analysis. In fact, if you are interested in elementary part (meaning no sets, no sequences, ...) and use logic with total functions than there seem to be no good alternative. 2) As practicioner of Real Analysis I am not interested in conseqences of '1/0 = 0'  as I wrote I believe that they do not affect important matters (in particular system remains consistent). Of course you may have different opinion. Coming back to 'exp(1/x^2)': with '1/0 = 0' this function formally is discontinuous. Informal reaction is that you either have wrong definition or ask wrong question (note that informally uniteresting question is a kind of wrong question). The point is that sometimes you do not care what happens at zero and then '1/0 = 0' "works", sometimes you care, then one has to do definition via cases. >  apparently at least one such set of theorems (that of Isablelle/HOL) >  already uses this convention, so you will have to "patch" >  existing theorems when you want different convention. >  >  > The notion that "it is done in Isabelle/HOL therefore it must be right" >  > has to be tempered with the fact that Isabelle/HOL is a=20 >  > *logical framework* in which one develops logics. What is often left >  > underappreciated is that there are many logics used to prove this and >  > that theorem, but we don't have yet a coherent set of logics to >  > handle all that has been accomplished in computational mathematics. >  > Of course, if you are into Calculemus, you already know this. >  > >  >  As I wrote in another message: there is no _logical_ problem >  with 1/0 being 0. > > I don't think I ever suggested there is a fundamental logical problem > with 1/0  0. However, what I do suggest is that I've not yet seen a > single logical framework that contains all the "conventions" (that make > some proofs go through nicely, even if they are not conventional) > in a single place that handles Real Analysis. I've seen bits and pieces. I do not think you will find a single logical framework that directly contains all popular conventins. IMHO various conventions are more like macros in programing languages: they are created to fit single problem (or domain) and are too specialised to work in general. Logical framework may (and probably should) contain a preprocessor to expand statements into canonical form. One can imagine predefined "macro files" with conventions for various domains. Let me add that IMHO when talking about logical framework for some part of mathematics like Real Analysis one needs mechanical checking (people are resonably good at inventing and writing down proofs, but formal checking is too tedious for them). And doing Real Analysis really means doing all mathematics. AFAICS current checking systems are limited. One problem is that to give short proof one needs large volume of preexisting knowledge (theorems). Connected problem is that proofs encoded in procedural systems are hard to read for even for specialists. Some people seem to believe that if we keep encoding existing theorems in existing systems then eventually system will have enough "base knowledge" to allow writing real research results. I somewhat doubt this: IMHO proof checking systems should process mathematics in smarter ways. It seems that when dealing with logic current systems are more capable than humans. But humans works at many levels: pragmatics (what is doable and what is intersting), procedural, logical. Also, people seems to be better at searching/recalling relevant existing knowledge.  Waldek Hebisch hebisch@... 
From: Gabriel Dos Reis <gdr@cs...>  20110413 18:18:00

Waldek Hebisch <hebisch@...> writes:  Gabriel Dos Reis wrote:  >  > Bill Page <bill.page@...> writes:  >  > [...]  >  >  >=A0However defining 'x/0' does not  >  > really change properties of field: normal field axioms only  >  > say what happens when you divide by nonzero element.  > =20  >  If the inverse of 0 is 0 then the domain should not even be a Group  >  let alone a Field.  >  > I am not sure that is the real issue.  >  > The real problem is if you take that axiom, what parts of the usual  > classical theorems remain true and to what extent?  > Anybody wants to make the function  >  > x +> exp(1/x^2)  >  > discontinue at x=?   A little nitpick: precise traditional definition of such function  is 'exp(1/x^2) for x ~= 0, 0 for x = 0'. This definition does  not depend on what happens with '1/x' at x = 0. The operational keyword is *discontinue*. If you make 1/0 = 0 then, by definition, the function x +> exp(1/x^2) is defined everywhere, including at 0 where it takes the value 1, not 0. And that definition is just as precise as it can get.  > How much of Real Analysis do you have to redefine?   If you mean Analysis in informal sense then basicaly nothing. If I mean the body of knowledge accumulated under the heading of Real Analysis.  you mean some set of theorems encoded in mechanically checkable  formal language, then the problem is essentially of translation  between closely related formal languages: practice has shown  that seemingly trival differences may cause trouble. OTOH I'm not just looking at the practice  because I don't want to equate "unfamiliar" with "wrong". As a scholar, I want to look at the logical consequences.  apparently at least one such set of theorems (that of Isablelle/HOL)  already uses this convention, so you will have to "patch"  existing theorems when you want different convention.   > The notion that "it is done in Isabelle/HOL therefore it must be right"  > has to be tempered with the fact that Isabelle/HOL is a=20  > *logical framework* in which one develops logics. What is often left  > underappreciated is that there are many logics used to prove this and  > that theorem, but we don't have yet a coherent set of logics to  > handle all that has been accomplished in computational mathematics.  > Of course, if you are into Calculemus, you already know this.  >   As I wrote in another message: there is no _logical_ problem  with 1/0 being 0. I don't think I ever suggested there is a fundamental logical problem with 1/0  0. However, what I do suggest is that I've not yet seen a single logical framework that contains all the "conventions" (that make some proofs go through nicely, even if they are not conventional) in a single place that handles Real Analysis. I've seen bits and pieces.  Pragmatics of theorem prover make it  quite reasonable (but prover based on partial functions and  leaving 1/0 udefined looks quite reasonable too). Pragmatics  of CAS differs very much form pragmatics of theorem prover  and for CAS getting error on 1/0 is much better. But if  somebody wants to swap computations between CAS and  theorem prover using '1/0 = 0' convention, than having  this convention also in CAS starts looking reasonable  (reasonable enough to implement special domain with such  behaviour). 
From: Waldek Hebisch <hebisch@ma...>  20110413 17:37:24

Gabriel Dos Reis wrote: > > Bill Page <bill.page@...> writes: > > [...] > >  >=A0However defining 'x/0' does not >  > really change properties of field: normal field axioms only >  > say what happens when you divide by nonzero element. > =20 >  If the inverse of 0 is 0 then the domain should not even be a Group >  let alone a Field. > > I am not sure that is the real issue. > > The real problem is if you take that axiom, what parts of the usual > classical theorems remain true and to what extent? > Anybody wants to make the function > > x +> exp(1/x^2) > > discontinue at x=? A little nitpick: precise traditional definition of such function is 'exp(1/x^2) for x ~= 0, 0 for x = 0'. This definition does not depend on what happens with '1/x' at x = 0. > How much of Real Analysis do you have to redefine? If you mean Analysis in informal sense then basicaly nothing. If you mean some set of theorems encoded in mechanically checkable formal language, then the problem is essentially of translation between closely related formal languages: practice has shown that seemingly trival differences may cause trouble. OTOH apparently at least one such set of theorems (that of Isablelle/HOL) already uses this convention, so you will have to "patch" existing theorems when you want different convention. > The notion that "it is done in Isabelle/HOL therefore it must be right" > has to be tempered with the fact that Isabelle/HOL is a=20 > *logical framework* in which one develops logics. What is often left > underappreciated is that there are many logics used to prove this and > that theorem, but we don't have yet a coherent set of logics to > handle all that has been accomplished in computational mathematics. > Of course, if you are into Calculemus, you already know this. > As I wrote in another message: there is no _logical_ problem with 1/0 being 0. Pragmatics of theorem prover make it quite reasonable (but prover based on partial functions and leaving 1/0 udefined looks quite reasonable too). Pragmatics of CAS differs very much form pragmatics of theorem prover and for CAS getting error on 1/0 is much better. But if somebody wants to swap computations between CAS and theorem prover using '1/0 = 0' convention, than having this convention also in CAS starts looking reasonable (reasonable enough to implement special domain with such behaviour).  Waldek Hebisch hebisch@... 
From: Gabriel Dos Reis <gdr@cs...>  20110409 01:27:51

Bill Page <bill.page@...> writes: [...]  > However defining 'x/0' does not  > really change properties of field: normal field axioms only  > say what happens when you divide by nonzero element.   If the inverse of 0 is 0 then the domain should not even be a Group  let alone a Field. I am not sure that is the real issue. The real problem is if you take that axiom, what parts of the usual classical theorems remain true and to what extent? Anybody wants to make the function x +> exp(1/x^2) discontinue at x=0? How much of Real Analysis do you have to redefine? The notion that "it is done in Isabelle/HOL therefore it must be right" has to be tempered with the fact that Isabelle/HOL is a *logical framework* in which one develops logics. What is often left underappreciated is that there are many logics used to prove this and that theorem, but we don't have yet a coherent set of logics to handle all that has been accomplished in computational mathematics. Of course, if you are into Calculemus, you already know this.  Gaby 
From: Gabriel Dos Reis <gdr@cs...>  20110409 00:59:36

[ replying late. ] Bill Page <bill.page@...> writes:  Gaby,   Is this a typo? Or a recent change? A typo  sorry.   As far as I can see VectorSpace *does* export dimension with a result  in CardinalNumber. I suppose that in most usages is it simply  converted to NNI.   Regards,  Bill Page.   On Thu, Mar 24, 2011 at 7:31 PM, you wrote:  >  > I have always considered it a weakness that VectorSpace did not use  > CardinalNumber for dimension  even if for all practical purposes  > NonNegativeInteger is sufficient and more efficient. That, in my  > opinion, calls for an efficient abstraction, e.g. find a way to  > support CardinalNumber and make the common cases as efficient as  > NonNegativeInteger.  > 