article

Open access

Functional declarative language design and predicate calculus: a practical approach

Author:

Raymond BouteAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 27, Issue 5

Pages 988 - 1047

https://doi.org/10.1145/1086642.1086647

Published: 01 September 2005 Publication History

Abstract

In programming language and software engineering, the main mathematical tool is de facto some form of predicate logic. Yet, as elsewhere in applied mathematics, it is used mostly far below its potential, due to its traditional formulation as just a topic in logic instead of a calculus for everyday practical use.The proposed alternative combines a language of utmost simplicity (four constructs only) that is devoid of the defects of common mathematical conventions, with a set of convenient calculation rules that is sufficiently comprehensive to make it practical for everyday use in most (if not all) domains of interest.Its main elements are a functional predicate calculus and concrete generic functionals. The first supports formal calculation with quantifiers with the same fluency as with derivatives and integrals in classical applied mathematics and engineering. The second achieves the same for calculating with functionals, including smooth transition between pointwise and point-free expression.The extensive collection of examples pertains mainly to software specification, language semantics and its mathematical basis, program calculation etc., but occasionally shows wider applicability throughout applied mathematics and engineering. Often it illustrates how formal reasoning guided by the shape of the expressions is an instrument for discovery and expanding intuition, or highlights design opportunities in declarative and (functional) programming languages.

References

[1]

Aarts, C., Backhouse, R., Hoogendijk, P., Voermans, E., and van der Woude, J. 1992. A Relational Theory of Data Types. Lecture notes, T. U. Eindhoven.]]

[2]

Almstrum, V. L. 1996. Investigating student difficulties with mathematical logic. In Teaching and Learning Formal Methods, C. Neville Dean and Michael G. Hinchey, Eds. Academic Press, Orlando, FL, pp. 131--160.]]

[3]

Alur, R., Henzinger, T. A., and Sontag, E. D., Eds. 1996. Hybrid Systems III. Lecture Notes in Computer Science, vol. 1066. Springer-Verlag, Berlin, Heidelberg.]]

[4]

Backus, J. 1978. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Commun. ACM 21, 8, (Aug.) 613--641.]]

[5]

Barendregt, H. P. 1984. The Lambda Calculus, Its Syntax and Semantics. North-Holland, Amsterdam, The Netherlands.]]

[6]

Bird, R. 1998. Introduction to Functional Programming using Haskell. Prentice-Hall International Series in Computer Science, London, England.]]

[7]

Bishop, R. H. 2001. LabVIEW Student Edition, Prentice-Hall, Englewood Cliffs, N.J.]]

[8]

Boiten, E. and Möller, B. 2002. In Proceedings of the 6th International Conference on Mathematics of Program Construction (Conference announcement). Dagstuhl. http://www.cs.kent.ac.uk/events/conf/2002/mpc2002.]]

[9]

Boute, R. T. 1982. On the requirements for dynamic software modification. In MICROSYSTEMS: Architecture, Integration and Use, van Spronsen, C. J. and L. Richter, Eds., North-Holland, Amsterdam, The Netherlands, pp. 259--271.]]

[10]

Boute, R. T. 1990. A heretical view on type embedding. ACM SIGPLAN Notices 25, 11 (Jan.), 22--28.]]

[11]

Boute, R. T. 1991. Declarative languages---Still a long way to go. In Computer Hardware Description Languages and their Applications. Dominique Borrione and Ronald Waxman, Eds. North-Holland, Amsterdam, The Netherlands, pp. 185--212.]]

[12]

Boute, R. T. 1992. The Euclidean definition of the functions div and mod. ACM Trans. Prog. Lang. Syst. 14, 2 (Apr.), 127--144.]]

[13]

Boute, R. T. 1993a. Funmath Illustrated: A Declarative Formalism and Application Examples. Declarative Systems Series No. 1, Computing Science Institute, University of Nijmegen.]]

