Abstract
We consider abstract interpretation (in particular strictness analysis) for pairs and lists. We begin by reviewing the well-known fact that the best known description of a pair of elements is obtained using the tensor product rather than the cartesian product. We next present a generalisation of Wadler's strictness analysis for lists using the notion of open set. Finally, we illustrate the intimate connection between the case analysis implicit in Wadler's strictness analysis and the precision that the tensor product allows for modelling the inverse cons operation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S.Abramsky: Abstract Interpretation, Logical Relations and Kan Extensions, Journal of Logic and Computation 1 1 (1990), 5–40.
H.-J.Bandelt: The tensorproduct of continuous lattices, Mathematische Zeitschrift 172 (1980) 89–96.
G.L.Burn, C.Hankin, S.Abramsky: Strictness analysis for higher-order functions, Science of Computer Programming 7 (1986) 249–278.
P.Cousot, R.Cousot: Systematic Design of Program Analysis Frameworks, Procedings POPL 1979.
A.B.Ferguson, R.J.M.Hughes: An Iterative Powerdomain Construction, Functional Programming, Glasgow 1989, K.Davis and J.Hughes (eds.), Springer-Verlag (1989) 41–55.
G.Grätzer: Lattice Theory: First concepts and distributive lattices, W.H.Freeman and Company (1971).
J.Hughes: Strictness detection in non-flat domains, Proc. Programs as Data Objects, Springer Lecture Notes in Computer Science 217 (1986) 112–135.
J.Hughes: Backwards Analysis of Functional Programs, Partial Evaluation and Mixed Computation, D.Bjørner, A.P.Ershov and N.D.Jones (eds.), North-Holland (1988) 187–208.
N.D.Jones, S.S.Muchnick: Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra, Program Flow Analysis: Theory and Applications, S.S.Muchnick and N.D.Jones (eds.), Prentice-Hall (1981).
S. Mac Lane: Categories for the Working Mathematician, Springer-Verlag (1971).
F.Nielson: Abstract Interpretation using Domain Theory, Ph.D.-thesis CST-31-84, University of Edinburgh, Scotland (1984).
F.Nielson: Tensor Products Generalize the Relational Data Flow Analysis Method, Proceedings of the 4'th Hungarian Computer Science Conference (1985) 211–225.
F.Nielson: Towards a Denotational Theory of Abstract Intepretation, Abstract Interpretation of Declarative Languages, S.Abramsky and C.Hankin (eds.), Ellis Horwood (1987) 219–245.
F.Nielson: Two-Level Semantics and Abstract Interpretation, Theoretical Computer Science — Fundamental Studies 69 2 (1989) 117–242.
F.Nielson, H.R.Nielson: Two-Level Functional Languages, Cambridge University Press (to appear 1992).
G.D.Plotkin: Lambda definability in the full type hierarchy, To H.B.Curry: Essays on Combinatorial Logic, Lambda Calculus and Formalism, Academic Press (1980).
P.Wadler: Strictness analysis on non-flat domains (by abstract interpretation over finite domains), Abstract Interpretation of Declarative Languages, S.Abramsky and C.Hankin (eds.), Ellis Horwood (1987) 266–275.
P.Wadler, R.J.M.Hughes: Projections for Strictness Analysis, Proceedings Functional Programming Languages and Computer Architecture, Springer Lecture Notes in Computer Science 274 (1987), 385–407.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielson, F., Nielson, H.R. (1992). The tensor product in Wadler's analysis of lists. In: Krieg-Brückner, B. (eds) ESOP '92. ESOP 1992. Lecture Notes in Computer Science, vol 582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55253-7_21
Download citation
DOI: https://doi.org/10.1007/3-540-55253-7_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55253-6
Online ISBN: 978-3-540-46803-5
eBook Packages: Springer Book Archive