Narrowing of algebraic value sets

Like logic programming, narrowing of algebraic value sets gives a method of reasoning about the values in unsolved or partially solved equations. Where logic programming relies on resolution, the algebra of value sets relies on narrowing rules. Narrowing rules allow the elimination of values from a solution set which are inconsistent with the equations being solved.

Unlike logic programming, narrowing of algebraic value sets makes no use of backtracking. Instead all values are contained in value sets, and are considered in parallel.

The approach is also similar to the use of constraints in constraint logic programming, but without the logic processing basis.

Probabilistic value sets is a natural extension of value sets to deductive probability. The value set construct holds the information required to calculate probabilities of calculated values based on probabilities of initial values.

History

Early programming languages were imperative. These implement functionality by allowing change to be represented. The assignment statement allows a variable to change its value.

In mathematics a variable's value may not change. This is fundamental to the mathematical approach. Functional languages based on lambda calculus allow this mathematical approach to programming. Functional languages developed by implementing lazy evaluation, and allowing functions to be passed as parameters.

Lazy evaluation is an essential feature of modern functional programming languages such as Haskell. Haskell is the latest in a series of languages based on lambda calculus and let expressions. These languages provide rich functionality through lazy evaluation, and a polymorphic type system using type inference. Functional programming languages also naturally support higher-order functions.

Logic programming based on Resolution developed alongside functional programming. Logic programming is a form of relational programming that makes deductions about values. Constraint logic programming extends logic programming, by supporting constraints. Constraint logic programming languages such as ECLiPSe provide the ability to solve complex logic problems. However ECLiPSe is not lazy.

Logic programming languages, although they have greater deduction abilities, never gained the power and flexibility of functional languages.

Narrowing is a technique that allows logical deduction, with the flexibility of functional languages.

Introduction

In mathematics an expression represents a single value. A function maps one or more values to one unique value.

Inverses of functions are not always well defined as functions. Sometimes extra conditions are required to make an inverse of a function fit the definition of a function.

Some Boolean operations, in particular do not have inverses that may be defined as functions. In particular the disjunction "or" has inverses that allow two values. In natural language "or" represents alternate possibilities.

Narrowing is based on value sets that allow multiple values to be packaged and considered as a single value. This allows the inverses of functions to always be considered as functions.

To achieve this value sets must record the context to which a value belongs. A variable may only take on a single value in each possible world. The value sets tag each value in the value set with the world to which it belongs.

Possible worlds belong to world sets. A world set is a set of all mutually exclusive worlds. Combining values from different possible worlds is impossible, because that would mean combining mutually exclusive possible worlds.

The application of functions to value sets creates combinations of value sets from different worlds. Narrowing reduces those worlds by eliminating combinations of different worlds from the same world set. Narrowing rules also detect situations where some combinations of worlds are shown to be impossible.

No back tracking is required in the use of narrowing. By packaging the possible values in a value set all combinations of values may be considered at the same time. Evaluation proceeds as for a functional language, combining combinations of values in value sets, with narrowing rules eliminating impossible values from the sets.

Introduction to 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 value set tracks the value along with the context, or world, in which they occurred.

Multiple solutions to an equation

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

[math]\displaystyle{ x^2 = 4 }[/math]

which implies,

[math]\displaystyle{ x = 2 \lor x = -2 }[/math]

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,

[math]\displaystyle{ x = \pm 2 }[/math]

Naively then,

[math]\displaystyle{ x + x \in \lbrace 4, 0, -4 \rbrace }[/math]

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.

Representation

The value set for 'x' is written as,

[math]\displaystyle{ V(\{2 :: x_1, -2 :: x_2\}) }[/math]

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

• [math]\displaystyle{ 2 :: x_1 }[/math]
• [math]\displaystyle{ -2 :: x_2 }[/math]

The value 2 is associated with the possible world [math]\displaystyle{ x_1 }[/math]. The value −2 is associated with the possible world [math]\displaystyle{ x_2 }[/math]. This means that the value cannot be both 2 and −2 at the same time. In the world [math]\displaystyle{ x_1 }[/math] the value of the value set must be 2. In the world [math]\displaystyle{ x_2 }[/math] the value of the value set must be −2.

The solution of the equation,

[math]\displaystyle{ x^2 = 4 }[/math]

is,

[math]\displaystyle{ x = V(\{2 :: x_1, -2 :: x_2\}) }[/math]

Possible worlds

A possible world is used here as an informal term. Formally a possible world is defined by a Boolean condition. A possible world may be considered the set of possibilities for the world that match the condition.

The term "possible world" is used to make the description of value sets easier to follow.

World sets

A world set is a set of possible worlds that represent all possibilities. So [math]\displaystyle{ \{x_1, x_2\} }[/math] is a world set as either x = 2 (in world [math]\displaystyle{ x_1 }[/math]) or x= −2 (in world [math]\displaystyle{ x_2 }[/math]). 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 [math]\displaystyle{ x_1 }[/math] and [math]\displaystyle{ x_2 }[/math] are true at the same time.

[math]\displaystyle{ (x = 2 \land x = -2) = \text{false} }[/math]

Application of functions

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

