User:Thepigdog/Value Set

From Knowino

Jump to: navigation, search

[edit] Summary

A Value Set is a type used in Constraint Logic Programming which is used to record a set of values allowed for a variables, attached to possible worlds. Value Sets allow us to reason about variables that may take multiple values.

A Value Set is a set of possible values for a variable. Constraint Logic Programming proceeds by "narrowing" this collection of values until only solution values are left. We need to know which "situation" each value is derived from. These situations are called possible worlds.

To describe Value Sets we first introduce possible worlds and then describe value sets in terms of possible worlds. Then we describe rules for working with Value Sets.

[edit] Possible Worlds

In general a Possible World may be thought of as an alternate possible reality that may eventuate under certain conditions.

Specifically in our case a Possible World is described by facts about the values of variables. The possible world is regarded as a set of outcomes and is represented in set builder notation like,

$\{ fact \} \!$

Note that we dont actually specify what the elements of the set are. The elements could be regarded as tuples of values of variables, but this is not necessary for our purposes.

In implementing a Constraint Logic Programming system Possible Worlds are not used to record boolean conditions. Possible Worlds are represented by their identity, and there hierarchical relationship.

However in proving theorems we will regard Possible Worlds as sets controlled by boolean conditions.

[edit] Possible World Set

A Possible World Set is a Partition of a Possible World P. It is a set of possible worlds $S$ such that,

if $X\in S \and Y\in S$ then $X \cup Y$ is empty.

$P = {\bigcup_{s\in S} s}\!$

[edit] Value Set

A Value Set is a set of tagged values. Each value is "tagged" with a possible world that allows us to track the value against a possible world in a calculation. A tagged value is defined by the operator ::

$a = a_v :: a_p\!$

The value of $a\!$ is $a_v\!$ . The possible world of $a\!$ is $a_p\!$

Value Sets are used to model the set of solutions to equations,

[edit] Extended Value

An extended value $e v (x, x V)$ is a pair,

$x$ is a variable
$x V$ is a value set

The following functions are defined,

A set of values,

$v(x_e) = \{ z \in x_V \and z_p \ne \empty : z_v \} \!$

A set of worlds,

$w(x_e) = \{ z \in x_V \and z_p \ne \empty : z_v \} \!$

An extended value is valid if,

[edit] Definition A1

Description

A variables value is in the set of values.

Definition

$x \in v(x_e) \!$

[edit] Definition A2

Description

The possible worlds from a Value Set form a World Set.

Definition

$x_W = \{ z \in x_V \and z_p \ne \empty : z_p \} \!$

[edit] Defintion A3

Description

A World Set covers all possiblities.

Definition

$\alpha = \{ true \} = \bigcup_{w \in x_W} : w \!$

[edit] Definition A4

Description

The possible world for a value for a variable, must have that variable with that value.

Definition

$\forall z \in x_V : z_p \subset \{ x = z_v \} \!$

[edit] Definition A5

Description

Asserting a value set is equivalent to asserting the value.

Definition

$\forall x: x_V \iff x$

This is the definition of what it means to type cast a value set to boolean. If a variable is of type boolean then its value set, type cast to boolean, is equal to the value.

[edit] Definition A6

Description

The value set of a function call on a variable is the same as the value set of the function set applied to the value set of the variable.

Definition

$\forall x: f(x)_V = f_V(x_V)$

for constant functions this reduces to,

$\forall x: f(x)_V = f(x_V)$

[edit] Basic Theorems

[edit] Theorem T1

$x_W \!$ is a partition of $\alpha \!$ .

This follows from A3 and A4.

[edit] Theorem T2

There exists world sets $x_w(z) \!$ such that,

$x \in S \iff x_V = \{ z\in S : z :: x_w(z) \} \!$

Proof:

$x_V = \{ z\in S : z :: x_w(z) \} \!$

Using this value for $x_V\!$ in A1 gives.

$x \in \{ w \in \{ z\in S : z :: x_w(z) \} \and w_p \ne \empty : w_v \} \!$

implies

$x \in S \!$

[edit] Other stuff

The Possible Worlds can be given names $x_w(z) \!$ so,

$x_W = \{ z\in S : x_w(z) \} \!$

Using this definition (A1) and (A2) definition can also be written,

(A1a) $x \in S \iff x_V = \{ z\in S : z :: x_w(z) \} \and x_W = \{ z\in S : x_w(z) \} \!$

(A1b) $x_V = \{ z\in S : z :: x_w(z) \} \implies x \in S \!$

[edit] (B) Functions of a Value Set

The following theorem gives the function on a value set of a type using the function of the type.

(B1) $f(X) = \{x\in X: f(x_v)::x_p\}\!$

Note that for a tagged value $x$ ,

$x = x_v :: x_p \!$

Proof

[edit] Function of multiple Parameters

If we allow Currying then we can extend the above definition to multiple parameters.

If currying is allowed,

$g(x, y) = g_{curry}(x)(y)\!$

The following theorem may then be used,

If $F$ is a value set of functions on a value set of a values,

(B2) $F(X) = \{f\in F, x\in X: f_v(x_v)::f_p\cap x_p\}\!$

Proof

[edit] Function of two parameters

$g(X, Y) = g_{curry}(X)(Y) = \{x\in X: g_{curry}(x_v)::x_p\}(y)\!$

Then the definition for value sets of functions may be applied giving,

$g(X, Y) = \{x\in X, y\in Y: g_{curry}(x_v)(y_v)::x_p\cap y_p\}\!$

