User:Thepigdog/Value sets

A Value set is an object, which represents the set of values a variable may have. The value set behaves mathematically as a single value, while internally representing multiple values. To achieve this the the Value Set tracks the value along with the context, or world, in which they occurred.

In mathematics, an expression must represent a single value. For example consider the equation,

:$x^2\; =\; 4$

which implies,

:$x\; =\; 2\; \backslash lor\; x\; =\; -2$

But this is a bit long winded, and it does not allow us to work with multiple values at the same time. If further conditions or constraints are added to x we would like to consider each value to see if it matches the constraint. So naively we would like to write,

:$x\; =\; \backslash pm\; 2$

Naively then,

:$x\; +\; x\; \backslash in\; 2,\; 0,\; -2$

but this is wrong. Each x must represent a single value in the expression. Either x is 2 or x = -2. This can be resolved by keeping track of the two values so that we make sure that the values are used consistently, and this is what a value set does.

The value set for 'x' is written as,

: $V(\backslash \{2\; ::\; x\_1,\; -2\; ::\; x\_2\backslash \})$

It is container V which has a set of tag, value pairs,

• $2\; ::\; x\_1$
• $-2\; ::\; x\_2$

The value 2 is associated with the possible world $x\_1$. The value -2 is associated with the possible world $x\_2$. This means that the value cannot be both 2 and -2 at the same time. In the world $x\_1$ the value of the value set must be 2. In the world $x\_2$ the value of the value set must be -2.

The solution of the equation,

:$x^2\; =\; 4$

is,

: $x\; =\; V(\backslash \{2\; ::\; x\_1,\; -2\; ::\; x\_2\backslash \})$

A world set is a set of possible worlds that represent all possibilities. So $\backslash \{x\_1,\; x\_2\backslash \}$ is a world set as either x = 2 (in world $x\_1$) or x= -2 (in world $x\_2$). There are no other possibilities.

Worlds from the same world set are mutually exclusive, so it is not possible that the propositions for both worlds $x\_1$ and $x\_2$ are true at the same time.

:$(x\; =\; 2\; \backslash land\; x\; =\; -2)\; =\; \backslash text\{false\}$

The rule for the application of functions to value sets is,

:$V(M)\backslash \; V(N)\; =\; V(\backslash \{(m\_v\backslash \; n\_v,\; m\_l\; \backslash cap\; n\_l)\; :\; m\_v\; ::\; m\_l\; \backslash in\; M\; \backslash land\; n\_v\; ::\; n\_l\; \backslash in\; N\backslash \})$

For example,

: $x\; +\; x\; =\; V(\backslash \{2\; ::\; x\_1,\; -2\; ::\; x\_2\backslash \})\; +\; V(\backslash \{2\; ::\; x\_1,\; -2\; ::\; x\_2\backslash \})$

is,

: $=\; V(\backslash \{-2+-2\; ::\; x\_1\; \backslash cap\; x\_1,\; -2+2\; ::\; x\_1\; \backslash cap\; x\_2,\; 2+-2\; ::\; x\_1\; \backslash cap\; x\_2,\; 2+2\; ::\; x\_2\backslash \})$

: $=\; V(\backslash \{-4\; ::\; x\_1\; \backslash cap\; x\_1,\; 0\; ::\; x\_1\; \backslash cap\; x\_2,\; 0\; ::\; x\_2\; \backslash land\; x\_1,\; 2+2\; ::\; x\_2\; \backslash cap\; x\_1\backslash \})$

The intersection of the possible world with itself is the possible world,

: $x\_1\; \backslash cap\; x\_1\; =\; x\_1$

: $x\_2\; \backslash cap\; x\_2\; =\; x\_2$

The intersection of the possible world with another possible world from the same world set is empty,

: $x\_1\; \backslash cap\; x\_2\; =\; \backslash \{\backslash \}$

: $x\_2\; \backslash cap\; x\_1\; =\; \backslash \{\backslash \}$

So,

: $=\; V(\backslash \{-4\; ::\; x\_1,\; 0\; ::\; \backslash \{\backslash \},\; 0\; ::\; \backslash \{\backslash \},\; 4\; ::\; x\_2\; \backslash \})$

The empty worlds rule allows tagged values from empty worlds to be dropped

:$V(K)\; =\; V(\backslash \{(v,\; l)\; :\; (v,\; l)\; \backslash in\; K\; \backslash land\; l\; \backslash ne\; \backslash \{\backslash \}\; \backslash \}$

giving,

: $=\; V(\backslash \{-4\; ::\; x\_1,\; 4\; ::\; x\_2\; \backslash \})$

Giving the result that $x\; +\; x$ is either -4 or 4, as expected.

: $a\; \backslash land\; b$

Is a relationship between a, b and true that implies that both a and b must be true.

: $a\; \backslash lor\; b$

Allows multiple values for a and b. If a is,

: $a\; =\; V(\backslash \{\backslash operatorname\{false\}\; ::\; a\_1,\; \backslash operatorname\{true\}\; ::\; a\_2\; \backslash \})$

then for b

: $b\; =\; V(\backslash \{\backslash operatorname\{true\}\; ::\; a\_1,\; \backslash operatorname\{false\}\; ::\; a\_2,\; \backslash operatorname\{true\}\; ::\; a\_2\; \backslash \})$

This means that if a is false then b must be true.

Now consider,

: $x\; =\; 2\; \backslash lor\; x\; =\; -2$

gives,

: $x\; =\; V(\backslash \{\backslash \_\; ::\; a\_1,\; 2\; ::\; a\_2\; \backslash \})$

and

: $x\; =\; V(\backslash \{-2\; ::\; a\_1,\; \backslash \_\; ::\; a\_2,\; -2\; ::\; a\_2\; \backslash \})$

unifying these two value sets gives,

: $x\; =\; V(\backslash \{-2\; ::\; a\_1,\; 2\; ::\; a\_2\backslash \})$

The pair $-2\; ::\; a\_2$ is dropped because of the "assert equal" rule,

:$\backslash forall\; m\_v\; \backslash forall\; m\_l\; \backslash forall\; n\_v\; \backslash forall\; n\_l\; ((m\_v,\; m\_l)\; \backslash in\; M\; \backslash land\; (n\_v,\; n\_l)\; \backslash in\; N)\; \backslash to\; (m\_v\; \backslash ne\; n\_v\; \backslash to\; m\_l\backslash cap\; n\_l\; =\; \backslash \{\backslash \}\; )$

Its value $-2\; ::\; a\_2$ did not match with $2\; ::\; a\_2$.