[14]

Boute, R. T. 1993b. Fundamentals of hardware description languages and declarative languages. In Fundamentals and Standards in Hardware Description Languages. Jean P. Mermet, Ed. Kluwer Academic Publishers, pp. 3--38.]]

[15]

Boute, R. T. 2000. Supertotal function definition in mathematics and software engineering. IEEE Trans. Softw. Eng. 26, 7 (July), pp. 662--672.]]

[16]

Boute, R. T. 2002. Functional Mathematics: A Unifying Declarative and Calculational Approach to Systems, Circuits and Programs---Part I: Basic Mathematics. Course text, Ghent University.]]

[17]

Boute, R. T. 2003. Concrete generic functionals: Principles, design and applications. In Generic Programming, Jeremy Gibbons, Johan Jeuring, Eds., Kluwer, pp. 89--119.]]

[18]

Boute, R. 2004. Functional declarative language design and predicate calculus: A practical approach. Tech. Rep. TR-B2004-03. INTEC, Ghent Univ.]]

[19]

Bryant, R. E. 1992. Symbolic Boolean manipulation with ordered binary-decision diagrams. Comput. Surv. 24, 3, (Sept.), 293--318.]]

[20]

Buck, J., Ha, S., Lee, E. A., and Messerschmitt, D. G. 1994. Ptolemy: A framework for simulating and prototyping heterogeneous systems. Int. J. Comput. Simul. (spec. issue on Simulation Software Development), (Jan.)]]

[21]

Carson, R. S. 1990. Radio Communications Concepts: Analog. Wiley, New York.]]

[22]

Cohen, E. 1990. Programming in the 1990s. Springer-Verlag, Berlin, Germany.]]

[23]

Cori, R. and Lascar, D. 2000. Mathematical Logic: A Course with Exercises, Part I. Oxford University Press, Oxford, England.]]

[24]

Davenport, J. H. 2000. A small OpenMath type system. SIGSAM Bull. 34, 2, (Jun.), 16--26.]]

[25]

Dean, C. N. and Hinchey, M. G. 1996. Teaching and Learning Formal Methods. Academic Press, London, England, 197--243.]]

[26]

Dijkstra, E. W. 1992. On the economy of doing mathematics. EWD1130, http://www.cs.utexas.edu/users/EWD/.]]

[27]

Dijkstra, E. W. 1996a. Beware of the empty range. EWD1247 (Sep.), http://www.cs.utexas.edu/users/EWD/.]]

[28]

Dijkstra, E. W. 1996b. Andrew's challenge once more. EWD1249 (Oct.), http://www.cs.utexas.edu/users/EWD/.]]

[29]

Dijkstra, E. W. 2000. Under the spell of Leibniz's dream. EWD1298 (Apr.), http://www.cs.utexas.edu/users/EWD/.]]

[30]

Dijkstra, E. W. and Scholten, C. S. 1990. Predicate Calculus and Program Semantics. Springer-Verlag, Berlin, Germany.]]

[31]

Forster, T. E. 1992. Set Theory with a Universal Set. Clarendon Press, Oxford, England.]]

[32]

Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M., and Scott, D. S. 1980. A Compendium of Discrete Lattices. Springer-Verlag, Berlin, Germany.]]

[33]

Graham, R. L., Knuth, D. E., and Patashnik, O. 1994. Concrete Mathematics: A Foundation for Computer Science. Addison-Wesley, Reading, MA.]]

[34]

Gries, D. 1996a. The need for education in useful formal logic. IEEE Comput. 29, 4, (Apr.), 29--30.]]

[35]

Gries, D. 1996b. A calculational proof of Andrew's challenge. Technical Note, http://webster.cs.uga.edu/~gries/Papers/andrews.pdf.]]

[36]

Gries, D. and Schneider, F. B. 1993. A Logical Approach to Discrete Math. Springer-Verlag, New York.]]

