Funmath

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

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.

• The Funmath LRRL (Language Rationale and Reference Leaflet), a 4-page quick reference guide for students. This layout is for printing on one sheet of paper (settings: landscape, flip on short edge) and folding.
• Functional Mathematics: A Unifying Formal Approach to Modelling Systems, Circuits and Programs -- Part I, course notes for students in Electrical and Computer Engineering. It has many exercises at the end of each chapter, and is written to be made into a textbook later (as time permits).
• Formal Logic for Practical Use -- A Calculational Approach, course notes for students in Computing Science (first part of a course on Formal Semantics). It is an "extended subset" of the preceding document, but contains no exercises (problems for each chapter are posted at the course website).

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.

Tutorials

• R. Boute, "Formal Methods and Signal Processing", Tutorial T5 at the 15th International Symposium on Formal Methods (FM08), Turku, Finland (May 2008)
• R. Boute, "Formal Methods as a Unifying Basis for Electrical and Computer Engineering", Tutorial 14 at the Formal Methods Conference (FM05), Newcastle upon Tyne, UK (July 2005)
• R. Boute, "Functional Predicate Calculus and Generic Functionals in Software Engineering", Tutorial 6 at the First International Colloquium on Theoretical Aspects of Computing (ICTAC2004), Guiyang, China (Sept. 2004)
• R. Boute, "Formal Reasoning about Systems, Software and Hardware", Tutorial 11 at the 18th World Computer Congress (WCC2004), Toulouse, France (Aug. 2004) [ask text version]
• R. Boute, "Formal calculation with Functions, Predicates and Quantifiers in Software, Computer and Electronics Engineering", Tutorial at the International Conference on Software Engineering and Formal Methods (SEFM2003). Brisbane, Australia (2003)

Seminars

• R. Boute, "Formal Calculation as a Tool for Discovery", NIII Colloquium, University of Nijmegen, The Netherlands (2006/02/15)
• R. Boute, "Formal Calculation as a Tool for Discovery", Seminarie Departement Computerwetenschappen, Leuven University (2006/02/14)
• R. Boute, "Making CS and classical EE meet: unification by formalization", Stanford CSL Colloquium, Computer Systems Laboratory, Stanford University (2004/10/13)
• R. Boute, "Formal Methods unifying Computing Science and Systems Theory", CHESS Seminar, Center for Hybrid and Embedded Software Systems, Berkeley University (2004/10/12)
• R. Boute, "Formal Calculation Unifying Engineering Theories Beyond Software", Summer School Marktoberdorf (2004/08/13)

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)

• Raymond Boute, "Functional Declarative Language Design and Predicate Calculus: a Practical Approach", ACM Transactions on Programming Languages and Systems, Vol. 27, No. 5, pp. 988-1047 (Sep. 2005) [ask copy]
• Raymond Boute, "Concrete Generic Functionals: Principles, Design and Applications". In: Jeremy Gibbons and Johan Jeuring (Eds.), Generic Programming, pp. 89--119. Kluwer (2003) [view] [ask copy]
• Raymond Boute, "Supertotal Function Definition in Mathematics and Software Engineering", IEEE Transactions on Software Engineering, Vol. 26, No. 7, pp. 662--672 (Jul. 2000) [ask copy]

Application-oriented publications (exploring applications in specific areas)

