Sun Oct 4 10:16:46 CEST 2009


The previous article lead me to funmath[1].  Funmath stands for
Functional mathematics (for other uses of the name, look here).  The
underlying principle consists in defining mathematical concepts as
functions (hence the name) whenever doing so is appropriate. This
turns out to be especially convenient where it has not yet become
common practice.

The idea is to build a defect-free notation for mathematics.  It
reminds me of what Sussman is up to with his recent work on Scheme +
differential geometry.

  By formalism we mean a framework for reasoning comprising two
  elements: (a) a symbolic language or notation, (b) rules for
  symbolic manipulation.

    (a) The language is usually characterized by its form, typically
    specified by a formal syntax, and its meaning, typically specified
    by a (denotational) semantics.

    (b) The rules are typically specified by a formal system, which
    can be seen as the axiomatic semantics of the language if we
    borrow the term from programming languages.

  Gries advocates calculational reasoning. This means that logical
  arguments are presented as symbolic calculations, stepping from one
  equation to the next using appropriate rules, and linking them by

[1] http://www.funmath.be/
[2] http://www.funmath.be/LRRL.pdf
[3] http://www.cs.utexas.edu/~EWD/ewd10xx/EWD1073.PDF