[math]\displaystyle{ V(M)\ V(N) = V(\{(m_v\ n_v, m_l \cap n_l) : m_v :: m_l \in M \land n_v :: n_l \in N\}) }[/math]

For example,

[math]\displaystyle{ x + x = V(\{2 :: x_1, -2 :: x_2\}) + V(\{2 :: x_1, -2 :: x_2\}) }[/math]

is,

[math]\displaystyle{ = V(\{-2+-2 :: x_1 \cap x_1, -2+2 :: x_1 \cap x_2, 2+-2 :: x_1 \cap x_2, 2+2 :: x_2\}) }[/math]

[math]\displaystyle{ = V(\{-4 :: x_1 \cap x_1, 0 :: x_1 \cap x_2, 0 :: x_2 \land x_1, 2+2 :: x_2 \cap x_1\}) }[/math]

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

[math]\displaystyle{ x_1 \cap x_1 = x_1 }[/math]

[math]\displaystyle{ x_2 \cap x_2 = x_2 }[/math]

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

[math]\displaystyle{ x_1 \cap x_2 = \{\} }[/math]

[math]\displaystyle{ x_2 \cap x_1 = \{\} }[/math]

So,

[math]\displaystyle{ = V(\{-4 :: x_1, 0 :: \{\}, 0 :: \{\}, 4 :: x_2 \}) }[/math]

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

