Deciding inclusion of set constants over infinite non-strict data structures
Schmidt-Schauss, Manfred ; Sabel, David ; Schütz, Marko1
1 Dept. of Mathematics and Computing Science, University of the South Pacific, Suva, Fiji Islands
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 41 (2007) no. 2, pp. 225-241.

Voir la notice de l'article dans Numdam

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.

DOI : 10.1051/ita:2007010
Classification : 68N18, 03B40, 68Q25, 68Q45
Mots-clés : functional programming languages, lambda calculus, strictness analysis, set constraints, tree automata

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

1 Dept. of Mathematics and Computing Science, University of the South Pacific, Suva, Fiji Islands 
@article{ITA_2007__41_2_225_0,
     author = {Schmidt-Schauss, Manfred and Sabel, David and Sch\"utz, Marko},
     title = {Deciding inclusion of set constants over infinite non-strict data structures},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {225--241},
     publisher = {EDP-Sciences},
     volume = {41},
     number = {2},
     year = {2007},
     doi = {10.1051/ita:2007010},
     mrnumber = {2350646},
     language = {en},
     url = {https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2007010/}
}
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 - Informatique Théorique et Applications
PY  - 2007
SP  - 225
EP  - 241
VL  - 41
IS  - 2
PB  - EDP-Sciences
UR  - https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2007010/
DO  - 10.1051/ita:2007010
LA  - en
ID  - ITA_2007__41_2_225_0
ER  - 
%0 Journal Article
%A Schmidt-Schauss, Manfred
%A Sabel, David
%A Schütz, Marko
%T Deciding inclusion of set constants over infinite non-strict data structures
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2007
%P 225-241
%V 41
%N 2
%I EDP-Sciences
%U https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2007010/
%R 10.1051/ita:2007010
%G en
%F ITA_2007__41_2_225_0
Schmidt-Schauss, Manfred; Sabel, David; Schütz, Marko. Deciding inclusion of set constants over infinite non-strict data structures. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 41 (2007) no. 2, pp. 225-241. doi : 10.1051/ita:2007010. https://geodesic-test.mathdoc.fr/articles/10.1051/ita:2007010/

Cité par Sources :