zbMATH — the first resource for mathematics

Examples
Geometry Search for the term Geometry in any field. Queries are case-independent.
Funct* Wildcard queries are specified by * (e.g. functions, functorial, etc.). Otherwise the search is exact.
"Topological group" Phrases (multi-words) should be set in "straight quotation marks".
au: Bourbaki & ti: Algebra Search for author and title. The and-operator & is default and can be omitted.
Chebyshev | Tschebyscheff The or-operator | allows to search for Chebyshev or Tschebyscheff.
"Quasi* map*" py: 1989 The resulting documents have publication year 1989.
so: Eur* J* Mat* Soc* cc: 14 Search for publications in a particular source with a Mathematics Subject Classification code (cc) in 14.
"Partial diff* eq*" ! elliptic The not-operator ! eliminates all results containing the word elliptic.
dt: b & au: Hilbert The document type is set to books; alternatively: j for journal articles, a for book articles.
py: 2000-2015 cc: (94A | 11T) Number ranges are accepted. Terms can be grouped within (parentheses).
la: chinese Find documents in a given language. ISO 639-1 language codes can also be used.

Operators
a & b logic and
a | b logic or
!ab logic not
abc* right wildcard
"ab c" phrase
(ab c) parentheses
Fields
any anywhere an internal document identifier
au author, editor ai internal author identifier
ti title la language
so source ab review, abstract
py publication year rv reviewer
cc MSC code ut uncontrolled term
dt document type (j: journal article; b: book; a: book article)
Deciding inclusion of set constants over infinite non-strict data structures. (English) Zbl 1146.68353
Summary: Various static analyses of functional programming languages that permit infinite data structures make use of set constants like {\tt Top}, {\tt Inf}, and {\tt Bot}, denoting all terms, all lists not eventually ending in Nil, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics in the set of all, also infinite, computable trees, where all term constructors are non-strict. This paper proves decidability, in particular DEXPTIME-completeness, of inclusion of co-inductively defined sets by using algorithms and results from tree automata and set constraints. The test for set inclusion is required by certain strictness analysis algorithms in lazy functional programming languages and could also be the basis for further set-based analyses.
MSC:
68N18Functional programming and lambda calculus
03B40Combinatory logic; lambda-calculus
68Q25Analysis of algorithms and problem complexity
68Q45Formal languages and automata
WorldCat.org
Full Text: DOI Numdam EuDML
References:
[1] S. Abramsky and C. Hankin , Abstract interpretation of declarative languages . Ellis Horwood, ( 1987 ).
[2] A. Aiken , Set constraints: Results, applications, and future directions , in Second Workshop on the Principles and Practice of Constraint Programming, Orcas Island, Washington, Springer-Verlag. Lect. Notes Comput. Sci. 874 ( 1994 ) 171 - 179 .
[3] A. Aiken , D. Kozen , M.Y. Vardi and E.L. Wimmers , The complexity of set constraints , in Proc. CSL 1993, Swansea, Wales ( 1993 ) 1 - 17 . Zbl 0953.68557 · Zbl 0953.68557
[4] Z.M. Ariola and S. Blom , Cyclic lambda calculi , in TACS, Sendai, Japan ( 1997 ) 77 - 106 . Zbl 0884.03008 · Zbl 0884.03008
[5] Z.M. Ariola and J.W. Klop , Lambda calculus with explicit recursion . Inform. Comput. 139 ( 1997 ) 154 - 233 . Zbl 0892.68015 · Zbl 0892.68015 · doi:10.1006/inco.1997.2651
[6] L. Bachmair , H. Ganzinger and U. Waldmann , Set constraints are the monadic class , in Proc. 8th Proc Symp. Logic in Computer Science, Swansea, Wales ( 1993 ) 75 - 83 . · Zbl 0793.68127
[7] G. Burn , Lazy Functional Languages: Abstract Interpretation and Compilation . Pitman, London, ( 1991 ). MR 1156765 | Zbl 0809.68079 · Zbl 0809.68079
[8] G.L. Burn , C.L. Hankin and S. Abramsky , The theory for strictness analysis for higher order functions , in Programs as Data Structures, edited by H. Ganzinger and N.D. Jones. Lect. Notes Comput. Sci. 217 ( 1985 ) 42 - 62 . Zbl 0596.68009 · Zbl 0596.68009
[9] W. Charatonik and A. Podelski , Co-definite set constraints , in Proceedings of the 9th International Conference on Rewriting Techniques and Applications, edited by T. Nipkow, Springer-Verlag. Lect. Notes Comput. Sci. 1379 ( 1998 ) 211 - 225 .
[10] D. Clark , C. Hankin , and S. Hunt , Safety of strictness analysis via term graph rewriting . In SAS 2000 ( 2000 ) 95 - 114 . Zbl 0966.68089 · Zbl 0966.68089
[11] H. Comon , M. Dauchet , R. Gilleron , F. Jacquemard , D. Lugiez , S. Tison and M. Tommasi . Tree automata techniques and applications . Available on: http://www.grappa.univ-lille3.fr/tata, 1997. release October, 1rst 2002.
[12] M. Coppo , F. Damiani and P. Giannini , Strictness, totality, and non-standard type inference . Theoret. Comput. Sci. 272 ( 2002 ) 69 - 112 . Zbl 0984.68028 · Zbl 0984.68028 · doi:10.1016/S0304-3975(00)00348-0
[13] P. Cousot and R. Cousot , Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints , in Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, ACM Press ( 1977 ) 252 - 252 .
[14] B.A. Davey and H.A. Priestley , Introduction to Lattices and Order . Cambridge University Press, Cambridge, ( 1992 ). MR 1902334 | Zbl 1002.06001 · Zbl 1002.06001
[15] P. Devienne , J.-M. Talbot and S. Tison , Co-definite set constraints with membership expressions , in JICSLP’98: Proceedings of the 1998 joint international conference and symposium on Logic programming, Cambridge, MA, USA, MIT Press ( 1998 ) 25 - 39 . Zbl 0949.68017 · Zbl 0949.68017
[16] T.P. Jensen , inference of polymorphic and conditional strictness properties, in Symposium on Principles of Programming Languages, San Diego, ACM Press. (1998) 209-221.
[17] S.P. Jones , Haskell 98 Language and Libraries . Cambridge University Press ( 2003 ). www.haskell.org MR 1989220 · Zbl 1067.68041
[18] Tsun-Ming Kuo and P. Mishra, Strictness analysis: A new perspective based on type inference, in Functional Programming Languages and Computer Architecture, ACM Press, (1989) 260-272.
[19] K. Lackner Solberg Gasser , H. Riis Nielson and F. Nielson , Strictness and totality analysis . Sci. Comput. Programming 31 ( 1998 ) 113 - 145 . Zbl 0941.68021 · Zbl 0941.68021 · doi:10.1016/S0167-6423(96)00043-3
[20] J. Launchbury and S. Peyton Jones , State in Haskell . Lisp Symbolic Comput. 8 ( 1995 ) 293 - 341 .
[21] L. Mauborgne , Improving the representation of infinite trees to deal with sets of trees , in ESOP ’00: Proceedings of the 9th European Symposium on Programming Languages and Systems. Lect. Notes Comput. Sci. 1782 ( 2000 ) 275 - 289 . Zbl 0960.68041 · Zbl 0960.68041
[22] A.K.D. Moran , D. Sands and M. Carlsson , Erratic fudgets: A semantic theory for an embedded coordination language . Sci. Comput. Programming 46 ( 2003 ) 99 - 135 . Zbl 1026.68091 · Zbl 1026.68091 · doi:10.1016/S0167-6423(02)00088-6
[23] A. Mycroft , Abstract Interpretation and Optimising Transformations for Applicative Programs . Ph.D. thesis, University of Edinburgh ( 1981 ).
[24] E. Nöcker , Strictness analysis using abstract reduction . Technical Report 90 - 14 , Department of Computer Science, University of Nijmegen ( 1990 ).
[25] E. Nöcker , Strictness analysis by abstract reduction in orthogonal term rewriting systems . Technical Report 92 - 31 , University of Nijmegen, Department of Computer Science ( 1992 ).
[26] E. Nöcker , Strictness analysis using abstract reduction . In Functional Programming Languages and Computer Architecture, ACM Press, ( 1993 ) 255 - 265 .
[27] D. Pape , Higher order demand propagation . In Implementation of Functional Languages (IFL ’98) London, edited by K. Hammond, A.J.T. Davie and C. Clack, Springer-Verlag. Lect. Notes Comput. Sci. 1595 ( 1998 ) 155 - 170 .
[28] D. Pape , Striktheitsanalysen funktionaler Sprachen . Ph.D. thesis, Fachbereich Mathematik und Informatik, Freie Universität Berlin, ( 2000 ). In German. Zbl 0951.68526 · Zbl 0951.68526
[29] R. Paterson , Compiling laziness using projections , in Static Analysis Symposium, Aachen, Germany. Lect. Notes Comput. Sci. 1145 ( 1996 ) 255 - 269 .
[30] R. Plasmeijer and M. van Eekelen , The concurrent Clean language report: Version 1.3 and 2.0 . Technical report, Dept. of Computer Science, University of Nijmegen, 2003. http://www.cs.kun.nl/ clean/ Zbl 0633.68003 · Zbl 0633.68003
[31] P. Rychlikowski and T. Truderung , in Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, Set constraints on regular terms, edited by J. Marcinkowski and A. Tarlecki, Springer. Lect. Notes Comput. Sci. 3210 (2004) 458-472. Zbl 1095.68056 · Zbl 1095.68056 · doi:10.1007/b100120
[32] M. Schmidt-Schauß , S. Eric Panitz and M. Schütz , Strictness analysis by abstract reduction using a tableau calculus , in Proc. of the Static Analysis Symposium. Lect. Notes Comput. Sci. 983 ( 1995 ) 348 - 365 .
[33] M. Schmidt-Schauß , M. Schütz and D. Sabel , On the safety of Nöcker’s strictness analysis . Technical Report Frank-19, Institut für Informatik. J.W. Goethe-University ( 2004 ). · Zbl 1153.68012
[34] M. Schmidt-Schauß , M. Schütz and D. Sabel , A complete proof of the safety of Nöcker’s strictness analysis . Technical Report Frank-20, Institut für Informatik. J.W. Goethe-University, ( 2005 ). · Zbl 1153.68012
[35] M. Schütz , Analysing demand in nonstrict functional programming languages . Dissertation, J.W.Goethe-Universität Frankfurt, 2000. Available at http://www.ki.informatik.uni-frankfurt.de/papers/marko [36] H. Seidl , Deciding equivalence of finite tree automata . SIAM J. Comput. 19 ( 1990 ) 424 - 437 . Zbl 0699.68075 · Zbl 0699.68075 · doi:10.1137/0219027
[36] W. Thomas , Automata on infinite objects . In Handbook of Theoretical Computer Science, Formal Models and Semantics (B), edited by J. van Leeuwen, Elsevier ( 1990 ) 133 - 192 . Zbl 0900.68316 · Zbl 0900.68316
[37] P. Wadler , Strictness analysis on non-flat domains (by abstract interpretation over finite domains). In Abstract Interpretation of Declarative Languages, Chap. 12. Edited by S. Abramsky and C. Hankin, Ellis Horwood Limited, Chichester ( 1987 ).
[38] P. Wadler and J. Hughes , Projections for strictness analysis . In Functional Programming Languages and Computer Architecture. Lect. Notes Comput. Sci. 274 ( 1987 ) 385 - 407 . Zbl 0625.68014 · Zbl 0625.68014