[math]\displaystyle{ V(K) = V(\{(v, l) : (v, l) \in K \land l \ne \{\} \} }[/math]

giving,

[math]\displaystyle{ = V(\{-4 :: x_1, 4 :: x_2 \}) }[/math]

Giving the result that [math]\displaystyle{ x + x }[/math] is either −4 or 4, as expected.

Application to Booleans

[math]\displaystyle{ a \land b }[/math]

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

[math]\displaystyle{ a \lor b }[/math]

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

[math]\displaystyle{ a = V(\{\operatorname{false} :: a_1, \operatorname{true} :: a_2 \}) }[/math]

then for b

[math]\displaystyle{ b = V(\{\operatorname{true} :: a_1, \operatorname{false} :: a_2, \operatorname{true} :: a_2 \}) }[/math]

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

Now consider,

[math]\displaystyle{ x = 2 \lor x = -2 }[/math]

gives,

[math]\displaystyle{ x = V(\{\_ :: a_1, 2 :: a_2 \}) }[/math]

and

[math]\displaystyle{ x = V(\{-2 :: a_1, \_ :: a_2, -2 :: a_2 \}) }[/math]

unifying these two value sets gives,

[math]\displaystyle{ x = V(\{-2 :: a_1, 2 :: a_2\}) }[/math]

The pair [math]\displaystyle{ -2 :: a_2 }[/math] is dropped because of the "assert equal" rule,

[math]\displaystyle{ \forall m_v \forall m_l \forall n_v \forall n_l ((m_v, m_l) \in M \land (n_v, n_l) \in N) \to (m_v \ne n_v \to m_l\cap n_l = \{\} ) }[/math]

Its value [math]\displaystyle{ -2 :: a_2 }[/math] did not match with [math]\displaystyle{ 2 :: a_2 }[/math].

Dependent worlds

Consider the problem,

[math]\displaystyle{ X = V(\{1 :: x_1, 3 :: x_2, 4 :: x_3\}) }[/math]

[math]\displaystyle{ Y = V(\{8 :: y_1, 9 :: y_2\}) }[/math]

[math]\displaystyle{ X * Y \lt 25 }[/math]

[math]\displaystyle{ X + Y \gt 10 }[/math]

Firstly calculate the value set for [math]\displaystyle{ X * Y \lt 25 }[/math],

[math]\displaystyle{ V(\{8 :: x_1 \cap y_1, 24 :: x_2 \cap y_1, 32 :: x_3 \cap y_1, 9 :: x_1 \cap y_2, 27 :: x_2 \cap y_2, 36 :: x_3 \cap y_2\}) \lt 25 }[/math]

[math]\displaystyle{ V(\{8\lt 25 :: x_1 \cap y_1, 24\lt 25 :: x_2 \cap y_1, 32\lt 25 :: x_3 \cap y_1, 9\lt 25 :: x_1 \cap y_2, 27\lt 25 :: x_2 \cap y_2, 36\lt 25 :: x_3 \cap y_2\}) \lt 25 }[/math]

[math]\displaystyle{ V(\{\text{true} :: x_1 \cap y_1, \text{true} :: x_2 \cap y_1, \text{false} :: x_3 \cap y_1, \text{true} :: x_1 \cap y_2, \text{false} :: x_2 \cap y_2, \text{false} :: x_3 \cap y_2\}) }[/math]

As this statement is asserted true, all the false values are dropped giving,

[math]\displaystyle{ V(\{\text{true} :: x_1 \cap y_1, \text{true} :: x_2 \cap y_2, \text{true} :: x_1 \cap y_2\}) }[/math]

The worlds,

[math]\displaystyle{ x_3 \cap y_1 }[/math]

[math]\displaystyle{ x_2 \cap y_2 }[/math]

[math]\displaystyle{ x_3 \cap y_2 }[/math]

are impossible. The worlds are empty.

If a world set is included in a calculation then every world from the world set must be included in the result. If a world is not found, it is called a dependent world, and must be empty. The world [math]\displaystyle{ X_3 }[/math] is not represented in this value, and so must be empty. The value set for [math]\displaystyle{ X }[/math] is now smaller,

[math]\displaystyle{ X = V(\{1 :: x_1, 3 :: x_2\}) }[/math]

The second condition is now simpler, because of the smaller value set.

[math]\displaystyle{ X + Y \gt 10 }[/math]

Then the value sets are,

[math]\displaystyle{ X = V(\{1 :: x_1, 3 :: x_2\}) }[/math]

[math]\displaystyle{ Y = V(\{8 :: y_1, 9 :: y_2\}) }[/math]

And the calculation is,

[math]\displaystyle{ V(\{1+8 :: x_1 \cap y_1, 3+8 :: x_2 \cap y_1, 2+9 :: x_1 \cap y_2, 1+9 :: x_2 \cap y_2\}) \gt 10 }[/math]

But [math]\displaystyle{ x_2 \cap y_2 }[/math] is empty. So,

[math]\displaystyle{ V(\{9\gt 10 :: x_1 \cap y_1, 11\gt 10 :: x_2 \cap y_1, 10\gt 10 :: x_1 \cap y_2\}) }[/math]

So [math]\displaystyle{ x_1 \cap y_1 }[/math] and [math]\displaystyle{ x_1 \cap y_2 }[/math] are empty,

[math]\displaystyle{ V(\{11\gt 10 :: x_2 \cap y_1\}) }[/math]

Now [math]\displaystyle{ X_1 }[/math] and [math]\displaystyle{ Y_2 }[/math] are not represented, and are removed as dependent worlds. So,

[math]\displaystyle{ X = V(\{3 :: x_2\}) = 3 }[/math]

[math]\displaystyle{ Y = V(\{8 :: y_1\}) = 8 }[/math]

Every calculation made may reduce the size of value sets by removing dependent worlds, but add a new value set whose size is the product of the sizes of the input value sets. Then calculations should proceed first where the product of the sizes of the input value sets is smallest.

Pizza, beer, whiskey

After a hard day's work attempting to meet some crazy deadline with the project from hell, there comes that desperate time at 10 PM when we all need pizza, beer, and whiskey. Pizza shops are open at,

[math]\displaystyle{ \text{PizzaShop}(V(\{\text{Carlton}::p_1, \text{Richmond}::p_2, \text{South Melbourne}::p_3, \text{Footscray}::p_4, \text{St Kilda}::p_5, \text{Toorak}::p_6\})) }[/math]

Beer you can get at,

[math]\displaystyle{ \text{BottleshopWithBeer}(V(\{\text{South Melbourne}::b_1, \text{St Kilda}::b_2, \text{Carlton}::b_3, \text{Docklands}::b_4\})) }[/math]

Whiskey,

[math]\displaystyle{ \text{BottleshopWithWhiskey}(V(\{\text{Essendon}::w_1, \text{South Melbourne}::w_2\})) }[/math]

The cops are about and we are not getting any younger. Where to go?

[math]\displaystyle{ \text{WhereToGo}(x) = \text{PizzaShop}(x) \land \text{BottleshopWithBeer}(x) \land \text{BottleshopWithWhiskey}(x) }[/math]

If the constraints are applied in the order left to right,

[math]\displaystyle{ x = V(\{\text{Carlton}::p_1, \text{Richmond}::p_2, \text{South Melbourne}::p_3, \text{Footscray}::p_4, \text{St Kilda}::p_5, \text{Toorak}::p_6\}) }[/math]

Then we need to unify this with,

[math]\displaystyle{ x = V(\{\text{South Melbourne}::b_1, \text{St Kilda}::b_2, \text{Carlton}::b_3, \text{Docklands}::b_4\}) }[/math]

This will create 24 combinations from which the matching ones are,

[math]\displaystyle{ x = V(\{\text{South Melbourne}::b_1 \cap p_3, \text{St Kilda}::b_2 \cap p_5, \text{Carlton}::b_3 \cap p_1\}) }[/math]

Finally we need to unify with whiskey.

[math]\displaystyle{ x = V(\{\text{Essendon}::w_1, \text{South Melbourne}::w_2\}) }[/math]

Which gives 6 combinations. The matching one is,

[math]\displaystyle{ x = V(\{\text{South Melbourne}::b_1 \cap p_3 \cap w_2\}) }[/math]

A total of 30 combinations were generated.

If the constraints are applied in the order right to left,

[math]\displaystyle{ x = V(\{\text{Essendon}::w_1, \text{South Melbourne}::w_2\}) }[/math]

Then we need to unify this with,

[math]\displaystyle{ x = V(\{\text{South Melbourne}::b_1, \text{St Kilda}::b_2, \text{Carlton}::b_3, \text{Docklands}::b_4\}) }[/math]

This will create 8 combinations from which the matching one is,

[math]\displaystyle{ x = V(\{\text{South Melbourne}::b_1 \cap w_2\}) }[/math]

Finally we need to unify with pizza.

[math]\displaystyle{ x = \{\text{Carlton}::p_1, \text{Richmond}::p_2, \text{South Melbourne}::p_3, \text{Footscray}::p_4, \text{St Kilda}::p_5, \text{Toorak}::p_6\} }[/math]

Which gives 6 combinations. The matching one is,

[math]\displaystyle{ x = V(\{\text{South Melbourne}::b_1 \cap w_2\ \cap p_3 \}) }[/math]

The result is the same but only 14 combinations were generated to arrive at the conclusion.

Every calculation combines value sets to create a value set which is the product of the sizes of the input value sets. The value set will then be trimmed down. And every calculation has an equal chance of narrowing the calculation. So by controlling the order and proceeding with calculations with the smallest product of sizes, there will be less calculation and less combinatorial explosion.

Let expressions and multiple values

A general solution to the problem of inverses of functions that are not functions is needed. What is required is a representation of a value that is constrained to be a member of a set of values. A let expression may be used to represent a value that is a member of a set,

[math]\displaystyle{ \operatorname{let} x \in X \operatorname{in} x }[/math]

In this expression [math]\displaystyle{ x \in X }[/math] is a constraint. A constraint is a Boolean expression that a variable must satisfy. The let expression allows the constraint be represented in an expression. If there was a general rule for function application of constraint expressions, then a constraint could be treated like a value.

Under function application, of one let expression to another,

[math]\displaystyle{ (\operatorname{let} x \in X \operatorname{in} x)\ (\operatorname{let} y \in Y \operatorname{in} y) }[/math]

[math]\displaystyle{ = \operatorname{let} x \in X \land y \in Y \operatorname{in} x\ y }[/math]

[math]\displaystyle{ = \operatorname{let} (x, y) \in X \times Y \operatorname{in} x\ y }[/math]

But a different rule applies for applying the let expression to itself. The let expression does not restrict the scope of the variable x, so x is the same variable in the two let expressions.

[math]\displaystyle{ (\operatorname{let} x \in X \operatorname{in} x)\ (\operatorname{let} x \in X \operatorname{in} x) }[/math]

[math]\displaystyle{ = \operatorname{let} x \in X \operatorname{in} x\ x }[/math]

There appears no simple rule for combining let expressions. What is required is a general form of expression that represents a variable whose value is a member of a set of values. The expression should be based on the variable and the set.

Function application applied to this form should give another expression in the same form. In this way any expression on functions of multiple values may be treated as if it had one value.

It is not sufficient for the form to represent only the set of values. Each value must have a condition that determines when the expression takes the value. The resulting construct is a set of pairs of conditions and values, called a "value set".

Theory of value sets

A "value set" K is defined as a set of pairs, each pair consisting of a value and a set of dependent conditions. The set of dependent conditions is used by the "condition function", to determine if the value set takes that value.

The condition function is defined by 3 axioms,

1. Each pair [math]\displaystyle{ (v, l) }[/math] means that the value of the value set [math]\displaystyle{ V(K) }[/math] is v if the condition function applied to the list, [math]\displaystyle{ C(l) }[/math], is true.
2. One of the conditions is true.
3. Only one of the conditions is true.

The condition is represented as a function applied to a set of dependent conditions, to allow the structure of the condition to be controlled. Also the set of conditions is used in narrowing by exclusion of dependent values. However for most purposes the value set may be thought of as a set of value, condition pairs. The condition function translates the set into the condition.

Formally,

Name	Definition
Condition function	[math]\displaystyle{ C(l) = ({\bigwedge_{(r, z, u) \in l} z = u})) = (\forall r \forall z \forall u (r, z, u) \in l \to z = u) }[/math]
Value condition	[math]\displaystyle{ \forall v \forall l ((v, l) \in K \land C(l) \to v = V(K) }[/math]
Complete set	[math]\displaystyle{ \exists v \exists l (v, l) \in K \land C(l) }[/math]
Exclusion	[math]\displaystyle{ \forall v_1 \forall l_1 \forall v_2 \forall l_2 ((v_1, l_1) \in K \land (v_2, l_2) \in K \land (v_1, l_1) \ne (v_2, l_2)) \to \neg (C(l_1) \land C(l_2)) }[/math]

Value function

Using the value condition and complete set axioms,

[math]\displaystyle{ \exists v \exists l (v, l) \in K \land C(l) \land v = V(K) }[/math]

As a let expression this becomes,

[math]\displaystyle{ V(K) = \operatorname{let} (v, l) \in K \land C(l) \operatorname{in} v }[/math]

Single value

The value set to represent a single value is,

[math]\displaystyle{ k = V(\{(k, \{\})\}) }[/math]

The derivation is,

[math]\displaystyle{ V(\{(k, \{\})\}) }[/math]

[math]\displaystyle{ = \operatorname{let} (v, l) \in \{(k, \{\})\} \land C(l) \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} v = k \land C(\{\}) \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} v = k \operatorname{in} v }[/math]