[37]

Halmos, P. and Givant, S. 1998. Logic as Algebra. Math. Assoc. Amer.]]

[38]

Harrison, J. 2000. The HOL Light Manual. University of Cambridge Computer Laboratory, http://www.cl.cam.ac.uk/users/jrh/hol-light/manual-1.1.pdf.]]

[39]

Hehner, E. C. R. 1996. Boolean formalism and explanations. Invited talk, AMAST, (Munich, Germany, (July), Text at http://www.cs.toronto.edu/~hehner/BFE.pdf.]]

[40]

Holzmann, G. 2003. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading, Mass.]]

[41]

Hudak, P., Peterson, J., and Fasel, J. H. 1999. A Gentle Introduction to Haskell 98 (Oct.). http://www.haskell.org/tutorial/]]

[42]

Hudak, P., Courtney, A., Nilsson, H., and Peterson, J. 2003. Arrows, robots and functional reactive programming. In Advanced Functional Programming, Johan Jeuring and Simon Peyton Jones, Eds., Lecture Notes in Computer Science, vol. 2638. Springer-Verlag, New York, haskell.CS.Yale.edu/Yampa/AFPLectureNotes.pdf.]]

[43]

IEEE 1994. IEEE Standard VHDL Language, Reference Manual. IEEE, New York.]]

[44]

Illingworth, V., Glaser, E. L., and Pyle, I. C. 1989. Dictionary of Computing, Oxford University Press, Oxford, England.]]

[45]

Jackson, P. B. 1992. NUPRL and its use in circuit design. In Theorem Provers in Circuit Design. Victoria Stavridou, Tom Melham, and Raymond T. Boute, Eds., North Holland, Amsterdam, The Netherlands, pp. 311--336.]]

[46]

Jensen, K. and Wirth, N. 1978. PASCAL User Manual and Report. Springer-Verlag, New York.]]

[47]

Johnson-Laird, P. N. 2000. (example problems in the psychological study of human reasoning), http://www.princeton.edu/~psych/PsychSite/fac_phil.html.]]

[48]

Lang, S. 1983. Undergraduate Analysis. Springer-Verlag, Berlin, Germany.]]

[49]

Lamport, L. and Paulson, L. C. 1997. Should your specification language be typed? SRC Research Report 147, Digital Equipment Corporation (May).]]

[50]

Lamport, L. 1993. How to write a proof. DEC SRC Research Report. http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-94.html.]]

[51]

Loeckx, J. and Sieber, K. 1984. The Foundations of Program Verification. Wiley-Teubner, New York.]]

[52]

Manolios, P. and Moore, J. S. 2001. On the desirability of mechanizing calculational proofs. Inf. Proc. Lett., 77, 2--4, 173--179.]]

[53]

Mendelson, E. 1987. Introduction to Mathematical Logic, 3rd. ed. Wadsworth & Brooks/Cole.]]

[54]

Meyer, B. 1991. Introduction to the Theory of Programming Languages. Prentice Hall, New York.]]

[55]

Ostroff, J. S. Rationale for restructuring the logic and discrete math (MATH1090/2090) courses for CS students. York University, http://www.cs.yorku.ca/~logicE/curriculum/logic_discrete_maths.html.]]

[56]

Page, R. 2000. BESEME: Better Software Engineering through Mathematics Education, project presentation http://www.cs.ou.edu/~beseme/besemePres.pdf]]

[57]

Parnas, D. L. 1993. Predicate logic for software engineering. IEEE Trans. SWE 19, 9, (Sept.), 856--862.]]

[58]

Paulson, L. C. 2001. Introduction to Isabelle, Cambridge Computer Laboratory. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/docs.html.]]

[59]

Pugh, W. 1994. Counting solutions to Presburger formulas: How and why. ACM SIGPLAN Notices 29, 6, (June), 121--122.]]

[60]

Rechenberg, P. 1990. Programming languages as thought models. Struct. Prog. 11, 105--115.]]

[61]

Reynolds, J. C. 1980. Using category theory to design implicit conversions and generic operators. In Semantics-Directed Compiler Generation. Neil D. Jones, Ed., Lecture Notes in Computer Science, vol. 94, Springer-Verlag, Berlin, Germany, pp. 261--288.]]

[62]

Roberts, R. A. and Mullis, C. T. 1987. Digital Signal Processing. Addison-Wesley, Reading, MA.]]

[63]

Rushby, J., Owre, S., and Shankar, N. 1998. Subtypes for Specifications: Predicate subtyping in PVS. Trans. Softw. Eng. 24, 9, (Sept.), 709--720.]]

[64]

Schieder, B. and Broy, M. 1999. Adapting calculational logic to the undefined. Comput. J. 42, 2, 73--81.]]

[65]

Spivey, J. M. 1989. The Z notation: A Reference Manual. Prentice-Hall, Englewood, Cliffs, N. J.]]

[66]

Stoy, J. E. 1977. Denotational Semantics: The Scott--Strachey Approach to Programming Language Theory. The MIT Press, Cambridge, Mass.]]

[67]

Tarski, A. and Givant, S. 1987. A Formalization of Set Theory without Variables. American Mathematical Society.]]

[68]

Taylor, P. 2000. Practical Foundations of Mathematics (second printing), No. 59 in Cambridge Studies in Advanced Mathematics, Cambridge University Press, http://www.dcs.qmul.ac.uk/~pt/Practical_Foundations/html/s10.html]]

[69]

Tennent, R. D. 1991. Semantics of Programming Languages. Prentice-Hall, Englewood Cliffs, NJ.]]

[70]

Vaandrager, F. W. and van Schuppen, J. H. Eds. 1999. Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1569. Springer-Verlag, Berlin Heidelberg, Germany.]]

[71]

van den Beuken, F. 1997. A functional approach to syntax and typing. Ph.D. dissertation. School of Mathematics and Informatics, University of Nijmegen.]]

[72]

van Thienen, H. 1994. It's about time---using funmath for the specification and analysis of discrete dynamic systems. Ph.D. dissertation. Department of Informatics, University of Nijmegen.]]

[73]

Wechler, W. 1987. Universal Algebra for Computer Scientists. Springer-Verlag, New York.]]

[74]

Winskel, G. 1993. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, Cambridge, MA.]]

[75]

Wolfram, S. 1996. The Mathematica book, 3rd. ed. Cambridge University Press, Cambridge, MA.]]

[76]

Zamfirescu, A. 1993. Logic and arithmetic in hardware description languages. In Fundamentals and Standards in Hardware Description Languages, J. P. Mermet, Ed. NATO ASI Series E, Vol. 249. Kluwer, Dordrecht, pp. 79--107.]]

Cited By

Hinsen K(2018)Verifiability in computer-aided research: the role of digital scientific notations at the human-computer interfacePeerJ Computer Science10.7717/peerj-cs.1584(e158)Online publication date: 23-Jul-2018
https://doi.org/10.7717/peerj-cs.158
Boute R(2012)The Geometry of Bandpass Sampling: A Simple and Safe Approach [Lecture Notes]IEEE Signal Processing Magazine10.1109/MSP.2012.219296929:4(90-96)Online publication date: Jul-2012
https://doi.org/10.1109/MSP.2012.2192969
Boute R(2010)Pointfree expression and calculationFormal Methods in System Design10.1007/s10703-010-0100-237:2-3(95-140)Online publication date: 1-Dec-2010
https://dl.acm.org/doi/10.1007/s10703-010-0100-2
Show More Cited By

Index Terms

Functional declarative language design and predicate calculus: a practical approach

Recommendations

Calculational semantics: Deriving programming theories from equations by functional predicate calculus

