Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav07_lecture_23 [2007/07/02 17:13] simon.blanchoud |
sav07_lecture_23 [2007/07/02 17:23] simon.blanchoud |
||
|---|---|---|---|
| Line 71: | Line 71: | ||
| We also define $S_I$ as the set of all possibly called methods that we can build using the following formula : | We also define $S_I$ as the set of all possibly called methods that we can build using the following formula : | ||
| \[ main \in S_I \bigwedge_{m \in M} \left ( m \in S_I \wedge p \in calls(m) \right ) \Rightarrow S_p \subseteq S_I \bigwedge_{m \in M} m \in S_I \Rightarrow inst(m) \subseteq S_I \] | \[ main \in S_I \bigwedge_{m \in M} \left ( m \in S_I \wedge p \in calls(m) \right ) \Rightarrow S_p \subseteq S_I \bigwedge_{m \in M} m \in S_I \Rightarrow inst(m) \subseteq S_I \] | ||
| + | |||
| Line 104: | Line 105: | ||
| In this particular case, the fixpoint is : $Atom \cup And(res, res) \cup Not(res) \subseteq res$ which computes correctly the fact that the $Or$ has been removed. | In this particular case, the fixpoint is : $Atom \cup And(res, res) \cup Not(res) \subseteq res$ which computes correctly the fact that the $Or$ has been removed. | ||
| - | This example shows that we can use set constraints to create type systems ! | + | This example shows that we can use set constraints to create type systems ! Read the following papers for more information : |
| + | |||
| + | * [[http://theory.stanford.edu/~aiken/publications/papers/fpca93.ps|Type inference]]. Semantics of untyped lambda calculus. | ||
| + | * [[http://theory.stanford.edu/~aiken/publications/papers/popl94.ps|Soft typing with conditional types]] | ||
| + | |||
| + | Modularity: [[http://doi.acm.org/10.1145/316686.316703|Componential set-based analysis]] | ||
| + | |||
| Line 115: | 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}})) | ||