[math]\displaystyle{ = k }[/math]

Element of a set

The value set to represent an element of a set is,

[math]\displaystyle{ \forall x \forall X (\operatorname{let} x \in X \operatorname{in} x) = \operatorname{let} R = V(\{(w, \{(R, x, w)\}) : w \in X\}) \operatorname{in} R }[/math]

This rather strange definition adds the value set in as part of the dependent condition. This is used in narrowing by exclusion of dependent values.

The value of the expression is

[math]\displaystyle{ x = V(R) }[/math].

Both R and x must be included in the dependent condition, because R identifies the value set to which the dependent condition belongs, and x provides the variable used to carry the value in the let expression.

If the addition of R to the dependent condition is ignored, the expression takes on a simpler and more understandable form,

[math]\displaystyle{ \forall x \forall X (\operatorname{let} x \in X \operatorname{in} x) = V(\{(w, \{(\_, x, w)\}) : w \in X\}) }[/math]

The derivation is,

[math]\displaystyle{ V(\{(w, \{(r, x, w) : w \in X\}) }[/math]

[math]\displaystyle{ = \operatorname{let} (v, l) \in \{(w, \{(r, x, w)\}) : w \in X\} \land C(l) \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} v \in X \land ({\bigwedge_{(r, z, u) \in \{(\_, x, v)\}} z = u}) \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} v \in X \land (\forall r \forall z \forall u (r, z, u) \in \{(\_, x, v)\} \to z = u) \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} v \in X \land x = v \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} x \in X \operatorname{in} x }[/math]

Application of functions

Function application of value sets is given by,

[math]\displaystyle{ V(M)\ V(N) = V(\{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \land (n_v, n_l) \in N\}) }[/math]

Derivation,

[math]\displaystyle{ V(M)\ V(N) }[/math]

[math]\displaystyle{ = \operatorname{let} (m_v, m_l) \in M \land C(m_l) \operatorname{in} m_v)\ (\operatorname{let} (n_v, n_l) \in N \land C(n_l) \operatorname{in} n_v) }[/math]

[math]\displaystyle{ = \operatorname{let} (m_v, m_l) \in M \land (n_v, n_l) \in N \land C(n_l) \land C(n_l) \operatorname{in} m_v\ n_v) }[/math]

Then using,

[math]\displaystyle{ C(m_l) \land C(n_l) }[/math]

[math]\displaystyle{ = ({\bigwedge_{(z, u) \in m_l} z = u}) \land ({\bigwedge_{(z, u) \in n_l} z = u}) }[/math]

[math]\displaystyle{ = ({\bigwedge_{(z, u) \in m_l \cup n_l} z = u}) }[/math]

[math]\displaystyle{ = C(m_l \cup n_l) }[/math]

get,

[math]\displaystyle{ = \operatorname{let} (m_v, m_l) \in M \land (n_v, n_l) \in N \land C(n_l \cup n_l) \operatorname{in} m_v\ n_v) }[/math]

[math]\displaystyle{ = \operatorname{let} (v, l) \in \{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \land (n_v, n_l) \in N\} \land C(l) \operatorname{in} v }[/math]

[math]\displaystyle{ = V(\{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \land (n_v, n_l) \in N\}) }[/math]

Exclusion

The exclusion is a rule that determines when conditions must be false,

[math]\displaystyle{ V(M) \in s \iff (\forall v \forall l ((v, l) \in M \land v \not \in s) \to \neg C(l)) }[/math]

This may be derived from,

[math]\displaystyle{ V(M) \in s }[/math]

[math]\displaystyle{ \to \forall v \forall l ((v, l) \in M \land C(l)) \to (v = V[M] \land V(M) \in s) }[/math]

[math]\displaystyle{ \to \forall v \forall l ((v, l) \in M \land C(l)) \to v \in S }[/math]

[math]\displaystyle{ \to \forall v \forall l ((v, l) \in M \land v \not \in S) \to \neg C(l) }[/math]

Simplification

The simplification rule allows values whose condition is false to be dropped.

[math]\displaystyle{ V(K) = V(\{(v, l) : (v, l) \in K \land C(l)\} }[/math]

Derivation

[math]\displaystyle{ V(\{(v, l) : (v, l) \in K \land C(l)\}) }[/math]

[math]\displaystyle{ = \operatorname{let} (v, l) \in \{(v, l) : (v, l) \in K \land C(l)\} \land C(l) \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} (v, l) \in K \land C(l) \land C(l) \operatorname{in} v }[/math]

[math]\displaystyle{ = \operatorname{let} (v, l) \in K \land C(l) \operatorname{in} v }[/math]

[math]\displaystyle{ = V(K) }[/math]

Summary of results

Name	Rule
Value function	[math]\displaystyle{ V(K) = \operatorname{let} (v, l) \in K \land C(l) \operatorname{in} v }[/math]
Single value	[math]\displaystyle{ k = V(\{(k, \{\})\}) }[/math]
Set element	[math]\displaystyle{ \forall x \forall X (\operatorname{let} x \in X \operatorname{in} x) = \operatorname{let} R = V(\{(w, \{(R, x, w)\}) : w \in X\}) \operatorname{in} R }[/math]
Function application	[math]\displaystyle{ V(M)\ V(N) = V(\{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \land (n_v, n_l) \in N\}) }[/math]
Exclusion	[math]\displaystyle{ V(M) \in s \iff (\forall v \forall l ((v, l) \in M \land v \not \in s) \to \neg C(l)) }[/math]
Simplification	[math]\displaystyle{ V(K) = V(\{(v, l) : (v, l) \in K \land C(l)\}) }[/math]
Assert equal	[math]\displaystyle{ V(M) = V(N) \to (\forall v \forall l ((v, l) \in N \land v \not \in S(M)) \to \neg C(l)) }[/math]

A value sets identity

By defining the application of functions to value sets the definition of equality of value sets has also been redefined. The old definition of equality still exists, because value sets are constructed as a set of pairs. Two sets are equal if they contain the same elements. This definition of equality for value sets is at best misleading.

What is needed is to use the name, or identity of the variable from which the value set is constructed as part of the structure of the value set. This would make value sets distinct, unless they are based on the same variable.

In mathematics, quantification is over values, not formulas. To proceed further with the exact definition of value sets, quantification over formulas is needed, in a way that allows the comparison of the identity of formulas. The distinction between the formula representing a value and the identity of the formula is the use–mention distinction. The notation,

[math]\displaystyle{ \forall x \#u }[/math]

is introduced to mean quantification over formula x where x refers to the value, as a use, and u refers to the identity of the formula as represented or mentioned.

Using this notation the element of a set definition would be,

[math]\displaystyle{ \forall x \#u \forall X (\operatorname{let} x \in X \operatorname{in} x) = \operatorname{let} R = V((u, \{(w, \{(R, x, w)\}) : w \in X\})) \operatorname{in} R }[/math]

Every reference to a value set would then need to be changed to take account of the extra level of structure in the value set, which would make the description harder to read. For the sake of readability this extra level of structure has been omitted from the definition of value sets.

Narrowing

"Narrowing" is determining when conditions for values must be false. Narrowing starts when the value of two value sets is asserted equal.

Narrowing by asserting equal

Assertion that two value sets are equal gives the narrowing rule,

[math]\displaystyle{ \forall m_v \forall m_l \forall n_v \forall n_l ((m_v, m_l) \in M \land (n_v, n_l) \in N) \to (m_v \ne n_v \to \neg (C(m_l)\land C(n_l)) ) }[/math]

For the derivation, start with,

[math]\displaystyle{ V(M) = V(N) }[/math]

The value condition gives,

[math]\displaystyle{ (\forall m_v \forall m_l ((m_v, m_l) \in M \land C(m_l) \to v = V(M)) \land (\forall n_v \forall n_l ((n_v, k) \in N \land C(n_l)) \to n_v = V(N)) \land V(M) = V(N) }[/math]

[math]\displaystyle{ \forall m_v \forall m_l \forall n_v \forall n_l (((m_v, m_l) \in M \land C(m_l)) \to m_v = V(M)) \land (((n_v, n_l) \in N \land C(n_l)) \to n_v = V(N)) \land V(M) = V(N) }[/math]

[math]\displaystyle{ \forall m_v \forall m_l \forall n_v \forall n_l ((m_v, m_l) \in M \land (n_v, n_l) \in N) \to ( C(j)\land C(k) \to v = u) }[/math]

[math]\displaystyle{ \forall m_v \forall m_l \forall n_v \forall n_l ((m_v, m_l) \in M \land (n_v, n_l) \in N) \to (m_v \ne n_v \to \neg (C(m_l)\land C(n_l)) ) }[/math]

Narrowing by conjunction

If any base condition is false, all the conditions obtained from it are false.

This comes from the definition of the Condition function,

[math]\displaystyle{ C(l) = ({\bigwedge_{(r, z, u) \in l} z = u})) }[/math]

The base condition for (r, z, u) is,

[math]\displaystyle{ C(\{(r, z, u)\} = (z = u) }[/math]

So if this is false [math]\displaystyle{ C(l) }[/math] is false.

Narrowing by crossed conditions

If a dependent condition list has two different base conditions from the same value set it must be false.

To derive this, start with the exclusion rule which is,

[math]\displaystyle{ \forall v_1 \forall l_1 \forall v_2 \forall l_2 ((v_1, l_1) \in K \land (v_2, l_2) \in K \land (v_1, l_1) \ne (v_2, l_2)) \implies \neg (C(l_1) \land C(l_2)) }[/math]

Then for any set of dependent conditions l,

[math]\displaystyle{ ((K, x, v_1) \in l \ \land (K, x, v_2) \in l \land v_1 \ne v_2 }[/math]

[math]\displaystyle{ \implies (v_1, \{(K, x, v_1)\}) \in K \land (v_2, \{(K, x, v_2)\}) \in K \land (v_1, l_1) \ne (v_2, l_2)) }[/math]

[math]\displaystyle{ \implies \neg (C(\{(K, x, v_1)\}) \land C(\{(K, x, v_2)\})) }[/math]

[math]\displaystyle{ \implies \neg C(l) }[/math]

So if a dependent condition list is based on two conditions from the same value set, the condition value of that dependent condition list is false.

Narrowing by exclusion of dependent values

Each value set puts a constraint on the base value set from which it is constructed. If a base values set includes values that are not present as dependent values in the value set, the conditions for these values must be false.

To derive this, start with the complete set rule,

[math]\displaystyle{ \exists v \exists \ l (v, l) \in K \to C(l) }[/math]

The condition function is,

[math]\displaystyle{ C(l) = ({\bigwedge_{(r, z, u) \in l} z = u})) }[/math]

A particular dependent condition may be chosen, as being implied by the whole condition,

[math]\displaystyle{ \forall L \ C(l) \to (L, z, u) \in l \to z = u }[/math]

So

[math]\displaystyle{ \forall L \exists v \exists l \ (v, l) \in K \to C(l) \to (L, z, u) \in l \to z = u }[/math]

Here [math]\displaystyle{ z = V(L) }[/math]. The expression may be rearranged to define the set of values that [math]\displaystyle{ V(L) }[/math] might take,

[math]\displaystyle{ E(K, L) = \{w : (v, l) \in K \land C(l) \land (L, z, w) \in l \} }[/math]

and so,

[math]\displaystyle{ V(L) \in E(K, L) }[/math]

Then using the exclusion rule,

[math]\displaystyle{ V(M) \in s \iff (\forall v \forall l ((v, l) \in M \land v \not \in s) \to \neg C(l)) }[/math]

gives,

[math]\displaystyle{ (\forall K \forall L \forall v \forall l ((v, l) \in L \land v \not \in E(K, L)) \to \neg C(l)) }[/math]

This is the narrowing exclusion rule. [math]\displaystyle{ E(K, L) }[/math] is the set of values in the base value L set which are represented in the value set K. Conditions for other values must be false.

Probabilistic value sets

The value set records the dependent conditions that the condition function may be applied to in order to deduce the truth of the proposition that the value set has a particular value. The same structure may be used to give the probability of a value set being equal to a particular value. The condition function is,

[math]\displaystyle{ C(l) = ({\bigwedge_{(r, z, u) \in l} z = u})) }[/math]

The probability function is,

[math]\displaystyle{ P(l) = ({\prod_{(r, z, u) \in l} P(z = u)})) }[/math]

