2009-09-07 On Sep 5, 7:41 am, slawekk <skoko...@yahoo.com> wrote: > > Theorem provers > > such as OCaml (HOL, Coq), Mizar does math formalism as a foundation, > > also function as a generic computer language, but lacks abilities as a > > computer algebra system or math notation representation. > > Isabelle's presentation layer is well integrated with LaTeX and you > can use math notation in (presentation of) proofs.
in my previous post http://xahlee.org/cmaci/notation/index.html it was quickly written and didn't clearly bring about my point. The point is, that formalism in mathematics, consistency of math notation issues (for human), math notation language systems (TeX, Mathematica, MathML), and calculational proof movement (a la Edsger Dijkstra), and computer algebra systems, and theorem proving systems, and computer language syntax, all of the above, should be unified into one single entity, and is today very much doable, in fact much of it is happening in disparate communities, but as far as i know i do not think there's any literature that expresses the idea that they should all be rolled into one. Let me address this a bit quickly without trying to write some coherent essay. few things to note: ---------- • theorem proving systems and computer algebra systems as unified tool is very much a need and is already happening. (e.g. there's a project i forgot the name now that tries to make Mathematica into a theorem proving system a la ocaml) ---------- • theorem proving systems (isabell, hol, coq etc, “proof assistants” or “automated proof systems”) and mathematics foundation by formalism should be unified. This active research the past 30 or more years, and is the explicit goal of the various theorem proving systems. ---------- • math notation consistency issues for human communication, as the calculational proof movement by Dijkstra, and also Stephen Wolfram criticism of traditional notation and Mathematica's StandardForm, is actually one single issue. They should be know as one single issue, instead of Calculational Proof movement happening only in math pedagogy community and Mathematica in its own community. ---------- • math notation issues and computer language syntax and logic notation syntax is also largely the same issue. Computer languages, or all computer languages, should move towards a formalized syntax system. I don't think there's much literature on this aspect (in comparison to other issues i mentioned in this essay). Most of today's computer languages's syntax are ad hoc, with no foundation, no consistency, no formal approach. e.g. especially bad ones are Ocaml, and all C-like langs such as C, C++, Java. Shell langs are also good examples of extremely ad hoc: e.g. bash, perl, PowerShell. There are langs that are more based on a consistent syntax system that are more or less can be reduced to a formal approach. Of those i know includes Mathematica, XML (and lots derivatives e.g. MathML) and lisps also. Other langs i don't know much but whose syntax i think are also close to a formal system are: APL, tcl. My use of the phrase “syntax with formal foundation” or “syntax system” is a bit fuzzy and needs more thinking and explanation... but basically, the idea is that computer language's syntax can be formalize in the same way we trying to formalize mathematics (albeit the problem is much simpler), so that the syntax and grammar can be reduced to few very simple formal rules in parsing it, is consistent, easy to understand. Mathematica and XML are excellent examples. (note here that such syntax system does not imply they look simple. Mathematica is a example.) the following 2 articles helps in explaining this: • The Concepts and Confusions of Prefix, Infix, Postfix and Fully Nested Notations http://xahlee.org/UnixResource_dir/writ/notations.html • Fundamental Problems of Lisp http://xahlee.org/UnixResource_dir/writ/lisp_problems.html ---------- • systems for displaying math, such as TeX, Mathematica, MathML, should be unified as part of the computer language's syntax. The point is that we should not have a lang just to generate the display of math notations such as done by TeX or MathML or Microsoft equation editor or other tools. Rather, it should be part of the general language for doing math. (e.g. any computer algebra system or theorem proving system) A good example that already have done this since ~1997 is Mathematica. practically speaking, this means, when you code in a language (say, Ocaml), you don't just write code, but you can dynamically, interactively, have your code display math 2D notations, and the info about formating the notation is part of the computer language, it's just that your IDE or specialized editor understand your language and can format it to render 2D notations on the fly (e.g. HTML is such a lang). If you know Mathematica, then you understand this. Otherwise, think of HTML/XML, which is a lang for formatting purposes without computational ability, yet today there are XML based general purpose computer languages. This language is a example of several issues in this essay. i.e. it's syntax is formalized syntax system, it's is a general purpose computer language, and it has semantics for 2D notations or arbitrary formatting/rendering such as headers. ---------- As a example of current situation in contrast of the above idea: suppose you doing some proof using OCaml derived theorem prover. Sometimes you need to do computer algebra, so you need to call Mathematica or Maple as supplement. Then often you need to display the result in math notation. So you'll need to call/output TeX or MathML. Then Dijkstra objects that your traditional math notation is so inconsistent, ambiguous, misleading, ad hoc, and does not help or correspond to the actual mathematical content behind them. So, you need to invent or re-write your notation to something proposed by the Calculational Proofs movement or Stephen Wolfram's (proprietary) Mathematica's StandardForm, that is not ambiguous. ---------- I think what inspired me to arrive at this idea is mostly my experiences with Mathematica, and my interest in math formalism and logicism as foundation, and my interest in technologies such as computer algebra systems and display systems such as MathML and TeX, and the intricate issues of relation between math notations and mathematics. This may sounds like pitching Mathematica, but as far as i know it is closest as the best example in unifying all these issues. It is a has a simple syntax system (i.e. the lang's syntax & grammar is not ad hoc). It is a general computer language. It is a computer algebra system (e.g. can solve math equations, etc.). The language also functions as a math notation display system (e.g. like TeX or MathML). It has a notation (StandardForm) that is compatible with the calculational proof movement. What it lacks is functioning as a theorem proving system. I'm singling out Mathematica because it is a system i know well and happened to be the most fitting example in this thesis. Note however, Mathematica is roughly the sole idea of Stephen Wolfram, and its syntax/grammar, is not the only approach. It just happens to be the lang that today has unified many of the issues in this essay (as far as i know). It is relatively easy to design alternative syntax. Many approaches to this unified language/syntax/notation/mathematics system are possible. Different communities mentioned above are trying to unify or advance different aspects. (e.g. as another example i haven't mentioned above, there's a project in LaTeX that tries to make its syntax understand the semantics of math notations, as opposed to sequence of structurally meaningless symbols that renders to meaningless display... Lots other examples in different tools really) i'll have to refine this essay for coherency and more concrete examples, perhaps with screen shots from different tools, syntax examples in different languages, rendered output in different tools, notation comparison from different schools, philosophies in formalism or logicism or computer proofing systems from different mathematicians, pertinent quotations and excerpts from various literatures, and more academic references and industrial publications... but i hope this idea is conveyed reasonably. Xah ∑ http://xahlee.org/ ☄ -- http://mail.python.org/mailman/listinfo/python-list
