Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_lecture_23 [2007/07/02 17:14] simon.blanchoud |
sav07_lecture_23 [2007/07/02 17:23] simon.blanchoud |
||
---|---|---|---|
Line 111: | Line 111: | ||
Modularity: [[http://doi.acm.org/10.1145/316686.316703|Componential set-based analysis]] | Modularity: [[http://doi.acm.org/10.1145/316686.316703|Componential set-based analysis]] | ||
+ | |||
Line 122: | Line 123: | ||
* regular tree grammars and tree automata ({{set-constraints-impl.ps|Practical aspects of set based analysis}}) | * regular tree grammars and tree automata ({{set-constraints-impl.ps|Practical aspects of set based analysis}}) | ||
* reduction to term algebras ({{http://theory.stanford.edu/~aiken/publications/papers/popl02.pdf|First-order theory of structural subtyping}}) | * reduction to term algebras ({{http://theory.stanford.edu/~aiken/publications/papers/popl02.pdf|First-order theory of structural subtyping}}) | ||
+ | |||
+ | ==== Term Algebras ==== | ||
+ | |||
+ | * $L = \lbrace a, f, \ldots \rbrace$ | ||
+ | * $H$ : set of all ground terms | ||
+ | * First-order theory : $\forall x \exist y . f(f(a,a), x) = f(y, a) \wedge y \neq a$ | ||
+ | This is First-Order Logic (FOL) with variables ! We can relate this to set constraints | ||
+ | |||
+ | ==== Monadic Class of FOL ==== | ||
+ | |||
+ | MFOL has : only unary predicates, no function symbol, quatifiers and logic. | ||
+ | |||
+ | Translating this to our sets language : | ||
+ | F := | ||
Deciding monadic class (({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}})) | Deciding monadic class (({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}})) |