# Deciding inclusion of set constants over infinite non-strict data structures

Manfred Schmidt-Schauss; David Sabel; Marko Schütz

RAIRO - Theoretical Informatics and Applications (2007)

- Volume: 41, Issue: 2, page 225-241
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topSchmidt-Schauss, Manfred, Sabel, David, and Schütz, Marko. "Deciding inclusion of set constants over infinite non-strict data structures." RAIRO - Theoretical Informatics and Applications 41.2 (2007): 225-241. <http://eudml.org/doc/250016>.

@article{Schmidt2007,

abstract = {
Various static analyses of functional programming languages
that permit infinite data structures make use of set
constants like Top, Inf, and 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.
},

author = {Schmidt-Schauss, Manfred, Sabel, David, Schütz, Marko},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Functional programming languages; lambda calculus; strictness analysis; set constraints; tree automata; DEXPTIME-completeness; lazy functional programming languages},

language = {eng},

month = {7},

number = {2},

pages = {225-241},

publisher = {EDP Sciences},

title = {Deciding inclusion of set constants over infinite non-strict data structures},

url = {http://eudml.org/doc/250016},

volume = {41},

year = {2007},

}

TY - JOUR

AU - Schmidt-Schauss, Manfred

AU - Sabel, David

AU - Schütz, Marko

TI - Deciding inclusion of set constants over infinite non-strict data structures

JO - RAIRO - Theoretical Informatics and Applications

DA - 2007/7//

PB - EDP Sciences

VL - 41

IS - 2

SP - 225

EP - 241

AB -
Various static analyses of functional programming languages
that permit infinite data structures make use of set
constants like Top, Inf, and 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.

LA - eng

KW - Functional programming languages; lambda calculus; strictness analysis; set constraints; tree automata; DEXPTIME-completeness; lazy functional programming languages

UR - http://eudml.org/doc/250016

ER -

## References

top- S. Abramsky and C. Hankin, Abstract interpretation of declarative languages. Ellis Horwood, (1987).
- 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.
- 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. Zbl0953.68557
- Z.M. Ariola and S. Blom, Cyclic lambda calculi, in TACS, Sendai, Japan (1997) 77–106. Zbl0884.03008
- Z.M. Ariola and J.W. Klop, Lambda calculus with explicit recursion. Inform. Comput.139 (1997) 154–233. Zbl0892.68015
- 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. Zbl0793.68127
- G. Burn, Lazy Functional Languages: Abstract Interpretation and Compilation. Pitman, London, (1991). Zbl0809.68079
- 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. Zbl0596.68009
- 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.
- D. Clark, C. Hankin, and S. Hunt, Safety of strictness analysis via term graph rewriting. In SAS 2000 (2000) 95–114. Zbl0966.68089
- H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison and M. Tommasi. Tree automata techniques and applications. Available on: , 1997. release October, 1rst 2002. URIhttp://www.grappa.univ-lille3.fr/tata
- M. Coppo, F. Damiani and P. Giannini, Strictness, totality, and non-standard type inference. Theoret. Comput. Sci.272 (2002) 69–112. Zbl0984.68028
- 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.
- B.A. Davey and H.A. Priestley, Introduction to Lattices and Order. Cambridge University Press, Cambridge, (1992). Zbl0701.06001
- 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. Zbl0949.68017
- T.P. Jensen, inference of polymorphic and conditional strictness properties, in Symposium on Principles of Programming Languages, San Diego, ACM Press. (1998) 209–221.
- S.P. Jones, Haskell 98 Language and Libraries. Cambridge University Press (2003). www.haskell.org
- 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.
- K. Lackner Solberg Gasser, H. Riis Nielson and F. Nielson, Strictness and totality analysis. Sci. Comput. Programming31 (1998) 113–145. Zbl0941.68021
- J. Launchbury and S. Peyton Jones, State in Haskell. Lisp Symbolic Comput.8 (1995) 293–341.
- 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. Zbl0960.68041
- A.K.D. Moran, D. Sands and M. Carlsson, Erratic fudgets: A semantic theory for an embedded coordination language. Sci. Comput. Programming46 (2003) 99–135. Zbl1026.68091
- A. Mycroft, Abstract Interpretation and Optimising Transformations for Applicative Programs. Ph.D. thesis, University of Edinburgh (1981).
- E. Nöcker, Strictness analysis using abstract reduction. Technical Report 90-14, Department of Computer Science, University of Nijmegen (1990).
- 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).
- E. Nöcker, Strictness analysis using abstract reduction. In Functional Programming Languages and Computer Architecture, ACM Press, (1993) 255–265.
- 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.
- D. Pape, Striktheitsanalysen funktionaler Sprachen. Ph.D. thesis, Fachbereich Mathematik und Informatik, Freie Universität Berlin, (2000). In German.
- R. Paterson, Compiling laziness using projections, in Static Analysis Symposium, Aachen, Germany. Lect. Notes Comput. Sci.1145 (1996) 255–269.
- 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. URIhttp://www.cs.kun.nl/~clean/
- 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. Zbl1095.68056
- 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.
- 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). Zbl1153.68012
- 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).
- M. Schütz, Analysing demand in nonstrict functional programming languages. Dissertation, J.W.Goethe-Universität Frankfurt, 2000. Available at URIhttp://www.ki.informatik.uni-frankfurt.de/papers/marko
- H. Seidl, Deciding equivalence of finite tree automata. SIAM J. Comput.19 (1990) 424–437. Zbl0699.68075
- 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. Zbl0900.68316
- 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).
- P. Wadler and J. Hughes, Projections for strictness analysis. In Functional Programming Languages and Computer Architecture. Lect. Notes Comput. Sci.274 (1987) 385–407. Zbl0625.68014

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.