The objects of programming semantics, namely, programs and languages, are inherently formal, but the derivation of semantic theories is all too often informal, deprived of the benefits of formal calculation “guided by the shape of the formulas.” ...
DT-an automated theorem prover for multiple-valued first-order predicate logics
ISMVL '96: Proceedings of the 26th International Symposium on Multiple-Valued Logic

We describe the automated theorem prover "Deep Thought" (DT). The prover can be used for arbitrary multiple-valued first-order logics, provided the connectives can be defined by truth tables and the quantifiers are generalizations of the classical ...
Logic Operators and Quantifiers in Type-Theory of Algorithms
Logic and Engineering of Natural Language Semantics
Abstract
In this work, I introduce the Type-Theory of Algorithms (TTA), which is an extension of Moschovakis Type-Theory of Algorithms and its reduction calculus, by adding logic operators and quantifiers. The formal language has two kinds of terms of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 27, Issue 5

September 2005

229 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1086642

Issue’s Table of Contents

Copyright © 2005 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2005

Published in TOPLAS Volume 27, Issue 5

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
1,476
Total Downloads

Downloads (Last 12 months)97
Downloads (Last 6 weeks)13

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hinsen K(2018)Verifiability in computer-aided research: the role of digital scientific notations at the human-computer interfacePeerJ Computer Science10.7717/peerj-cs.1584(e158)Online publication date: 23-Jul-2018
https://doi.org/10.7717/peerj-cs.158
Boute R(2012)The Geometry of Bandpass Sampling: A Simple and Safe Approach [Lecture Notes]IEEE Signal Processing Magazine10.1109/MSP.2012.219296929:4(90-96)Online publication date: Jul-2012
https://doi.org/10.1109/MSP.2012.2192969
Boute R(2010)Pointfree expression and calculationFormal Methods in System Design10.1007/s10703-010-0100-237:2-3(95-140)Online publication date: 1-Dec-2010
https://dl.acm.org/doi/10.1007/s10703-010-0100-2
Boute R(2009)Teaching and practicing computer science at the university levelACM SIGCSE Bulletin10.1145/1595453.159545841:2(24-30)Online publication date: 25-Jun-2009
https://dl.acm.org/doi/10.1145/1595453.1595458
Morris JBunkenburg ATyrrell M(2009)Term transformersACM Transactions on Programming Languages and Systems10.1145/1516507.151651131:4(1-42)Online publication date: 26-May-2009
https://dl.acm.org/doi/10.1145/1516507.1516511
Boute R(2009)The Decibel Done Right: A Matter of Engineering the MathIEEE Antennas and Propagation Magazine10.1109/MAP.2009.543313751:6(177-184)Online publication date: Dec-2009
https://doi.org/10.1109/MAP.2009.5433137
Boute R(2009)Making Temporal Logic CalculationalProceedings of the 2nd World Congress on Formal Methods10.1007/978-3-642-05089-3_25(387-402)Online publication date: 4-Nov-2009
https://dl.acm.org/doi/10.1007/978-3-642-05089-3_25
Morris JTyrrell M(2008)Dually nondeterministic functionsACM Transactions on Programming Languages and Systems10.1145/1391956.139196130:6(1-34)Online publication date: 30-Oct-2008
https://dl.acm.org/doi/10.1145/1391956.1391961
Khwaja AUrban J(2008)RealSpecProceedings of the 2008 The 19th IEEE/IFIP International Symposium on Rapid System Prototyping10.1109/RSP.2008.9(3-9)Online publication date: 2-Jun-2008
https://dl.acm.org/doi/10.1109/RSP.2008.9
Boute R(2008)Simple Gedanken Experiments in Leveraging Applications of Formal MethodsLeveraging Applications of Formal Methods, Verification and Validation10.1007/978-3-540-88479-8_60(847-861)Online publication date: 2008
https://doi.org/10.1007/978-3-540-88479-8_60
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents