Symbolic Logic:Programming:Value Set

From Knowino
Jump to: navigation, search
A Value Set is a single compound value that represents a set of values that a variable may be equal to.

A Value Set is a type which is used to record a set of values allowed for a variable, 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. Evaluation 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.

Contents

[edit] Introduction

Sometimes a variable may have multiple values,

x^2 = 4 \!

Also the logic operations that allow multiple values.

x=2 \or x=-2\!

If we have functions, they should return one value. Then everything is nice and we can feed that value into the next function and get out results without having to think.

What if we could write,

x=\{2, -2\}\!

meaning that the set {2, -2} is the result set. Naively we could calculate results by applying functions to all combination's of the values. However there are problems,

x+x = \{2, -2\}+\{2, -2\} \!

Naively the resulting values are 2+2, 2+-2, -2+2, -2+-2. So 3 values are possible, -4, 0, 4.

x+x = \{4, 0, -4\} \!

But clearly x+x does not equal 4. To get around this problem we need to tag the values with the where the value come from.

Suppose you toss a coin. The result is ether heads or tails. The result cant be both. Its one or the other. These are two different future situations.

So what do we call these future situations? In fact they may not even be in the future. I call them Possible Worlds.

The behaviour of Value Sets is worked out below. Value Sets allow us to work with logic in an easy an intuitive way. And they allow the computer to do the same.

Languages like Prolog handle logic by trying out possibilities and back tracking when they prove inconsistent. Using Value Sets that is not necessary. All calculation is then the evaluation of functions, similar to (but not the same as) Functional Programming].

[edit] How it works

In our example above,

x=2 \or x=-2\!

insert picture here,

The result is,

x=\{2::A, -2::B\} \!

Then

y = x + x=\{2::A, -2::B\}+ \{2::A, -2::B\} = \{2+2::A\cap A,-2+2::A\cap B,-2+2::B\cap A,-2+-2::B\cap B\} \!

But A \cap B is impossible. It is like the coin turning up heads and tails at the same time. So,

y = x + x = \{4::A, -4::B\} \!

Using some simple rules the same method may be applied to any situation.

[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 \cap Y is empty.
P = {\bigcup_{s\in S} s}\!

[edit] Value Set

A Value Set has 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\!

this is purely a notation. The above is a tuple and could also have been written,

a = (a_v, a_p)\!

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

There are multiple ways of representing the same value set. All the representations are regarded as equivalent. Two Value Sets are equal if they represent the same set of values.

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

[edit] (A) Definition of a Value Set

A Value Set is intended to represent the possible values for a variable, attached to possible worlds. For each expression x \! there is a Value Set V(x) \!.

[edit] Notation

A Value Set has a Tagged Set. The distinction is kept because two Value Sets are regarded as equal when there Tagged Sets are not.

If X \! is a value set, its set of expression values is S(X) \! where,

S(X) = \{z_v : z \in X_t \and z_p \ne \empty \} \!

The set of possible worlds is W(X) where,

W(X) = \{z_p : z \in X_t \and z_p \ne \empty \} \!

[edit] Definition A1

Description

A variables value is in the value set of expression values from non empty possible worlds.

Definition

x \in S(V(x)) \!

[edit] Definition A2

Description

Two Value Sets are equivalent if their expression sets are identical.

Definition

X = Y \iff S(X) = S(Y) \!

[edit] Definition A3

Description

A World Set covers all possiblities.

Definition

\alpha = \{ true \} = \bigcup_{w \in W(X)} : 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 {V(x)}_t : z_p \subset \{ x = z_v \} \!

[edit] Definition A5

Description

Asserting a value set is equivalent to asserting the value.

Definition

\forall x: V(x) \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: V(f(x)) = V(f)(V(x))

for constant functions this reduces to,

\forall x: V(f(x)) = f(V(x))

[edit] Basic Theorems

[edit] Theorem T1

W(x) \! is a partition of \alpha \!.

This follows from A3 and A4.

[edit] Theorem T2

x \in S \iff V(x) = v(\{ z :: \{x = z\} : z\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) = v(\{ f(x_v)::x_p : x\in X_t \}) \!

[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) = v(\{ f_v(x_v)::f_p\cap x_p : f\in F, x\in X \})\!

[edit] Function of two parameters

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

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

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

or,

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

The result can be extended to more parameters.

[edit] Function of Vector of Parameters

The result may be generalised to multiple parameters. If x is a vector, and X is a vector of Value Sets (representing multiple parameters) then,

(B4) F(X) = v(\{ f(x_v)::\bigcap_{j \in J} x_p[j] : x\in X \}) \!

[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) \!

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 : x \in X \and x_p \neq \empty \} \!

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

[edit] (D) Resolution

If two Value Sets are equated all but the matching values are removed. This implies that some the Value Sets that dont match are empty. This may mean that other Possible Worlds that are also empty. How do we determine when this occurs?

Definition:

If X is a child of Y, and no Possible World in X is a member of a Possible World in Y then it is empty, as long as the Possible Worlds are in the standard form.

This rule is important in resolving the effects of pruning of Value Sets on each other.

The standard form for Possible Worlds is defined as,

X = f(Y, Z) \!
\forall x_p \in X, y_p \in Y: x_p \subset y_p \or x_p \cap y_p = \empty \!

The formulas for functions of Value Sets are in this form. The form is only broken if Possible Worlds with the same value are merged. This is the form that will be used in the CLP implementation.

If X \!, Y \! and Z \! are a Value Sets, where

X = f(Y, Z) \!

then,

(y_p \in S(Y) \and (\forall x_p \in S(X): x_p \not \subset y_p )) \implies y_p = \empty \!

[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 T2,

V(x) = v(\{ z :: \{x = z\} : z\in \Re \}) \!

Using A5 and A6,

V(x)^2 = 4 \!
V(x) > 0 \!

[edit] Step 2: Apply B

Using (B1) on V(x)^2 = 4 \! ,

V(x^2 = 4) = v(\{k_v^2=4::k_p : k \in \{ z :: \{x = z\} : z\in \Re \} \})\!

which simplifies down to,

V(x^2 = 4) = v(\{z^2=4::\{x = z\} : z \in \Re \})\!

[edit] Step 3: Apply C

Using (C1),

\forall z \in \Re: z^2=4 \or (\{x = z\} = \empty) \!

gives \{x = z\} = \empty \! unless z = 2\! or -2\!,

Using (C2) on V(x)\! tagged values from empty possible worlds can be removed without changing the value of the Value Set.

V(x) = v(\{-2::\{x = -2\}, 2::\{x = 2\}\}) \!

[edit] Step 4: Apply B again

Using (B1) on V(x)>0 \! ,

V(x)>0 = v(\{-2>0::\{x = -2\}, 2>0::\{x = 2\} \})\!

[edit] Step 5: Apply C again

Using (C1) on V(x > 0),

-2 > 0 \or \{x = -2\} = \empty \and 2 > 0 \or \{x = 2\} = \empty \!

gives \{x = -2\} = \empty \! and so,

So using (C2) on V(x)\! drop the tagged value with \{x = -2\} \!.

V(x) = v(\{2::x_w(2)\})\!

then from (A1),

x \in \{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),

V(x) = v(\{ -2 :: \{x=-2\}, 2 :: \{x=2\} \}) \!

And using A6,

V(y) = V(x) + V(x) \!

[edit] Step 2: Apply B

Using (B3),

V(y) = v(\{ -2 + -2 :: \{x=-2\} \cap \{x=-2\}, -2 + 2 :: \{x=-2\} \cap \{x=2\}, 2 + -2 :: \{x=2\} \cap \{x=-2\}, 2 + 2 :: \{x=2\} \cap \{x=-2\} \}) \!

but,

\{x=2\} \cap \{x=-2\} \! = \empty

this is obvious in the example but the law used is that the two possible worlds are from the same World Set,

V(y) = v(\{ -2 + -2 :: \{x=-2\} \cap \{x=-2\}, -2 + 2 :: \empty, 2 + -2 :: \empty, 2 + 2 :: \{x=2\} \cap \{x=-2\} \}) \!

or using C3,

V(y) = \{ -4 :: x_w(-2), 4 :: x_w(2) \} \!

[edit] Step 3: Apply A

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

[edit] Implementation

Constraint Logic Programming systems implements the logic of Value Sets. As part of this implementation the relationship between Value Sets and Possible Worlds is modelled.

[edit] Modelling Possible Worlds and Possible World Sets

Full details of the Possible Worlds do not need to be modelled. The Constraint Logic Programming System only needs to know if the Possible World is empty or not.

The rules in Functions Of a value set describe how values are combined,

(B3) F(X) = v(\{ f(x_v)::\bigcap_{j \in J} x_p[j] : x\in X \}) \!

The Possible World is then,

p = \bigcap_{j \in J} x_p[j] \!

If any of the component x_p[j] \! are empty then p \! is empty.

If none of the x_p[j] \! are empty, the product will still be empty if more than one of the x_p[j] \! are from different values in the same Value Set. As the Possible World Set is a partition the intersection must be empty in that case.

[edit] Links

Personal tools
Variants
Actions
Navigation
Community
Toolbox