article

Fast and loose reasoning is morally correct

Authors:

Nils Anders Danielsson,

Patrik Jansson,

Jeremy GibbonsAuthors Info & Claims

ACM SIGPLAN Notices, Volume 41, Issue 1

Pages 206 - 217

https://doi.org/10.1145/1111320.1111056

Published: 11 January 2006 Publication History

Abstract

Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values.It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation.

References

[1]

Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3--27, 2005.

Digital Library

[2]

Peter Aczel. The strength of Martin-Löf's intuitionistic type theory with one universe. In Proceedings of Symposia in Mathematical Logic, Oulu, 1974, and Helsinki, 1975, pages 1--32, University of Helsinki, Department of Philosophy, 1977.

[3]

Marek A. Bednarczyk and Andrzej M. Borzyszkowski. Cpo's do not form a cpo and yet recursion works. In VDM '91, volume 551 of LNCS, pages 268--278. Springer-Verlag, 1991.

Digital Library

[4]

R.C. Backhouse, P.J. de Bruin, P. Hoogendijk, G. Malcolm, T.S. Voermans, and J.C.S.P. van~der Woude. Relational catamorphisms. In Constructing Programs from Specifications, pages 287--318. North-Holland, 1991.

[5]

Richard Bird and Oege de Moor. Algebra of Programming. Prentice Hall, 1996.

Digital Library

[6]

M. Beeson. Recursive models for constructive set theories. Annals of Mathematical Logic, 23:127--178, 1982.

[7]

Andrzej Blikle. MetaSoft Primer, Towards a Metalanguage for Applied Denotational Semantics, volume 288 of LNCS. Springer-Verlag, 1987.

Digital Library

[8]

Andrzej Blikle and Andrzej Tarlecki. Naive denotational semantics. In Information Processing 83, pages 345--355. North-Holland, 1983.

[9]

Nils Anders Danielsson. Personal web page, available at http://www.cs.chalmers.se/~nad/, 2005.

[10]

Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976.

Digital Library

[11]

Nils Anders Danielsson and Patrik Jansson. Chasing bottoms, a case study in program verification in the presence of partial and infinite values. In MPC 2004, volume 3125 of LNCS, pages 85--109. Springer-Verlag, 2004.

[12]

Peter Dybjer. Program verification in a logical theory of constructions. In FPCA'85, volume 201 of LNCS, pages 334--349. Springer-Verlag, 1985. Appears in revised form as Programming Methodology Group Report 26, University of Göteborg and Chalmers University of Technology, 1986.

Digital Library

[13]

Peter Dybjer. Representing inductively defined sets by wellorderings in Martin-Löf's type theory. Theoretical Computer Science, 176:329--335, 1997.

Digital Library

[14]

Maarten M Fokkinga and Erik Meijer. Program calculation properties of continuous algebras. Technical Report CS-R9104, Centre for Mathematics and Computer Science, Amsterdam, The Netherlands, 1991.

[15]

Harvey Friedman. Equality between functionals. In Logic Colloquium: Symposium on Logic held at Boston, 1972-73, number 453 in Lecture Notes in Mathematics, pages 22--37. Springer, 1975.

[16]

Lars Hallnäs. An intensional characterization of the largest bisimulation. Theoretical Computer Science, 53(2--3):335--343, 1987.

Digital Library

[17]

Graham Hutton and Jeremy Gibbons. The generic approximation lemma. Information Processing Letters, 79(4):197--201, 2001.

Digital Library

[18]

Hagen Huwig and Axel Poigné. A note on inconsistencies caused by fixpoints in a cartesian closed category. Theoretical Computer Science, 73(1):101--112, 1990.

Digital Library

[19]

J. Jeuring. Algorithms from theorems. In Programming Concepts and Methods, pages 247--266. North-Holland, 1990.

[20]

Patricia Johann and Janis Voigtländer. Free theorems in the presence of seq. In POPL'04, pages 99--110. ACM Press, 2004.

Digital Library

[21]

E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA'91, volume 523 of LNCS, pages 124--144. Springer-Verlag, 1991.

Digital Library

[22]

Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

Digital Library

[23]

Simon Peyton Jones, editor. Haskell 98 Language and Libraries, The Revised Report. Cambridge University Press, 2003.

[24]

Hilary A. Priestley. Ordered sets and complete lattices, a primer for computer science. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 of LNCS, chapter~2, pages 21--78. Springer-Verlag, 2002.

Digital Library

[25]

John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, pages 513--523. Elsevier, 1983.

[26]