This is the probability of each base case holding the particular value, if the events are independent.

The probability function is defined by 3 axioms,

1. Each pair [math]\displaystyle{ (v, l) }[/math] means that the probability of the value set [math]\displaystyle{ V(K) }[/math] is v is the probability function applied to the list, [math]\displaystyle{ P(l) }[/math].
2. The sum of the probabilities over the whole value set is 1.
3. The probability of any two pairs in the value set is zero.

The probability function gives probabilities for results based on initial probabilities given by Boolean inductive inference.

Formally,

Name	Definition
Probability function	[math]\displaystyle{ P(l) = ({\prod_{(r, z, u) \in l} P(z = u)})) }[/math]
Value condition	[math]\displaystyle{ \forall v P(v = V(K)) = \sum_{(v, l) \in K} P(l) }[/math]
Complete set	[math]\displaystyle{ \sum_{(v, l) \in K} P(l) = 1 }[/math]
Allowed values	[math]\displaystyle{ \sum_{(v, l) \in K \land v \in \operatorname{gset}(V(K))} P(l) = 1 }[/math]
Exclusion	[math]\displaystyle{ \forall v_1 \forall l_1 \forall v_2 \forall l_2 ((v_1, l_1) \in K \land (v_2, l_2) \in K \land (v_1, l_1) \ne (v_2, l_2)) \to P(C(l_1) \land C(l_2)) = 0 }[/math]

Probabilities for each value in a value set may be calculated from probabilities in base value sets using the probability function and the value condition. Base value sets are either for a single value, or multiple value value set.

Probability for a single value

The value set to represent a single value is,

[math]\displaystyle{ k = V(\{(k, \{\})\}) }[/math]

The complete set rule is,

[math]\displaystyle{ \sum_{(v, l) \in K} P(l) }[/math]

[math]\displaystyle{ = \sum_{(v, l) \in \{(k, \{\})\}} P(l) }[/math]

[math]\displaystyle{ = P(\{\}) }[/math]

[math]\displaystyle{ = 1 }[/math]

Which is consistent with the axiom.

Probabilities for multiple values

The value set to represent multiple values is,

[math]\displaystyle{ \forall x \forall X (\operatorname{let} x \in X \operatorname{in} x) = V(\{(w, \{(\_, x, w)\}) : w \in X\}) }[/math]

The probability is given by the allowed values rule,

[math]\displaystyle{ \sum_{(v, l) \in K \land v \in \operatorname{gset}(V(K))} P(l) = 1 }[/math]

which simplifies to,

[math]\displaystyle{ \sum_{v \in \operatorname{gset}(V(K))} P(x = v) = 1 }[/math]

If prior estimates of probabilities for values are given then they will be proportional to the posterior probabilities, if the value is in the value set.

[math]\displaystyle{ \forall v \in \operatorname{gset}(V(K)), P(x = v) = w * P_i(x = v) }[/math]

If the value is not in the value set the probabilities will be zero,

[math]\displaystyle{ \forall v \not \in \operatorname{gset}(V(K)), P(x = v) = 0 }[/math]

