[<<][compsci][>>][..]

Sun Oct 4 10:16:46 CEST 2009

## Funmath

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
(in)equalities.
[1] http://www.funmath.be/
[2] http://www.funmath.be/LRRL.pdf
[3] http://www.cs.utexas.edu/~EWD/ewd10xx/EWD1073.PDF

[Reply][About]

[<<][compsci][>>][..]