X

#### Xah Lee

http://xahlee.org/cmaci/notation/index.html

plain text version follows. (lacks links)

-----------------------------

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

Xah Lee, 2009-08-31

This page is a collection of essays and expositions on the subjects of

nomenclature and notations in math and computer languages, in the

context of facilitating human communication and theorem proving

systems.

Most of these essays here are originally from email, blogs, or rants.

They are not of publication quality, and they are not a coherent

exposition the subject. Here's a very brief summary of of these

essays's central thesis:

• Traditional math notations are very inconsistent. Edsger Dijkstra is

a leader in a movement of what's called Calculational Proofs. That is,

using a notation that is consistent and facilitates the calculation

aspects when doing math by humans.

• Today, especially since 1990s, tremendous advances are made in

computer algebra systems and theorem proving systems. In these

languages, a coherent syntax, grammar, are needed for math

expressions.

• In computer algebra or theorem proving systems, they are intimately

tied to the math philosophies of formalism and logicism. In a sense,

formalism and logicism today are tied together as a single subject,

and using computer languages as foundation.

• Math expressions/syntax in computer languages are intimately tied to

math notations for human reading. (e.g. Mathematical, MathML are

technologies that combine the two.)

• The syntax and grammar of today's computer languages, such as Java,

C, Python, SQL, Lisp, are ad-hoc and their communities have little

understanding of the knowledge gained in math related fields such as

computer algebra or theorem proving languages. (This applies to

functional langs such as Haskell as well, but to a lesser degree.) On

the other hand, mathematicians in general are illiterate about

programing or using computer languages.

All of the above considered together, computer language designers and

mathematicians, should be made aware of these issues, so that when

they design or use computer languages, may it be math oriented or not,

the language's syntax and grammar can move towards a consistent syntax

system with solid foundation (as opposed to ad-hoc), and such language

should have build-in markup or simple mapping to 2-dimensional

notations for human reading (such as done with Mathematica or Semantic

MathML), and this computer language should be in fact as a basis of

theorem prover or computer algebra system (as in OCaml, Haskell,

Mathematica). The languages of computer algebra and theorem prover

would in fact merge together into one single subject if it is not

already slowly happening today.

Progress in the above issues are made in different fields but there

are little unification going on.

For example, there's Edsger Dijkstra's Calculational Proofs movement.

It improves math notations towards consistency and formalism. However,

people in Calculational Proofs movement are mostly math pedagogy

community i think. They are not programers interested in computer

languages, nor logicians interested in math formalism, or industrial

and commercial organizations interested in math notation

representation systems.

There's the computer algebra community, such as Mathematica, Maple,

Matlab, which requires a syntax and grammar for mathematical concepts.

There's the theorem proving community, such as OCaml, Coq, HOL, which

not only requires a syntax for math concepts, but also made major

understanding about math as a system of forms, i.e. formal systems.

Both computer algebra and theorem proving systems require math

notations and computer language syntax that are consistent and can

represent math concepts. However, the 2 camps are largely separate

communities. For example, there is as far as i know no tool that is

both a practical computer algebra system as well as a theorem proving

language.

Common computer languages, such as C, Java, Python, requires a good

syntax, parsers, and compilers, but their community, including

computer scientists and programers, are usually illiterate in typical

topics of of mathematics proper. Functional languages, such as Scheme

Lisp, APL, OCaml, Haskell, are more based on logic foundations (lambda

calculus) but their syntax and grammar has little to do with the math

notations as a logic or formal system. (these languages do not have a

formal spec in the sense of Formlism, i.e. transformation of forms. In

fact, almost no languages has a formal spec, formalism or not.)

There's math notation representation needs, such as TeX, MathCAD,

MathML, Mathematica. These are typically commercial organizations in

the computing industry. They can render math notations. In the case of

MathML and Mathematica, the language also represent the semantic

content of math notations. These two made major understanding about

the relation of math notations and computer languages, but they in

general have little to do with formalism or theorem proving. (with

some exception of Mathematica)

Calculational proof notational system, Computer algebra systems,

theorem prover languages, formalism and logicism as foundation of

mathematics, functional languages, and computer languages in general,

mathematics and its notations, all are in fact can be considered as a

single subject with a unified goal. All the technologies and movements

exist, but today they have mostly not come together. For example,

Microsoft Equaton Editor, TeX, and various other tools does well with

math notation rendering. MathML has both representational and semantic

aspects (OpenMath is a new group that focus on semantic aspects), for

the purpose of rendering as well semantic representation. Mathematica

is a computer algebra system for solving arbitrary math equations,

that is also able to represent math notation as a computer language,

so that computation can be done with math notation directly. However,

the system lacks a foundation as a theorem prover. 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.

Notations

* The Codification of Mathematics

* State Of Theorem Proving Systems 2008

* The Problems of Traditional Math Notation

* A Notation for Plane Geometry

* the Moronicity of the Expositions of Common Mathematicians

(rant)

* Fundamental Problems of Lisp (see section 1, on the importance

for regularity of syntax)

* The Concepts and Confusions of Prefix, Infix, Postfix and Fully

Functional Notations

* The Moronicities of Typography

Jargons

Math

* Math Terminology and Naming of Things

* Math Jargons Explained

* Politics and the English Language, 1946, by George Orwell.

Harm Of Bad Terminologies In Computing Languages

* The Importance of Terminology's Quality In A Computer Language

* What are OOP's Jargons and Complexities?

* Java's Abuse of the Jargon “Interface” and API

* Jargons of Info Tech Industry

* The Term Currying In Computer Science

* Function Application is not Currying

* Why You should Not Use The Jargon Lisp1 and Lisp2

* The Jargon “Tail Recursion”

* What Is Closure In A Programing Language

* Jargons And High Level Languages (unpolished essay)

* Why You Should Avoid The Jargon “Tail Recursion”

* I Can Not Find A Word Better Than “CAR”

Harm of Mixing Concept of Syntax and Formatting

* The TeX Pestilence

* The Harm of hard-wrapping Lines (harm of confusing syntax with

formatting)

* Tabs versus Spaces in Source Code (harm of treating syntax as

formatting instead of syntax)

Applications of Regular Syntax

* A Text Editor Feature: Syntax Tree Walk (application of syntax)

* A Simple Lisp Code Formatter (application of syntax regularity)

References

* “Mathematica Notation: Past and Future” (2000-10-20), by Stephen

Wolfram, at http://www.stephenwolfram.com/publications/recent/mathml/index.html.

* Functional Mathematics, by Raymond Boute, 2006. http://www.funmath.be/

* Formalized Mathematics, by John Harrison, 1996-08-13.

http://www.rbjones.com/rbjpub/logic/jrh0100.htm

* “How Computing Science created a new mathematical style”. (1990)

By Edsger W Dijkstra. EWD1073

* “Under the spell of Leibniz's dream” (2000) By Edsger W

Dijkstra. EWD1298

* Abuse of notation

* Formal system