• Raymond Boute, "Making Temporal Logic Calculational: A Tool for Unification and Discivery", in:Ana Cavalcanti and Dennis Dams (Eds.), Proc. Second World Congress on Formal Methods (FM2009), Eindhoven, The Netherlands, Nov. 2-6, 2009, Springer LNCS, vol. 5850, pp. 387-402. Springer (2009) (best paper award) [ask copy]
• Raymond Boute, "Simple gedanken experiments in leveraging applications of formal methods", in: Tiziana Margaria and Bernhard Steffen (Eds.), Proc. 3rd Intl. Sympos. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008), Porto Sani, Greece, October 13-15, 2008, Springer CCIS, vol. 17, pp. 847-861. Springer (2008) [ask copy]
• Raymond Boute, "Calculational Semantics: Deriving Programming Theories from Equations by Functional Predicate calculus", ACM Transactions on Programming Languages and Systems, Vol. 28, No. 4, pp. 748-793 (Jul. 2006) [ask copy]
• Hannes Verlinde and Martine De Cock and Raymond Boute, "Fuzzy versus quantitative association rules: a fair data-driven comparison", IEEE Transactions on Systems, Man and Cybernetics, part B: Cybernetics, Vol. 36, No. 3, pp. 679-684 (Jun. 2006) [ask copy]
• Raymond Boute, Andreas Schäfer, "The Timer Cascade: Functional Modelling and Real Time Calculi", in: Dang Van Hung, Martin Wirsing (Eds.), Proc. 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC05), Springer LNCS 3722 (Oct. 2005) [view] [ask copy]
• Raymond Boute, "Signal Processing Functions, Algorithms and Smurfs: The Need for Declarativity". SPS-DARTS 2005 -- First annual IEEE BENELUX/DSP Valley Signal Processing Symposium, Paper #141. Antwerpen (Apr. 2005) [view paper] [view poster]
• Hannes Verlinde and Raymond Boute, "Systematic functional design of an XML editor". In: David de Frutos-Escrig, Manuel Nunez (Eds.), FORTE 2004 -- Work-in-Progress Papers, pp. 1-17 (Sep. 2004)
• Raymond Boute, "Integrating Formal Methods by Unifying Abstractions". In: Eerke A. Boiten, John Derrick, Graeme Smith (Eds.), Integrated Formal Methods: 4th International Conference, IFM 2004 Canterbury, UK. Springer LNCS 2999 (Apr. 2004). [view] [ask copy]
• Raymond Boute and Hannes Verlinde, "Functionals for the Semantic Specification of Temporal Formulas for Model Checking". In: Hartmut Koenig, Monika Heiner, Adam Wolisz (Eds.), FORTE 2003 -- Work-in-Progress Papers, pp. 23-28 (Sep. 2003)
• Hannes Verlinde, Systematisch ontwerp van XML-hulpmiddelen in een functionele taal. Master thesis, Universiteit Gent (2003)

Implementation-oriented and comparative work

• Hannes Verlinde and Raymond Boute, "A Proof Assistant for Equational Propositional Logic". Submitted to IJCAR 2006 [ask copy]
• Hannes Verlinde, "System Development through Refinement -- A First Acquaintance with the B Method". Internal report, Ghent University (2005)

About education in formal methods or Computer Science in general 

• Raymond Boute, "Teaching and Practicing Computer Science at the University Level", ACM SIGCSE Bulletin, Vol. 41, Issue 2, pp. 24-30 (June 2009) [ask copy]
• Raymond Boute, "Formal Methods: Teaching and Practicing Computer Science at the University Level", in: Jim Davies, Jeremy Gibbons, Mike Hinchey and Kenji Taguchi (Eds.), Proc. 1st International Symposium on Formal Methods Education and Training (FMET 2008), Technical Report GRACE-TR-2008-03, pp. 11-25. GRACE Center, National Institute of Informatics, Tokyo (Oct. 2008)
• Raymond Boute, "Microsemantics as a Bootstrap in Teaching Formal Methods", in: Paul Boca, Jonathan Bowen and David Duce eds., Teaching Formal Methods: Practice and Experience, pp. 69-74. The British Computer Society FACS (Dec. 2006)
• Raymond Boute, "Using Domain-Independent Problems for Introducing Formal Methods", in: Jayadev Misra, Tobias Nipkow, Emil Sekerinski (Eds.), FM 2006: Formal Methods, pp. 316--331. Springer LNCS 4085 (Aug. 2006) [ask copy]
• C. Neville Dean and Raymond T. Boute (Eds.), Teaching Formal Methods. Proc. CoLogNET / Formal Methods Europe Symposium, TFM 2004, Ghent, Belgium. Springer LNCS 3294 (Nov. 2004).

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)

Links

Recent events  

Links to directly Funmath-related topics

• The Formal Methods Europe website, plus the upcoming FM 2006 Conference to be held at McMaster University (Canada), August 21-27 2006.
• The IFIP Working Group 2.1 -- Algorithmic Languages and Calculi, doing very interesing work on the calculational derivation of programs.
• The Calculemus group, working towards a new generation of mathematical software systems and computer-aided verification tools. Not all their work is calculational as described, since it is not directed towards human reasoning.
• The upcoming MPC 2006 conference by the Mathematics of Program Construction community, whose logo we have shown.
• David Gries, whose work on calculational logic is mentioned at various places on this (Funmath) site. More recently, together with his son Paul Gries, he designed ProgramLive, an active introductory programming text using Java, based on sound programming methodology. It migt provide a good antidote to the perils of JavaSchools discussed by Joel Spolsky.
• Last but not least, the E. W. Dijkstra Archive, a treasure trove of notes and observations on various aspects on mathematics, computing, and their interrelation.

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.

• Fun and Challenging Math Problems for the Young and Young At Heart (with solutions) for gifted secondary school students, a site made by Karl Dahlke in the context of his Math Reference Project.
• FUNdamentallyMATH, educational software for the K-12 math curriculum.
• Funmaths Game Station, educational software for high school students by Fundamental Software. Various (free) downloads can be found on the web, some advertised as "Funmath Game Station".
• A Korean site at http://www.funmath.net, apparently also educational.

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.