Funmath

Functional mathematics

What is a function in mathematics?

This question is answered in quite some detail (occasionally technical) in the paper Rekindling critical thinking: heeding major errors in current Introduction to Proof type textbooks. Note that this is only an initial version, prepared for MathFest 2015. All questions, comments and suggestions sent to raymond.boute@pandora.be would be much appreciated. Please note that, due to priorities, this site is maintained only very occasionally (last time was 5 years ago, and this entry is not counted as maintenance).

Introduction

What is Funmath?

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.
Funmath provides a simple and coherent framework for establishing more convenient mathematical conventions, styles of expression, exposition and (calculational) reasoning in most branches of pure and applied mathematics.

Important remark   From the preceding paragraph, it is clear that we are talking here about mathematical reasoning by humans (say, "pencil and paper") and communication among humans. In the current version of this website, we refer only occasionally to automated tools or mathematical software (e.g., when mentioning current and future work).

What is its purpose?

Funmath is designed to make the idea of letting the symbols do the work feasible and convenient in everyday mathematical practice.
This idea is nicely captured by the logo (shown on the left) of the conference series on the Mathematics of Program Construction (MPC), which is oriented towards Computer Science.
Making this idea work in a wider context, for every "working mathematician" (not "logicians only") and every engineer in classical as well as computer-related areas, requires a framework that is free of the many defects (ambiguities, abuses of notation, inconsistencies etc.) one encounters in common mathematical conventions, as discussed in a later subsection.
Funmath provides such a defect-free framework, while also preserving the "look and feel" of familiar conventions to the largest extent possible without hampering the stated purpose. It is more expressive and convenient than traditional conventions, and is eminently suitable when working just with pencil and paper or on the blackboard.

Where is it useful?

Funmath is applicable at all levels of mathematical practice, starting from the most elementary ones. However, it is most useful at the higher levels and for the mathematical modeling of systems in all branches of engineering.
In particular, in its design we paid special attention to bridging the methodological gap that has grown between classical engineering disciplines and computer science. As a result, Funmath provides a complete unifying framework for the mathematics of Electrical and Computer Engineering (ECE) --- from Antennas and Algorithms to Z-notation and z-transforms.

The formalism

In its most general sense, Funmath is a discipline for designing and using "good" conventions, notations and reasoning style in mathematics, based on defining (most) mathematical objects as functions. As such, it can be used advantageously in any existing mathematical framework. However, this view is rather open-ended without a concrete embodiment as a complete formalism and a representative collection of applications in mathematics and engineering, in particular systems modeling.
Such an embodiment has been elaborated over the past 15 years (see the history) and is the main topic of this section.

Formalisms in general

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. Here we haste to say that this amounts to generalizing the term to mathematical and specification languages, not just procedural or algorithmic ones.
Another characteristic beside syntax and semantics is pragmatics, generally speaking: the way in which a formalism is put to use in various application domains.
The "goodness" or merits of a formalism are determined by its expressive power, which includes the scope, clarity, compactness, freedom of ambiguities etc. of the language, and its manipulative power, not in the Orwellian sense as in politics, but referring to support that the rules provide in symbolic manipulation: clarity, freedom of inconsistencies, simplicity, ease of use etc.

The need for defect-free conventions in mathematics

The purpose of the formalism requires defect-free notations and conventions.
The degree to which traditional mathematics satisfies this requirement is very uneven. Typical defects are discussed in a paper by Lee and Varaiya (page 4) for classical engineering mathematics. The same defects plus others related to discrete mathematics, sets and logic are discussed in some the references below and very briefly in the Funmath LRRL (a 4-page Language Rationale and Reference Leaflet).
This is not about small matters like semicolons and commas, but about serious interference with "letting the symbols do the work". Indeed, if during symbol manipulation one has to be continuously aware of inadequacies in the notation, there is no question of the symbols doing useful work.
It is observed in the LRRL that the support for formal calculation provided by traditional conventions is inversely proportional to the needs in Computer Science.
However, even in classical mathematics, the adequacy of the conventions for symbolic calculation can be very uneven within a single area. Conventions in calculus, for instance, make calculation with derivatives and integrals rather smooth and problem-free: the rules are well-known and widely used, letting the symbols do the work. By contrast, the logical reasoning for deriving or justifying these rules is typically very informal, done with words rather than symbols, and often obscuring the structure of the argument.
This situation is aptly described in the following excerpt from Paul Taylor's website on Practical Foundations of Mathematics.

 The notation of elementary school arithmetic, which nowadays everyone takes for granted, took centuries to develop. There was an intermediate stage called syncopation, using abbreviations for the words for addition, square, root, etc . For example Rafael Bombelli ( c.  1560) would write R. c. L. 2 p. di m. 11 L       for our       3Ö{2+11i}. Many professional mathematicians to this day use the quantifiers ( ",\$) in a similar fashion, \$d > 0 s.t. |f(x)-f(x0)| < e if |x-x0| < d, for all e > 0, in spite of the efforts of [various logicians][...]   Even now, mathematics students are expected to learn complicated (e-d)-proofs in analysis with no help in understanding the logical structure of the arguments. Examiners fully deserve the garbage that they get in return.

The highlighting in red at the end was added afterwards to emphasize some educational consequences.
Taylor correctly traces back the problem to syncopation: using symbols as mere abbreviations words, without calculation rules for putting them to work. This is the manner in which the vast majority of mathematicians and engineers use quantifiers like " and \$.
One should not be too hasty in blaming them: even the best textbooks on formal logic present symbolic reasoning only at the beginning, and not in a form that is suitable for practical use in the remainder, let alone for the everyday practice of "working mathematicians" and engineers. There is no other reason why logic textbooks abandon symbolic reasoning in later chapters and treat the remaining topics (axiomatic set theory, ordinal numbers and so on) with arguments in words.
In brief, the title of Gries's paper The Need for Education in Useful Formal Logic appropriately reflects the state of affairs until shortly before its publication in in 1996.

Calculational reasoning

In the cited paper, 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. As mentioned in the introduction, this is the convenient style mathematicians are accustomed to in algebra and calculus, but now extended to logic. For the purpose of formal reasoning by humans, it has turned out to be vastly superior to what is misleadingly called "natural reasoning". For its mechanization, additional work is needed.
Many researchers and educators in Computer Science have been first experimenting and then, after inevitably becoming enthusiastic, systematically working with calculational reasoning. In his renowned EWD series of notes on Mathematics and Computing Science, the late Edsger W. Dijkstra explains How Computing Science created a new mathematical style. This is largely due to calculational reasoning Under the spell of Leibniz's dream (pp. 12-13) whereby "the symbols direct reason" in mathematical arguments. This idea is also advocated by Hilbert, who adds the following comment in his famous lecture Mathematical Problems at the International Congress of Mathematicians in 1900.

 It is an error to believe that rigor in the proof is the enemy of simplicity. On the contrary we find it confirmed by numerous examples that the rigorous method is at the same time the simpler and the more easily comprehended. The very effort for rigor forces us to find out simpler methods of proof. It also frequently leads the way to methods which are more capable of development than the old methods of less rigor.

In retrospect, when these ideas were put forward by Leibniz and Hilbert, the time was not yet ripe for their implementation in everyday mathematical practice, due to the aforementioned practical deficiencies in formal logic, also described in more detail in Gries's paper. Nowadays, however, due to the work of Dijkstra, Gries and others, it has become commonplace in the approach to Computing Science by many researchers and educators.
Funmath extends these advantages to mathematics for all areas of engineering.

Design of Funmath

As seen from the preceding discussion, a widely applicable formalism should be (a) free of defects and (b) support formal reasoning, i.e., guided by the form of the expressions rather than their meaning. Point (b) is the main criterion whereas (a), being a necessary condition, is just a consequence. Various researchers including Dijkstra and Gries were so dissatisfied with the way in which traditional conventions often interfered with formal reasoning that they advocated starting from scratch.
The design of Funmath adhered to the same stringent requirements, but revealed that the "look and feel" of familiar conventions could be salvaged (by resynthesizing) to a larger extent than originally anticipated.
Eliminating defects separately in an ad hoc fashion is obviously out of the question. Funmath avoids the defects by an orthogonal design, made possible by the Functional Mathematics principle of defining mathematical concepts as functions whenever appropriate. The resulting design can be characterizd as follows.

(a) The language has a structure that is extremely simple, as it has only four constructs (summarized in the Funmath LRRL). Yet, this amply suffices for synthesizing not only the traditional notations while preserving their familiar "look and feel" (of course, minus the ambiguities, inconsistencies, abuse of notation and other defects), but also new and useful forms of expression.

(b) The rules are calculational, making formal reasoning practical and attractive in everyday use by mathematicians and engineers. They are convenient for calculation "by hand" or on the blackboard, and amenable to automation (but the latter is not essential to their usefulness).

The reasoning framework has two main elements.
First, concrete generic functionals support smooth transition between pointwise and point-free formulations (i.e., with and without variables). It facilitates calculation with functionals and exploiting formal commonalities between mathematical models in the various areas of classical and computer engineering.
Second, a functional predicate calculus makes formal logic practical for everyday use by mathematicians and engineers, allowing them to calculate with predicates and quantifiers as fluently as they have learned to do with derivatives and integrals.
For the complete picture, we refer to the sources of information below.

History

 (this section, if completed, will be a short overview only)

References regarding Funmath

There are three groups of references: a short list with course materials, one for tutorials and seminars, and one (subdivided) for research publications.

Course materials

Here only the most recent versions are shown, available for immediate display.

In a future textbook version, these documents will be merged, some of the technicalities at the beginning reduced, and more applications (in different areas) will be added. The additions will make the amount of material too large for a single course, but are meant to allow lecturers to select topics for particular courses.

Tutorials and seminars

The named links refer to the organizers; the links marked [view] allow viewing the images of the presentations (all in pdf). Presentations for tutorials (1/2 day or a full day) are usually much lengthier than for seminars (about 1 hour). Inevitably there is a considerable overlap, especially in the initial parts outlining the fundamentals.

Research publications

Only publications related to Funmath are listed; other (older) publications can be found at a different website (neglected and incomplete). The lists will initially mention mainly recent documents; older ones will be gradually be added at the end as time permits. Overlap in content is kept minimal.
The named links refer to the title of the article and the journal or conference; the links marked [view] display the images of the presentations (all in pdf) and via [ask copy] a copy of the paper itself can be obtained from the author.

Publications about fundamentals (also containing many small application examples in diverse areas for illustration and clarification)

Application-oriented publications (exploring applications in specific areas)

Implementation-oriented and comparative work

About education in formal methods or Computer Science in general

Spin-off papers  Here are some results on calculational or conceptual simplification and other issues. The first paper eliminates the "weirdness" in the traditional definitions of the decibel, and makes dB into a first-class mathematical function alongside the exponential, suitable for clean algebraic-style calculation. The next two papers show how some classical problems that are traditionally presented as requiring calculus can be solved by elementary high-school geometry, which is arguably simpler. The last paper shows how the familiar positional representation of nonzero integers is equally well possible without the digit 0.

• Raymond Boute, "The decibel done right: a matter of engineering the math", IEEE Antennas and Propagation Magazine, Vol. 51, No. 6, pp. 177-184 (Dec. 2009)
• Raymond Boute, "Simple geometric solutions to De l'Hospital's pulley problem", The College Mathematics Journal, Vol. 30, No. 4, pp. 311-314 (Sept. 1999)
• Raymond Boute, "Moving a rectangle around a corner: geometrically", The American Mathematical Monthly, Vol. 111, No. 5, pp. 435-437 (May 2004)
• Raymond Boute, "Zeroless positional number representation and string ordering", The American Mathematical Monthly, Vol. 107, pp. 437-444, (May 2000)

Doctoral dissertations  Only dissertations pertaining to Funmath are included here; others can be found at a different website (neglected and incomplete). This work was supervised by Raymond Boute, in some cases jointly with a colleague as mentioned.
Important remark  Dissertations until 1998 reflect the state of Funmath when only language design was explored; the formal calculation rules were a later development.

• Johan Hoffman, Declaratieve specificatie en transformationeel ontwerp van software-systemen (Declarative Specification and Transformational Design of Software Systems), Universiteit Gent (1998)
• Frank van den Beuken, A Functional Approach to Syntax and Typing, Nijmegen University; copromotor: H. A. van Thienen (1997)
• Mieke Massink, Functional Techniques in Concurrency, Nijmegen University; copromotor: D. Pedreschi, University of Pisa (1996) [gzipped postscript]
• Marc Seutter, The Development of Semantic Functions for a System Description Language with Multiple Interpretations, Nijmegen University (1994)
• Huub van Thienen, It's about time -- Using Funmath for the Specification and Analysis of Discrete Dynamic Systems, Nijmegen University (1994)
• Jozef De Man, Systems Engineering Using a Functional Language, Leuven University; promotors: Johan Lewi, Raymond Boute (1994)
• Cees van Reeuwijk, The Implementation of a Systems Description Language and its Semantic Functions, Delft University; promotors: Jan Davidse, Raymond Boute (1991)

 Formal Methods Week Nov. 2-6, 2009, Eindhoven, The Netherlands. Fifteen co-located symposia, workshops and other FM-related events including the 16th Symposium / 2nd World Congress on Formal Methods

The Nijmegen Connection   Links to related research by former students (some of them now working elsewhere) and by colleagues at the University of Nijmegen, where I worked as a full professor from 1981 to 1994.

• Mieke Massink, who is also a member of the Formal Methods && Tools Group in Pisa, Italy. This group is active in the fields of development and application of formal notations, methods and software support tools for the specification, design and verification of complex computer systems.
• Frits Vaandrager, head of the Informatics for Technical Applications group at Nijmegen University. This group is doing research on formal methods and tools for embedded systems and protocols.
• Henk Barendregt, head of the The Foundations Institute for Computing and Information Sciences at Nijmegen University. This group studies mathematical theories concerned with computability, provability and complexity. Henk Barendregt also initiated the Automath Archive in honour of prof. N. G. De Bruijn, one of the founding fathers of the automated proof checking community.
• Freek Wiedijk, who is currently working with Henk Barendregt on formalizing selected parts of mathematics and comparative study of automated proof checkers and assistants. He has an interesting site with updates on the list of 100 theorems offered on the web as benchmarks for theorem proving.

Links related by name, not subject matter   The following links are not related to Functional Mathematics, yet are mentioned here because they also use the name funmath (or similar) for projects or products related to mathematics.

Not related to mathematics is FunMath.com a site (in French) for finding products of all kinds via the web.

Acknowledgement   The logo UT FACIANT OPUS SIGNA ('let the symbols do the work') is due to Johan Jeuring (for the basic idea including the Droste effect), Lambert Meertens (for the Latin translation) and Tobias Baanders (for the graphical execution).
I also thank Freek Wiedijk for his suggestion to make material on Funmath more easily available by setting up a dedicated website.

 Author: Raymond BouteMail: raymond.boute@pandora.be Site most recently updated: 2010/12/18

If you find any errors or broken links, please let me know.