Deciding subset relationship of co-inductively defined set constants
Manfred Schmidt-Schauß, David Sabel, Marko Schütz · Publication Server of Goethe University Frankfurt am Main (Goethe University Frankfurt) · 2005
Static analysis of different non-strict functional programming languages makes use of set constants like Top, Inf, and Bot denoting all expressions, all lists without a last Nil as tail, 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. This paper proves decidability, in particular EXPTIME-completeness, of subset relationship of co-inductively defined sets by using algorithms and results from tree automata. This shows decidability of the test for set inclusion, which is required by certain strictness analysis algorithms in lazy functional programming languages.