John C. Reynolds. Polymorphism is not set-theoretic. In Semantics of Data Types, volume 173 of LNCS, pages 145--156. Springer-Verlag, 1984.

[27]

Dana Scott. Data types as lattices. SIAM Journal of Computing, 5(3):522--587, 1976.

[28]

Jan Smith. An interpretation of Martin-Löf's type theory in a type-free theory of propositions. Journal of Symbolic Logic, 49(3):730--753, 1984.

[29]

David Turner. Elementary strong functional programming. In FPLE'95, volume 1022 of LNCS, pages 1--13. Springer-Verlag, 1996.

Digital Library

[30]

Philip Wadler. Theorems for free! In FPCA'89, pages 347--359. ACM Press, 1989.

Digital Library

Cited By

Gissurarson MRoque DKoppel J(2023)Spectacular: Finding Laws from 25 Trillion Terms2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00035(293-304)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00035
Kappelmann KRädle JStevens L(2022)Engaging, Large-Scale Functional Programming Education in Physical and Virtual SpaceElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.363.6363(93-113)Online publication date: 26-Jul-2022
https://doi.org/10.4204/EPTCS.363.6
Fernandes JCunha JSaraiva JPardo A(2019)Watch Out for that Tree! A Tutorial on Shortcut DeforestationCentral European Functional Programming School10.1007/978-3-030-28346-9_1(1-41)Online publication date: 14-Aug-2019
https://doi.org/10.1007/978-3-030-28346-9_1
Show More Cited By

Index Terms

Fast and loose reasoning is morally correct
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Fast and loose reasoning is morally correct
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with ...
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)
Haskell '18

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how ...
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)
Haskell 2018: Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 41, Issue 1

Proceedings of the 2006 POPL Conference

January 2006

421 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1111320

Issue’s Table of Contents

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2006
432 pages
ISBN:1595930272
DOI:10.1145/1111037
General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2006

Published in SIGPLAN Volume 41, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

51
Total Citations
View Citations
730
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)2

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gissurarson MRoque DKoppel J(2023)Spectacular: Finding Laws from 25 Trillion Terms2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00035(293-304)Online publication date: Apr-2023
https://doi.org/10.1109/ICST57152.2023.00035
Kappelmann KRädle JStevens L(2022)Engaging, Large-Scale Functional Programming Education in Physical and Virtual SpaceElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.363.6363(93-113)Online publication date: 26-Jul-2022
https://doi.org/10.4204/EPTCS.363.6
Fernandes JCunha JSaraiva JPardo A(2019)Watch Out for that Tree! A Tutorial on Shortcut DeforestationCentral European Functional Programming School10.1007/978-3-030-28346-9_1(1-41)Online publication date: 14-Aug-2019
https://doi.org/10.1007/978-3-030-28346-9_1
Román M(2018)Mikrokosmos: an educational lambda calculus interpreterJournal of Open Source Education10.21105/jose.000291:8(29)Online publication date: Oct-2018
https://doi.org/10.21105/jose.00029
Pieters RSchrijvers TRivas E(2017)Handlers for Non-Monadic ComputationsProceedings of the 29th Symposium on the Implementation and Application of Functional Programming Languages10.1145/3205368.3205372(1-11)Online publication date: 30-Aug-2017
https://dl.acm.org/doi/10.1145/3205368.3205372
Christiansen JDanilenko NDylus S(2016)All sorts of permutations (functional pearl)ACM SIGPLAN Notices10.1145/3022670.295194951:9(168-179)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951949
Christiansen JDanilenko NDylus SGarrigue JKeller GSumii E(2016)All sorts of permutations (functional pearl)Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951949(168-179)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951949
Honsell FLenisa MLiquori LScagnetto I(2016)Implementing Cantor’s ParadiseProgramming Languages and Systems10.1007/978-3-319-47958-3_13(229-250)Online publication date: 9-Oct-2016
https://doi.org/10.1007/978-3-319-47958-3_13
JASKELIOFF MO'CONNOR R(2015)A representation theorem for second-order functionalsJournal of Functional Programming10.1017/S095679681500008825Online publication date: 8-Sep-2015
https://doi.org/10.1017/S0956796815000088
Mol MEekelen MPlasmeijer R(2008)Proving Properties of Lazy Functional Programs with SparkleCentral European Functional Programming School10.1007/978-3-540-88059-2_2(41-86)Online publication date: 1-Jun-2008
https://dl.acm.org/doi/10.1007/978-3-540-88059-2_2
Show More Cited By

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents