Nils Anders Danielsson
Patrik Jansson
Jeremy Gibbons
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.
- Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3--27, 2005. Google Scholar
Digital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Richard Bird and Oege de Moor. Algebra of Programming. Prentice Hall, 1996. Google ScholarDigital Library
- M. Beeson. Recursive models for constructive set theories. Annals of Mathematical Logic, 23:127--178, 1982.Google ScholarCross Ref
- Andrzej Blikle. MetaSoft Primer, Towards a Metalanguage for Applied Denotational Semantics, volume 288 of LNCS. Springer-Verlag, 1987. Google ScholarDigital Library
- Andrzej Blikle and Andrzej Tarlecki. Naive denotational semantics. In Information Processing 83, pages 345--355. North-Holland, 1983.Google Scholar
- Nils Anders Danielsson. Personal web page, available at http://www.cs.chalmers.se/~nad/, 2005.Google Scholar
- Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Peter Dybjer. Representing inductively defined sets by wellorderings in Martin-Löf's type theory. Theoretical Computer Science, 176:329--335, 1997. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- Lars Hallnäs. An intensional characterization of the largest bisimulation. Theoretical Computer Science, 53(2--3):335--343, 1987. Google ScholarDigital Library
- Graham Hutton and Jeremy Gibbons. The generic approximation lemma. Information Processing Letters, 79(4):197--201, 2001. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. Jeuring. Algorithms from theorems. In Programming Concepts and Methods, pages 247--266. North-Holland, 1990.Google Scholar
- Patricia Johann and Janis Voigtländer. Free theorems in the presence of seq. In POPL'04, pages 99--110. ACM Press, 2004. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997. Google ScholarDigital Library
- Simon Peyton Jones, editor. Haskell 98 Language and Libraries, The Revised Report. Cambridge University Press, 2003.Google Scholar
- 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. Google ScholarDigital Library
- John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, pages 513--523. Elsevier, 1983.Google Scholar
- John C. Reynolds. Polymorphism is not set-theoretic. In Semantics of Data Types, volume 173 of LNCS, pages 145--156. Springer-Verlag, 1984.Google ScholarCross Ref
- Dana Scott. Data types as lattices. SIAM Journal of Computing, 5(3):522--587, 1976.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- David Turner. Elementary strong functional programming. In FPLE'95, volume 1022 of LNCS, pages 1--13. Springer-Verlag, 1996. Google ScholarDigital Library
- Philip Wadler. Theorems for free! In FPCA'89, pages 347--359. ACM Press, 1989. Google ScholarDigital Library
Index Terms
- Fast and loose reasoning is morally correct
Recommendations
Fast and loose reasoning is morally correct
Proceedings of the 2006 POPL ConferenceFunctional 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 '18Equational 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 HaskellEquational 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