Re: Math Notations, Computer Languages, and the “Form” in Formalism

[Xah Lee]

2009-09-07

On Sep 5, 7:41 am, slawekk <skoko... at 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/

☄