So,

[math]\displaystyle{ \sum_{v \in \operatorname{gset}(V(K))} w * P_i(x = v) = 1 }[/math]

[math]\displaystyle{ w = \frac{1}{\sum_{v \in \operatorname{gset}(V(K))} P_i(x = v)} }[/math]

[math]\displaystyle{ \forall v \in \operatorname{gset}(V(K)), P(x = v) = \frac{P_i(x = v)}{\sum_{v \in \operatorname{gset}(V(K))} P_i(x = v)} }[/math]

[math]\displaystyle{ \forall v \not \in \operatorname{gset}(V(K)), P(x = v) = 0 }[/math]

If the prior probabilities are all the same the probabilities are,

[math]\displaystyle{ \forall v \in \operatorname{gset}(V(K)), P(x = v) = \frac{1}{|\operatorname{gset}(V(K))|} }[/math]

Probabilities of general value sets

A general value set is created out of the application of base value sets. The value condition rule and the probability function may be combined to give,

[math]\displaystyle{ \forall v P(v = V(K)) = \sum_{(v, l) \in K \land v \in \operatorname{gset}(V(K))} ({\prod_{(r, z, u) \in l} P(z = u)})) }[/math]

Accessing the value set

Narrowing allows the elimination of values that do not satisfy a variable's constraints. Considered as the basis for an algorithm for solving equations, this narrowing gives a set of values consistent with the constraints on a variable. However in mathematics there is no way to access this set of values.

If [math]\displaystyle{ E(x) }[/math] is an expression constraining a variable x then the set of values that the variable may take is,

[math]\displaystyle{ \{z : E(z)\} }[/math]

Define the gset of x to be the set of values that satisfy the constraints on x. Consider defining gset as,

[math]\displaystyle{ \operatorname{gset}(x) = \{z : E(z)\} }[/math]

This definition depends on knowing the expression E, which is the condition giving all the constraints on x. Within mathematics E may not be obtained from x. So there is no mathematical function that may be applied to a variable to request the set of values. So may the gset function be added to mathematics?

Meta math definition

A meta-mathematical definition of gset may be possible. Imagine that what we know of as mathematics is actually implemented by a meta function called math. math takes an abstract syntax tree and gives meaning to the variables and mathematical structures and adds existential quantifiers for variables not explicitly quantified.

math would be an expression in a meta mathematical environment with its own variables. To distinguish these meta-variables from math variables represent them by capital letters and the mathematical variables by lower case letters.

Now suppose there is an extended implementation of mathematics implemented by the xmath function, defined as,

[math]\displaystyle{ \operatorname{xmath}[E] = \forall M, \operatorname{let} T[M] = \operatorname{math}[E] \operatorname{in} T[\_] }[/math]

Using xmath, gset may be defined by,

[math]\displaystyle{ \forall x \#u, \exists N, \operatorname{gset}(x) = \operatorname{let} M[u] = x \operatorname{in} \{z : z = N[u] \land T[N]\} }[/math]

Here again the notation,

[math]\displaystyle{ \forall x \#u }[/math]

is used to mean quantification over variables x where x refers to the value, and u refers to the unique identity of the variable.

Example

For example take the constraint expression [math]\displaystyle{ x^2 = 4 }[/math]. Then,

[math]\displaystyle{ x^2 = 4 }[/math]

[math]\displaystyle{ \land s = \operatorname{gset}(x) }[/math]

[math]\displaystyle{ \land (\forall x \#u, \exists N \operatorname{gset}(x) = \operatorname{let} M[u] = x \operatorname{in} \{z : z = N[u] \land T[N]\}) }[/math]

Then the xmath expression is,

[math]\displaystyle{ \forall M, \operatorname{let} T[M] = }[/math]

[math]\displaystyle{ \exists x, \exists s, (x^2 = 4 }[/math]

[math]\displaystyle{ \land s = \operatorname{gset}(x) }[/math]

[math]\displaystyle{ \land (\forall x \#u, \exists N, \operatorname{gset}(x) = \operatorname{let} M[u] = x \operatorname{in} \{z : z = N[u] \land T[N]\}) }[/math]

[math]\displaystyle{ \operatorname{in} T[\_] }[/math]

Then where u is the unique identity of the variable x, represented here as the number 1 (for the first variable used in a call to gset),

[math]\displaystyle{ M[1] = x \land s = \{z : z = N[1] \land T[N]\} }[/math]

Here [math]\displaystyle{ T[N] }[/math] invokes T with M as N.

[math]\displaystyle{ s = \{z : z = N[1] \land x^2 = 4 \land x = N[1]\} }[/math]

[math]\displaystyle{ s = \{z : z^2 = 4\} }[/math]

See also

• Functional programming
  • Lazy evaluation
  • Polymorphic type system
  • Type inference
  • Higher-order function
  • Haskell
• Lambda calculus
  • Deductive lambda calculus
  • Let expression
• Logic programming
  • Resolution (logic)
  • Constraint logic programming
  • constraints
  • ECLiPSe
• Mathematics
  • Function (mathematics)
  • Algebra
  • Disjunction
• Relational programming