or,

(B3) $g(X, Y) = \{x\in X, y\in Y: g(x_v, y_v)::x_p\cap y_p\}\!$

The result can be extended to more parameters.

[edit] (C) Assertions on Value Sets

The above rules allow us to transform a function of variable values into a function about value sets. A statement is a function that is asserted to return the true boolean value. A statement may be transformed into a function that returns a value set.

This is unusual because we dont normally assert a set to be true. But we can think of this polymorphically. A statement returning a value set may be treated differently from a statement returning a boolean.

In this case if $V$ is a value set, the following law applies,

(C1) $V \implies \forall x \in V: x_v \or (x_p = \empty) \!$

Proof

In words, if we assert a Value Set then for every tagged value in the set either the value is true or its possible world is empty. A value tagged with an empty possible world is an impossible value,

(C2) $X = \{x \in X \and x_p \neq \empty : x \} \!$

In other words you can remove all values tagged with the empty possible world from a value set.

[edit] Examples

[edit] Example 1

$x \in \Re \!$

$x^2 = 4 \!$

$x > 0 \!$

Clearly x = 2. But I want to show how this value is derived using value sets. Ultimately the application of these rules is automated into a logic programming system.

[edit] Step 1: Apply A

Using A1,

$x_V = \{ z\in \Re : z :: x_w(z) \} \!$

Using A5 and A6,

$x_V^2 = 4 \!$

$x_V > 0 \!$

Note that the $x_w(z) \!$ are possible worlds from a possible world set in $\alpha \!$ (the actual world).

[edit] Step 2: Apply B

Using (B1) on $x_V^2 = 4 \!$ ,

$\{k \in \{ z\in \Re : z :: x_w(z) \}: k_v^2=4::k_p\}\!$

which simplifies down to,

$\{z \in \Re: z^2=4::x_w(z)\}\!$

[edit] Step 3: Apply C

Using (C1),

$\forall z \in \Re: z^2=4 \or (x_w(z) = \empty) \!$

gives $x_w(z) = \empty \!$ unless $z = 2\!$ or $-2\!$ ,

Using (C2)

$x_V = \{-2::x_w(-2), 2::x_w(2)\}\!$

[edit] Step 4: Apply B again

Using (B1) on $x_V>0 = 4 \!$ ,

$\{-2>0::x_w(-2), -2>0::x_w(-2)\}\!$

[edit] Step 5: Apply C again

Using (C1),

$-2 > 0 \or x_w(-2) = \empty \and 2 > 0 \or x_w(2) = \empty \!$

gives $x_w(-2) = \empty \!$ and so,

$x_V = \{2::x_w(2)\}\!$

$x_W\!$ is a possible world set of $\alpha \!$ (the actual world). As all the possible worlds in the world set except $x_w(2)\!$ are empty we get,

$x_w(2) = \alpha \!$

$x_V = \{ 2::\alpha \}\!$

then from (A1),

$x \in \{2\}\!$

or,

$x = 2\!$

[edit] Example 2

$x \in \{-2, 2\}$

$y = x + x \!$

This example shows how repeated use of a variables are handled. Naively,

$y = -2 + 2 \!$

But this possiblity is removed because the two values are from possible worlds whose intersection is empty.

[edit] Step 1: Apply A

Applying (A1a),

$x_V = \{ -2 :: x_w(-2), 2 :: x_w(2) \} \!$

And using (A4a) and (A4b),

$y_V = x_V + x_V \!$

[edit] Step 2: Apply B

Using (B3),

$y_V = \{ -2 + -2 :: x_w(-2) \cap x_w(-2), -2 + 2 :: x_w(-2) \cap x_w(2), 2 + -2 :: x_w(2) \cap x_w(-2), 2 + 2 :: x_w(2) \cap x_w(2) \} \!$

but,

$x_w(2) \cap x_w(-2) \! = \empty$

so,

$y_V = \{ -2 + -2 :: x_w(-2), -2 + 2 :: \empty, 2 + -2 :: \empty, 2 + 2 :: x_w(2) \cap x_w(2) \} \!$

or,

$y_V = \{ -4 :: x_w(-2), 4 :: x_w(2) \} \!$

[edit] Step 3: Apply A

$y \in \{ -4, 4 \} \!$

[edit] Conclusion

The steps shown in the examples are suited for automating into a algorithm that implements constraint logic programming. The rules are described as mathematics first to give the theory the widest applicability.

User:Thepigdog/Value Set

Contents

[edit] Summary

[edit] Possible Worlds

[edit] Possible World Set

[edit] Value Set

[edit] Extended Value

[edit] Definition A1

[edit] Definition A2

[edit] Defintion A3

[edit] Definition A4

[edit] Definition A5

[edit] Definition A6

[edit] Basic Theorems

[edit] Theorem T1

[edit] Theorem T2

[edit] Other stuff

[edit] (B) Functions of a Value Set

[edit] Function of multiple Parameters

[edit] Function of two parameters

[edit] (C) Assertions on Value Sets

[edit] Examples

[edit] Example 1

[edit] Step 1: Apply A

[edit] Step 2: Apply B

[edit] Step 3: Apply C

[edit] Step 4: Apply B again

[edit] Step 5: Apply C again

[edit] Example 2

[edit] Step 1: Apply A

[edit] Step 2: Apply B

[edit] Step 3: Apply A

[edit] Conclusion

[edit] Links

Personal tools

Namespaces

Variants

Views

Actions

Search

Navigation

Community

Toolbox