Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_23 [2007/07/02 17:13]
simon.blanchoud
+++ sav07_lecture_23 [2007/07/02 17:51]
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 :
 \[ 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.
-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 116: / Line 124: @@
   * reduction to term algebras ({{http://theory.stanford.edu/~aiken/publications/papers/popl02.pdf|First-order theory of structural subtyping}})
-Deciding monadic class (({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}}))
+==== Term Algebras ====
-  * reduction to boolean algebras (MSOL fragment, has QE)
-  * small model property
+  * $L = \lbrace a, f, \ldots \rbrace$
-  * resolution variants
+  * $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(({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}}))  has : only unary predicates, no function symbol, quatifiers and logic.
+Translating this to our sets language :
+  F := S = S
+     | S ⊆ S
+     | card(S) ≥ k
+     | card(S) = k
+     | F ∧ F
+     | ¬ F
+     | ∃v.F
+  S := v
+     | S ∪ S
+     | S ∩ S
+     | S'
+     | ∅
+     | 1
+ Where :
+  * $card(S) \geq k$ is syntactic sugar to represent a unary operator, as $k$ is not a variable, that compare the cardinality of $S$ with $k$
+  * $k \geq 0$ is an integer
+  * $S'$ is the complement set of $S$
+  * $1$ represents the whole universe
+ In order to agree with our definitions of set constraints, we need to eliminate :
+  * $S_1 = S_2 \rightarrow S_1 \subseteq S_2 \wedge S_2 \subseteq S_1 $
+  * $S_1 \subseteq S_2 \rightarrow card(S_1 \cup S_2') = 0$
+We then have to be able to represent the following formulas :
+  * $\neg(card(s) \geq k) \rightarrow \bigvee_{i=0}^{k-1} card(S) = i$
+  * $\neg(card(s) = k) \rightarrow card(S) \geq k+1 \vee \bigvee_{i=0}^{k-1} card(S) = i$
+We can then perform quantifier elimination. Note that this is not possible in case we do not have the $card$ operator : \[\exists v.card(S_1 \cap v) = k_1 \wedge card(S_1 \cap v') = k_2 \Rightarrow card(S_1) = k_1 + k_2\]
+After elimination of the quantifiers, deciding the result of the formula is trivial.
+If we add to our language the possibility ot replace $k$ by $card(S)$ then this new language is still decidable and is equivalent to Presbulgarian arithmetic !