Semantica operazionale
Tipi aggiuntivi
Estring
$$ \frac{-} {env \ \triangleright Estring(s) \Rightarrow String(s)} $$

Estype
$$ \frac{-} {env \ \triangleright Estype(t) \Rightarrow Stype(t)} $$

Costruttori
Eset
$$ \frac{ env \ \triangleright t \Rightarrow t_1,\quad \forall e. (e\in s \and \exists !;v.( env \triangleright e \Rightarrow v) \and stypecheck(t_1,v)),\ \ {v\ |\ (\exists\ e\in s\ .\ env\ \triangleright\ e\Rightarrow\ v)}\Rightarrow vList }{env \ \triangleright Eset(t, s) \Rightarrow SetValue(t_1, vList)} $$

EmptySet
$$ \frac{env \ \triangleright t \Rightarrow t_1} {env \ \triangleright EmptySet(t) \Rightarrow SetValue(t_1, \emptyset)} $$

Singleton
$$ \frac{env \ \triangleright t \Rightarrow t_1, \quad {v \ | \ env\ \triangleright e \Rightarrow v\ \and stypecheck(t_1,v)} \Rightarrow vList} {env \ \triangleright Singleton(e, t) \Rightarrow SetValue(t_1, vList)} $$

Operazioni
Union
$$ \frac{ env\ \triangleright set_1 \Rightarrow SetValue(t_1, l_1),\quad env\ \triangleright set_2 \Rightarrow SetValue(t_2, l_2),\quad t_1 = t_2 } {env \ \triangleright Union(set_1, set_2) \Rightarrow SetValue(t_1, l_1 \cup l_2)} $$

Intersection
$$ \frac{ env\ \triangleright set_1 \Rightarrow SetValue(t_1, l_1),\quad env\ \triangleright set_2 \Rightarrow SetValue(t_2, l_2),\quad t_1 = t_2 } {env \ \triangleright Intersection(set_1, set_2) \Rightarrow SetValue(t_1, l_1 \cap l_2)} $$

Difference
$$ \frac{ env\ \triangleright set_1 \Rightarrow SetValue(t_1, l_1),\quad env\ \triangleright set_2 \Rightarrow SetValue(t_2, l_2),\quad t_1 = t_2 } {env \ \triangleright Difference(set_1, set_2) \Rightarrow SetValue(t_1, l_1 \setminus l_2)} $$

Insert
$$ \frac{ env\ \triangleright set \Rightarrow SetValue(t, l),\quad env\ \triangleright e \Rightarrow v,\quad stypecheck(t, v),\quad (v\not \in l) } {env \ \triangleright Insert(set, e) \Rightarrow SetValue(t, l \cup {v})} $$

Remove
$$ \frac{ env\ \triangleright set \Rightarrow SetValue(t, l),\quad env\ \triangleright e \Rightarrow v,\quad stypecheck(t, v),\quad (v \in l) } {env \ \triangleright Remove(set, e) \Rightarrow SetValue(t, l \setminus {v})} $$

IsEmpty
$$ \frac{env\ \triangleright set \Rightarrow SetValue(t, l)} {env \ \triangleright IsEmpty(set) \Rightarrow Bool(l = \emptyset)} $$

IsIn
$$ \frac{env\ \triangleright set \Rightarrow SetValue(t, l),\quad env\ \triangleright e \Rightarrow v} {env \ \triangleright Contains(set, e) \Rightarrow Bool(v \in l)} $$

Subset
$$ \frac{env\ \triangleright set_1 \Rightarrow SetValue(t_1, l_1),\quad env\ \triangleright set_2 \Rightarrow SetValue(t_2, l_2),\quad t_1 = t_2} {env \ \triangleright Subset(set_1, set_2) \Rightarrow Bool(l_1 \subseteq l_2)} $$

Min
$$ \frac{env\ \triangleright set \Rightarrow SetValue(t, l),\quad (l\not= \emptyset),\quad {\exists m\ .\ m\in l \and \forall x\ .(x\in l\ \Rightarrow \ m\le x)}\Rightarrow min} {env \ \triangleright Min(set) \Rightarrow Int(min)} $$

Max
$$ \frac{env\ \triangleright set \Rightarrow SetValue(t, l),\quad (l\not= \emptyset),\quad {\exists m\ .\ m\in l \and \forall x\ .(x\in l\ \Rightarrow \ x\le m)}\Rightarrow max} {env \ \triangleright Max(set) \Rightarrow Int(max)} $$

ForAll
$$ \frac {env\ \triangleright set \Rightarrow SetValue(t, l),\quad env\ \triangleright f\ \Rightarrow funVal,\quad set\Rightarrow (t_1, s), \ (\forall e\in s\ . ((env\ \triangleright FunCall(funVal, e) \Rightarrow res)\ \and\ res = Bool(true) ))\Rightarrow ret} {env\ \triangleright\ ForAll(set, f)\Rightarrow Bool(ret)} $$

Exists
$$ \frac {env\ \triangleright set \Rightarrow SetValue(t, l),\quad env\ \triangleright f\ \Rightarrow funVal,\quad set\Rightarrow (t_1, s), \ (\exists e\in s\ . ((env\ \triangleright FunCall(funVal, e) \Rightarrow res)\ \and\ res = Bool(true) ))\Rightarrow ret} {env\ \triangleright\ Exists(set, f)\Rightarrow Bool(ret)} $$

Filter
$$ \frac {env\ \triangleright set \Rightarrow SetValue(t, l),\quad env\ \triangleright f\ \Rightarrow funVal,\quad set\Rightarrow (t_1, s), \ { v\ |\ \exists e\in s\ . (env\ \triangleright e = v\ \and\ (env\ \triangleright FunCall(funVal, e) \Rightarrow res)\ \and\ res = Bool(true) ))\Rightarrow vList} {env\ \triangleright\ Filter(set, f)\Rightarrow SetValue(t, vList)} $$

Map
$$ \frac{ env\ \triangleright set \Rightarrow SetValue(t, l),\quad env\ \triangleright f\ \Rightarrow funVal,\ set \Rightarrow (t_1, s),\quad env\ \triangleright IsEmpty(set)\Rightarrow isempty, \ isempty \implies (t_{out} := t_1,\ l_{out} := \emptyset), \ \neg isempty \implies (\exists e_0 \in s\ .(extracttype(env\ \triangleright FunCall(funVal, e_0))) \Rightarrow t_{base}, \ (\forall e \in s\ .(extracttype(env\ \triangleright FunCall(funVal, e))) = t_{base}), \ {v\ |\ \exists! e \in s\ .(env \triangleright FunCall(funVal, e) = v} \Rightarrow l_{out}) } {env\ \triangleright\ Map(set, f)\Rightarrow SetValue(type_b, list_b)} $$