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

Discussion in 'Python' started by Xah Lee, Aug 31, 2009.

  1. Xah Lee

    Xah Lee Guest

    • Math Notations, Computer Languages, and the “Form” in Formalism
    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
     
    Xah Lee, Aug 31, 2009
    #1
    1. Advertising

  2. Xah Lee

    slawekk Guest


    > 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.

    Slawekk
     
    slawekk, Sep 5, 2009
    #2
    1. Advertising

  3. Xah Lee

    Xah Lee Guest

    2009-09-07

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

    ☄
     
    Xah Lee, Sep 7, 2009
    #3
  4. Xah Lee

    fortunatus Guest

    fortunatus, Sep 8, 2009
    #4
  5. Musatov
    Search for
    Math Notations, Computer Languages, and the “Form †in Formalism  
    (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 ... Aug 31 by Xah Lee
    - 4 messages - 3 authors Math Notations, Computer Languages, and the
    “ Form†in Formalism   Aatu Koskensilta sci
    math Xah Lee <> writes: • 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 ... Aug 31 by Aatu Koskensilta - 4 messages - 3 authors
    This Week's Finds in Mathematical Physics (Week 279)   To see this,
    note that any guy in h_2(K) has this form: A = t+xy y* tx where t and
    x are real elements of K, and y is an arbitrary element. .... They
    formulated a supersymmetric model in 6 dimensions using the
    quaternions, and speculated about a similar formalism in 10 dimensions
    using the octonions: 6) Taichiro ... Sep 6 by Androcles - 4 messages -
    3 authors Math Notations, Computer Languages, and the “ Form†in
    Formalism   Aatu Koskensilta sci math David C
    Ullrich <> writes: Nonsense, surely. Pure
    nonsense, no doubt. But are you really certain that there's no
    nonsense out there that's even more pure? Not really. I'm just winging
    it. -- Aatu Koskensilta () "Wovon mann ... Sep
    1 by Aatu Koskensilta - 4 messages - 3 authors Math Notations,
    Computer Languages, and the “Form†in Formalism   David C Ullrich
    sci math On Mon, 31 Aug 2009 17:12:20 +0300, Aatu
    Koskensilta wrote: Xah Lee <> writes: • 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 ... Aug 31 by David C Ullrich - 4 messages - 3
    authors   ‪‬   fortunatus wrote:
    > On Sep 7, 3:06 pm, Xah Lee <> wrote:
    > ...
    > > • systems for displaying math, such as TeX, Mathematica, MathML,
    > > should be unified as part of the computer language's syntax.

    > ...
    > > ☄

    >
    > to that end you might be interested in Fortress at Sun:
    >
    > http://projectfortress.sun.com/Projects/Community
    > http://research.sun.com/projects/plrg/fortress.pdf
    > http://research.sun.com/spotlight/2007/2007-01-10_fortress.html

    Math Forum Discussions - sci.math.*"Form" in Formalism. David C.
    Ullrich. sci.math. 8/31/09. 1 ... subnazi musatov decides what's good
    for all --with no one's permission. adamk.
    sci.math ...www.mathforum.com/kb/forumcategory.jspa?
    categoryID=16&start=45 Discussions - sci.math | Google GroupsMusatov
    (3 authors) 3:18am. Heavy water is water nonetheless. 67 new of 67 ...
    Math Notations, Computer Languages, and the "Form" in Formalism. 2 new
    of 2 ...groups.google.fm/group/sci.math/topics?gvc=2&hl=en
    Discussions - sci.math | Google GroupsBy Musatov - 6:27pm - 5 new of 5
    messages ... Math Notations, Computer Languages, and the "Form" in
    Formalism ... Languages, and the "Form" in
    Formalism ...groups.google.co.zw/group/sci.math/topics?
    start=10&hl=en&sa=N Discussions - sci.math | Google GroupsMath
    Notations, Computer Languages, and the "Form" in Formalism. 3 new of 3
    - Sep 1 ... subnazi musatov decides what's good for all --with no
    one's permission ...groups.google.jo/group/sci.math/topics?
    hl=en&start= Sotheby's - Auctions - Calendar - Modern and
    Contemporary Russian Art... accusations of formalism (which the state
    defined as the focus on the formal ... 48 he took some drawing classes
    in the art studio led by S. N. Ivashev-Musatov. ...sothebys.com/app/
    live/lot/LotDetail.jsp?...&live_lot_id=24 Seismic Wave Field in the
    Vicinity of Caustics and Higher-Order Travel ...In this section we
    shall briefly discuss the main formalism (some details can be ... and
    the quadratic form in (9') is sufficient to describe the
    wave ...www.math.purdue.edu/~aduchkov/papers/duch_Studia_03.pdf
    Perturbative QCD Analysis of the Nucleon's Pauli Form Factor F...
    sophisticated formalism has ... Sudakov form factor in regulating
    possible end-point. singularities in the ... [31] I. Musatov and A.
    Radyushkin, Phys. ...www.jlab.org/~riordan/papers/e092003
    Discussions - sci.math | Google GroupsMath Notations, Computer
    Languages, and the "Form" in Formalism. 3 new of 3 - Sep 1 ... Korner:
    On the theorem of Ivasev-Musatov. II ...groups.google.com.ua/group/
    sci.math/topics?hl=pt Discussions - sci.math | Google GroupsMath
    Notations, Computer Languages, and the "Form" in Formalism. 3 new of 3
    - Aug 31 ... Korner: On the theorem of Ivasev-Musatov.
    II ...groups.google.gm/group/sci.math/topics?tsc=2 << 1234567 >>
     
    -7/9 n n + 1.76666666 + 2/, Sep 9, 2009
    #5
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. Steven T. Hatton

    C++ Formalism: any progress since n1885-6?

    Steven T. Hatton, Dec 13, 2006, in forum: C++
    Replies:
    5
    Views:
    325
    kwikius
    Dec 20, 2006
  2. Xah Lee
    Replies:
    30
    Views:
    1,847
    Peter J. Holzer
    Jun 16, 2007
  3. Xah Lee
    Replies:
    30
    Views:
    1,306
    Peter J. Holzer
    Jun 16, 2007
  4. Xah Lee
    Replies:
    32
    Views:
    649
  5. VK
    Replies:
    15
    Views:
    1,331
    Dr J R Stockton
    May 2, 2010
Loading...

Share This Page