Misplaced Pages

Narrowing of algebraic value sets: Difference between revisions

Article snapshot taken from[REDACTED] with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Browse history interactively← Previous editContent deleted Content addedVisualWikitext
Revision as of 08:18, 5 May 2014 editThepigdog (talk | contribs)Extended confirmed users5,174 edits Boolean inductive inference← Previous edit Latest revision as of 08:08, 27 February 2020 edit undoReyk (talk | contribs)Autopatrolled, Extended confirmed users, Pending changes reviewers, Rollbackers33,854 edits reduce verbosity per Misplaced Pages:Manual_of_Style/Words_to_watch#Editorializing and MOS:NOTE 
(87 intermediate revisions by 8 users not shown)
Line 10: Line 10:
|pages=617–31 |pages=617–31
|chapter=Constraint Solving by Narrowing in Combined Algebraic Domains |chapter=Constraint Solving by Narrowing in Combined Algebraic Domains
}}</ref> }}</ref><ref>
<ref>
{{cite book {{cite book
|first1=Puri |first1=Puri
Line 19: Line 18:
|title=Proc. of the International Symposium on Logic Programming (ILPS'97) |title=Proc. of the International Symposium on Logic Programming (ILPS'97)
|year=1997 |year=1997
|publisher=The MIT Press, |publisher=The MIT Press
|pages=53–67 |pages=53–67
|chapter=A Lazy Narrowing Calculus for Functional Logic Programming with Algebraic Polymorphic Types. |chapter=A Lazy Narrowing Calculus for Functional Logic Programming with Algebraic Polymorphic Types.
Line 29: Line 28:
{{cite book {{cite book
| first1=Kim | first1=Kim
| last1=Marriot | last1=Marriott
| first2=Peter J. | first2=Peter J.
| last2=Stuckey | last2=Stuckey
Line 38: Line 37:
</ref> in ], but without the logic processing basis. </ref> in ], but without the logic processing basis.


] is a natural extension of value sets to ]. The value set construct holds the information required to calculate probabilities of calculated values based on probabilities of initial values. ] is a natural extension of value sets to ]. 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 ]. 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. ] languages based on ] allow this mathematical approach to programming. Functional languages developed by implementing ], and allowing functions to be passed as parameters.

Lazy evaluation is an essential feature of modern ] languages such as ]. Haskell is the latest in a series of languages based on ] and ]s. These languages provide rich functionality through lazy evaluation, and a ] using ]. Functional programming languages also naturally support ]s.

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

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 == == Introduction ==
Line 46: Line 59:
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. 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 ] "or"" has inverses that allow two values. In natural language "or" represents alternate possibilities. Some Boolean operations, in particular do not have inverses that may be defined as functions. In particular the ] "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.
] in logic provides a mechanism for dealing with the problems with Boolean operators. It is the basis for the ] languages. However it is a specific solution, related to logic. It is not a general solution to the problem of inverses of functions that are not 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 ]. The value sets tag each value in the value set with the world to which it belongs.
] extends logic programming, by supporting ]. Constraint logic programming languages such as ] provide the ability to solve complex logic problems. However ECLiPSe is not ].


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.
Lazy evaluation is an essential feature of modern ] languages such as ]. Haskell is the latest in a series of languages based on ] and ]s. These languages provide rich functionality through lazy evaluation, and a ] using ]. Functional programming languages also naturally support ]s.


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.
Logic programming languages lack the flexibility and power of functional languages, and are not readily extended in the same ways that functional programming languages have, because of their dependence on resolution.


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.
== Multiple values ==

== 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>x^2 = 4</math>
which implies,
:<math>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>x = \pm 2 </math>

Naively then,

:<math>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> V(\{2 :: x_1, -2 :: x_2\}) </math>

It is container ''V'' which has a set of tag, value pairs,
* <math> 2 :: x_1 </math>
* <math> -2 :: x_2 </math>

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

The solution of the equation,
:<math>x^2 = 4</math>

is,
: <math> 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> \{x_1, x_2\} </math> is a world set as either x = 2 (in world <math>x_1</math>) or x= −2 (in world <math>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>x_1</math> and <math>x_2</math> are true at the same time.
:<math>(x = 2 \land x = -2) = \text{false} </math>

=== Application of functions ===

The rule for the application of functions to value sets is,
:<math>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> x + x = V(\{2 :: x_1, -2 :: x_2\}) + V(\{2 :: x_1, -2 :: x_2\}) </math>

is,
: <math> = 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> = 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> x_1 \cap x_1 = x_1 </math>
: <math> 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> x_1 \cap x_2 = \{\} </math>
: <math> x_2 \cap x_1 = \{\} </math>

So,
: <math> = V(\{-4 :: x_1, 0 :: \{\}, 0 :: \{\}, 4 :: x_2 \}) </math>

The empty worlds rule allows tagged values from empty worlds to be dropped
:<math> V(K) = V(\{(v, l) : (v, l) \in K \land l \ne \{\} \} </math>

giving,
: <math> = V(\{-4 :: x_1, 4 :: x_2 \}) </math>

Giving the result that <math>x + x</math> is either −4 or 4, as expected.

=== Application to Booleans ===

: <math> a \land b </math>

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

: <math> a \lor b </math>

Allows multiple values for ''a'' and ''b''. If ''a'' is,
: <math> a = V(\{\operatorname{false} :: a_1, \operatorname{true} :: a_2 \}) </math>

then for ''b''
: <math> 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> x = 2 \lor x = -2 </math>

gives,
: <math> x = V(\{\_ :: a_1, 2 :: a_2 \}) </math>
and
: <math> x = V(\{-2 :: a_1, \_ :: a_2, -2 :: a_2 \}) </math>

unifying these two value sets gives,
: <math> x = V(\{-2 :: a_1, 2 :: a_2\}) </math>

The pair <math> -2 :: a_2 </math> is dropped because of the "assert equal" rule,
:<math>\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> -2 :: a_2 </math> did not match with <math> 2 :: a_2 </math>.

=== Dependent worlds ===

Consider the problem,
: <math> X = V(\{1 :: x_1, 3 :: x_2, 4 :: x_3\}) </math>
: <math> Y = V(\{8 :: y_1, 9 :: y_2\}) </math>
: <math> X * Y < 25 </math>
: <math> X + Y > 10 </math>

Firstly calculate the value set for <math> X * Y < 25 </math>,
: <math> 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\}) < 25 </math>
: <math> V(\{8<25 :: x_1 \cap y_1, 24<25 :: x_2 \cap y_1, 32<25 :: x_3 \cap y_1, 9<25 :: x_1 \cap y_2, 27<25 :: x_2 \cap y_2, 36<25 :: x_3 \cap y_2\}) < 25 </math>
: <math> 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> 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> x_3 \cap y_1 </math>
: <math> x_2 \cap y_2 </math>
: <math> 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>X_3</math> is not represented in this value, and so must be empty. The value set for <math>X</math> is now smaller,
: <math> X = V(\{1 :: x_1, 3 :: x_2\}) </math>

The second condition is now simpler, because of the smaller value set.
: <math> X + Y > 10 </math>

Then the value sets are,
: <math> X = V(\{1 :: x_1, 3 :: x_2\}) </math>
: <math> Y = V(\{8 :: y_1, 9 :: y_2\}) </math>

And the calculation is,
: <math> 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\}) > 10 </math>

But <math> x_2 \cap y_2 </math> is empty. So,
: <math> V(\{9>10 :: x_1 \cap y_1, 11>10 :: x_2 \cap y_1, 10>10 :: x_1 \cap y_2\}) </math>

So <math> x_1 \cap y_1 </math> and <math> x_1 \cap y_2 </math> are empty,
: <math> V(\{11>10 :: x_2 \cap y_1\}) </math>

Now <math>X_1</math> and <math>Y_2</math> are not represented, and are removed as dependent worlds. So,
: <math> X = V(\{3 :: x_2\}) = 3 </math>
: <math> 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>\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>\text{BottleshopWithBeer}(V(\{\text{South Melbourne}::b_1, \text{St Kilda}::b_2, \text{Carlton}::b_3, \text{Docklands}::b_4\}))</math>

Whiskey,
: <math>\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>\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>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>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>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>x = V(\{\text{Essendon}::w_1, \text{South Melbourne}::w_2\})</math>

Which gives 6 combinations. The matching one is,
: <math>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>x = V(\{\text{Essendon}::w_1, \text{South Melbourne}::w_2\})</math>

Then we need to unify this with,
: <math>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>x = V(\{\text{South Melbourne}::b_1 \cap w_2\})</math>

Finally we need to unify with pizza.
: <math>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>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 ].

== 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 ] may be used to represent a value that is a member of a set, 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 ] may be used to represent a value that is a member of a set,
Line 65: Line 292:
Under function application, of one let expression to another, Under function application, of one let expression to another,
:<math> (\operatorname{let} x \in X \operatorname{in} x)\ (\operatorname{let} y \in Y \operatorname{in} y) </math> :<math> (\operatorname{let} x \in X \operatorname{in} x)\ (\operatorname{let} y \in Y \operatorname{in} y) </math>
:<math> = \operatorname{let} x \in X \and y \in Y \operatorname{in} x\ y </math> :<math> = \operatorname{let} x \in X \land y \in Y \operatorname{in} x\ y </math>
:<math> = \operatorname{let} (x, y) \in X \times Y \operatorname{in} x\ y </math> :<math> = \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. 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> (\operatorname{let} x \in X \operatorname{in} x)\ (\operatorname{let} x \in X \operatorname{in} x) </math> :<math> (\operatorname{let} x \in X \operatorname{in} x)\ (\operatorname{let} x \in X \operatorname{in} x) </math>
:<math> = \operatorname{let} x \in X \operatorname{in} x\ x </math> :<math> = \operatorname{let} x \in X \operatorname{in} x\ x </math>
Line 78: Line 305:
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". 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".


== Value sets == == 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. 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.
Line 96: Line 323:
| Condition function || <math>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> | Condition function || <math>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>\forall v \forall l ((v, l) \in K \and C(l) \to v = V(K)</math> | Value condition || <math>\forall v \forall l ((v, l) \in K \land C(l) \to v = V(K)</math>
|- |-
| Complete set || <math>\exists v \exists l (v, l) \in K \and C(l) </math> | Complete set || <math>\exists v \exists l (v, l) \in K \land C(l) </math>
|- |-
| Exclusion || <math>\forall v_1 \forall l_1 \forall v_2 \forall l_2 ((v_1, l_1) \in K \and (v_2, l_2) \in K \and (v_1, l_1) \ne (v_2, l_2)) \to \neg (C(l_1) \and C(l_2)) </math> | Exclusion || <math>\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>
|} |}


Line 106: Line 333:


Using the value condition and complete set axioms, Using the value condition and complete set axioms,
:<math>\exists v \exists l (v, l) \in K \and C(l) \and v = V(K) </math> :<math>\exists v \exists l (v, l) \in K \land C(l) \land v = V(K) </math>


As a let expression this becomes, As a let expression this becomes,
:<math> V(K) = \operatorname{let} (v, l) \in K \and C(l) \operatorname{in} v </math> :<math> V(K) = \operatorname{let} (v, l) \in K \land C(l) \operatorname{in} v </math>


=== Single value === === Single value ===
Line 118: Line 345:
The derivation is, The derivation is,
:<math> V(\{(k, \{\})\}) </math> :<math> V(\{(k, \{\})\}) </math>
:<math> = \operatorname{let} (v, l) \in \{(k, \{\})\} \and C(l) \operatorname{in} v </math> :<math> = \operatorname{let} (v, l) \in \{(k, \{\})\} \land C(l) \operatorname{in} v </math>
:<math> = \operatorname{let} v = k \and C(\{\}) \operatorname{in} v </math> :<math> = \operatorname{let} v = k \land C(\{\}) \operatorname{in} v </math>
:<math> = \operatorname{let} v = k \operatorname{in} v </math> :<math> = \operatorname{let} v = k \operatorname{in} v </math>
:<math> = k </math> :<math> = k </math>
Line 130: Line 357:
This rather strange definition adds the value set in as part of the dependent condition. This is used in ]. This rather strange definition adds the value set in as part of the dependent condition. This is used in ].


The value of the expression is
Note also that,
:<math> x = V(R) </math> :<math> x = V(R) </math>.


is the value of the expression. 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. 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, If the addition of ''R'' to the dependent condition is ignored, the expression takes on a simpler and more understandable form,


:<math> \forall x \forall X (\operatorname{let} x \in X \operatorname{in} x) = V(\{(w, \{(\_, x, w)\}) : w \in X\}) </math> :<math> \forall x \forall X (\operatorname{let} x \in X \operatorname{in} x) = V(\{(w, \{(\_, x, w)\}) : w \in X\}) </math>
Line 141: Line 368:
The derivation is, The derivation is,
:<math> V(\{(w, \{(r, x, w) : w \in X\}) </math> :<math> V(\{(w, \{(r, x, w) : w \in X\}) </math>
:<math> = \operatorname{let} (v, l) \in \{(w, \{(r, x, w)\}) : w \in X\} \and C(l) \operatorname{in} v </math> :<math> = \operatorname{let} (v, l) \in \{(w, \{(r, x, w)\}) : w \in X\} \land C(l) \operatorname{in} v </math>
:<math> = \operatorname{let} v \in X \and ({\bigwedge_{(r, z, u) \in \{(\_, x, v)\}} z = u}) \operatorname{in} v </math> :<math> = \operatorname{let} v \in X \land ({\bigwedge_{(r, z, u) \in \{(\_, x, v)\}} z = u}) \operatorname{in} v </math>
:<math> = \operatorname{let} v \in X \and (\forall r \forall z \forall u (r, z, u) \in \{(\_, x, v)\} \to z = u) \operatorname{in} v </math> :<math> = \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> = \operatorname{let} v \in X \and x = v \operatorname{in} v </math> :<math> = \operatorname{let} v \in X \land x = v \operatorname{in} v </math>
:<math> = \operatorname{let} x \in X \operatorname{in} x </math> :<math> = \operatorname{let} x \in X \operatorname{in} x </math>


Line 150: Line 377:


Function application of value sets is given by, Function application of value sets is given by,
:<math>V(M)\ V(N) = V(\{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \and (n_v, n_l) \in N\}) </math> :<math>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, Derivation,
:<math>V(M)\ V(N) </math> :<math>V(M)\ V(N) </math>
:<math> = \operatorname{let} (m_v, m_l) \in M \and C(m_l) \operatorname{in} m_v)\ (\operatorname{let} (n_v, n_l) \in N \and C(n_l) \operatorname{in} n_v) </math> :<math> = \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> = \operatorname{let} (m_v, m_l) \in M \and (n_v, n_l) \in N \and C(n_l) \and C(n_l) \operatorname{in} m_v\ n_v) </math> :<math> = \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, Then using,
:<math>C(m_l) \and C(n_l)</math> :<math>C(m_l) \land C(n_l)</math>
:<math> = ({\bigwedge_{(z, u) \in m_l} z = u}) \and ({\bigwedge_{(z, u) \in n_l} z = u})</math> :<math> = ({\bigwedge_{(z, u) \in m_l} z = u}) \land ({\bigwedge_{(z, u) \in n_l} z = u})</math>
:<math> = ({\bigwedge_{(z, u) \in m_l \cup n_l} z = u}) </math> :<math> = ({\bigwedge_{(z, u) \in m_l \cup n_l} z = u}) </math>
:<math> = C(m_l \cup n_l)</math> :<math> = C(m_l \cup n_l)</math>


get, get,
:<math> = \operatorname{let} (m_v, m_l) \in M \and (n_v, n_l) \in N \and C(n_l \cup n_l) \operatorname{in} m_v\ n_v) </math> :<math> = \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> = \operatorname{let} (v, l) \in \{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \and (n_v, n_l) \in N\} \and C(l) \operatorname{in} v </math> :<math> = \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> = V(\{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \and (n_v, n_l) \in N\}) </math> :<math> = 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 === === Exclusion ===


The exclusion is a rule that determines when conditions must be false, The exclusion is a rule that determines when conditions must be false,
:<math> V(M) \in s \iff (\forall v \forall l ((v, l) \in M \and v \not \in s) \to \neg C(l)) </math> :<math> 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, This may be derived from,
:<math> V(M) \in s </math> :<math> V(M) \in s </math>
:<math> \to \forall v \forall l ((v, l) \in M \and C(l)) \to (v = V \and V(M) \in s)</math> :<math> \to \forall v \forall l ((v, l) \in M \land C(l)) \to (v = V \land V(M) \in s)</math>
:<math> \to \forall v \forall l ((v, l) \in M \and C(l)) \to v \in S</math> :<math> \to \forall v \forall l ((v, l) \in M \land C(l)) \to v \in S</math>
:<math> \to \forall v \forall l ((v, l) \in M \and v \not \in S) \to \neg C(l) </math> :<math> \to \forall v \forall l ((v, l) \in M \land v \not \in S) \to \neg C(l) </math>


=== Simplification === === Simplification ===


The simplification rule allows values whose condition is false to be dropped. The simplification rule allows values whose condition is false to be dropped.
:<math> V(K) = V(\{(v, l) : (v, l) \in K \and C(l)\} </math> :<math> V(K) = V(\{(v, l) : (v, l) \in K \land C(l)\} </math>


Derivation Derivation
:<math> V(\{(v, l) : (v, l) \in K \and C(l)\}) </math> :<math> V(\{(v, l) : (v, l) \in K \land C(l)\}) </math>
:<math> = \operatorname{let} (v, l) \in \{(v, l) : (v, l) \in K \and C(l)\} \and C(l) \operatorname{in} v </math> :<math> = \operatorname{let} (v, l) \in \{(v, l) : (v, l) \in K \land C(l)\} \land C(l) \operatorname{in} v </math>
:<math> = \operatorname{let} (v, l) \in K \and C(l) \and C(l) \operatorname{in} v </math> :<math> = \operatorname{let} (v, l) \in K \land C(l) \land C(l) \operatorname{in} v </math>
:<math> = \operatorname{let} (v, l) \in K \and C(l) \operatorname{in} v </math> :<math> = \operatorname{let} (v, l) \in K \land C(l) \operatorname{in} v </math>
:<math> = V(K) </math> :<math> = V(K) </math>


Line 198: Line 425:
! Name !! Rule ! Name !! Rule
|- |-
| Value function || <math> V(K) = \operatorname{let} (v, l) \in K \and C(l) \operatorname{in} v </math> | Value function || <math> V(K) = \operatorname{let} (v, l) \in K \land C(l) \operatorname{in} v </math>
|- |-
| Single value || <math> k = V(\{(k, \{\})\})</math> | Single value || <math> k = V(\{(k, \{\})\})</math>
Line 204: Line 431:
| Set element|| <math> \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> | Set element|| <math> \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>V(M)\ V(N) = V(\{(m_v\ n_v, m_l \cup n_l) : (m_v, m_l) \in M \and (n_v, n_l) \in N\})</math> | Function application || <math>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> V(M) \in s \iff (\forall v \forall l ((v, l) \in M \and v \not \in s) \to \neg C(l)) </math> | Exclusion || <math> 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> V(K) = V(\{(v, l) : (v, l) \in K \and C(l)\}) </math> | Simplification || <math> V(K) = V(\{(v, l) : (v, l) \in K \land C(l)\}) </math>
|- |-
| Assert equal || <math>V(M) = V(N) \to (\forall v \forall l ((v, l) \in N \and v \not \in S(M)) \to \neg C(l)) </math> | Assert equal || <math>V(M) = V(N) \to (\forall v \forall l ((v, l) \in N \land v \not \in S(M)) \to \neg C(l)) </math>
|} |}


Line 222: Line 449:
:<math>\forall x \#u </math> :<math>\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 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 ] definition would be, Using this notation the ] definition would be,
Line 237: Line 464:


Assertion that two value sets are equal gives the narrowing rule, Assertion that two value sets are equal gives the narrowing rule,
<math>\forall m_v \forall m_l \forall n_v \forall n_l ((m_v, m_l) \in M \and (n_v, n_l) \in N) \to (m_v \ne n_v \to \neg (C(m_l)\and C(n_l)) ) </math> :<math>\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, For the derivation, start with,
Line 244: Line 471:
The value condition gives, The value condition gives,


<math>(\forall m_v \forall m_l ((m_v, m_l) \in M \and C(m_l) \to v = V(M)) \and (\forall n_v \forall n_l ((n_v, k) \in N \and C(n_l)) \to n_v = V(N)) \and V(M) = V(N) </math> :<math>(\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>\forall m_v \forall m_l \forall n_v \forall n_l (((m_v, m_l) \in M \and C(m_l)) \to m_v = V(M)) \and (((n_v, n_l) \in N \and C(n_l)) \to n_v = V(N)) \and V(M) = V(N) </math> :<math>\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>\forall m_v \forall m_l \forall n_v \forall n_l ((m_v, m_l) \in M \and (n_v, n_l) \in N) \to ( C(j)\and C(k) \to v = u) </math> :<math>\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>\forall m_v \forall m_l \forall n_v \forall n_l ((m_v, m_l) \in M \and (n_v, n_l) \in N) \to (m_v \ne n_v \to \neg (C(m_l)\and C(n_l)) ) </math> :<math>\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 === === Narrowing by conjunction ===
Line 268: Line 495:
If a dependent condition list has two different base conditions from the same value set it must be false. 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 is, To derive this, start with the exclusion rule which is,
:<math>\forall v_1 \forall l_1 \forall v_2 \forall l_2 ((v_1, l_1) \in K \and (v_2, l_2) \in K \and (v_1, l_1) \ne (v_2, l_2)) \implies \neg (C(l_1) \and C(l_2)) </math> :<math>\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'', Then for any set of dependent conditions ''l'',
:<math> ((K, x, v_1) \in l \ \and (K, x, v_2) \in l \and v_1 \ne v_2 </math> :<math> ((K, x, v_1) \in l \ \land (K, x, v_2) \in l \land v_1 \ne v_2 </math>
:<math> \implies (v_1, \{(K, x, v_1)\}) \in K \and (v_2, \{(K, x, v_2)\}) \in K \and (v_1, l_1) \ne (v_2, l_2))</math> :<math> \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> \implies \neg (C(\{(K, x, v_1)\}) \and C(\{(K, x, v_2)\}))</math> :<math> \implies \neg (C(\{(K, x, v_1)\}) \land C(\{(K, x, v_2)\}))</math>
:<math> \implies \neg C(l)</math> :<math> \implies \neg C(l)</math>


Line 296: Line 523:


Here <math> z = V(L) </math>. The expression may be rearranged to define the set of values that <math> V(L) </math> might take, Here <math> z = V(L) </math>. The expression may be rearranged to define the set of values that <math> V(L) </math> might take,
:<math>E(K, L) = \{w : (v, l) \in K \and C(l) \and (L, z, w) \in l \} </math> :<math>E(K, L) = \{w : (v, l) \in K \land C(l) \land (L, z, w) \in l \} </math>


and so, and so,
Line 302: Line 529:


Then using the exclusion rule, Then using the exclusion rule,
:<math> V(M) \in s \iff (\forall v \forall l ((v, l) \in M \and v \not \in s) \to \neg C(l)) </math> :<math> V(M) \in s \iff (\forall v \forall l ((v, l) \in M \land v \not \in s) \to \neg C(l)) </math>


gives,
Gives,
:<math> (\forall K \forall L \forall v \forall l ((v, l) \in L \and v \not \in E(K, L)) \to \neg C(l)) </math> :<math> (\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>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. This is the narrowing exclusion rule. <math>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.

== Relational evaluation ==

An assertion is an expression that is deemed true. So an expression like,
:<math>x = 5</math>

is a relationship between the values ''x'', ''5'', and ''true''. Because ''x'' is unknown, the relationship defines the value of ''x'' as ''5''. For another example,
:<math>y + 3 = 5</math>

This may be seen as two relationships; a relationship between ''y'', ''3'' and another value which we may call ''x'', and a relationship between ''x'', ''5'', and true. The second relationship tells us that ''x'' is ''5'', so the first relationship between ''y'', ''3'' and ''5'', which gives ''y'' is ''2''.

''y'' is ''2'' is used to represent that ''y'' has already been found to have the value ''2'', but <math>y = 2</math> is a relationship, that implies that ''y'' is ''2''.

A relationship has a function, and one or more inverse functions. This set of functions may be used to calculate the unknown value from the known values. What values may be calculated from given inputs depends on the relation.

If the value of a particular value is required, or requested, then a relationship including the variable may be found. That relationship may have more unknowns. These unknowns may then be requested, chaining back eventually to known values.

There are limitations to this strategy. If a variable for a function is given twice, perhaps a recursive function is defined. But in general where a variable appears multiple times, the strategy fails, and the equation may need to be solved by other means.

== Notation ==

Moving away from the technical details of the derivations above, value sets lend themselves to some simple intuitions and rules when applied as a method for evaluating logical problems.

Consider,
: <math> x^2 = 4 </math>

This is a relationship between ''x'', ''2'' and ''4''. If ''x'' is requested then the relationship defines the values for ''x''. However in this case there are two values. By using a value set, these two values may be handled as one value. This is written as,
: <math> x = V(\{(-2, x_1), (2, x_2)\}) </math>

<math>x_1</math> and <math>x_2</math> are base conditions. They are written this way instead of as <math>x = 2</math> and <math>x = -2</math>, because there details do not matter. Only the identity, and that they belong to the variable ''x'' matters. So ''x'' is sub-scripted with unique indexes to represent this.

Also for readability the operator ''::'' is introduced to represent the condition, value pair. Define,
: <math> (v, l) = v :: l </math>

The list is represented as a conjunction of base conditions
then,
: <math> x = V(\{-2 :: x_1, -2 :: x_2\}) </math>

Consider now,
: <math> x + x = V(\{2 :: x_1, -2 :: x_2\}) + V(\{2 :: x_1, -2 :: x_2\}) </math>

] may then be interpreted as,
: <math> = V(\{-2+-2 :: x_1 \and x_1, -2+2 :: x_1 \and x_2, 2+-2 :: x_2 \and x_1, 2+2 :: x_2\}) </math>
: <math> = V(\{-4 :: x_1, 0 :: \operatorname{false}, 0 :: \operatorname{false}, 4 :: x_2 \}) </math>

Here the condition list is represented by the base conditions combined with the "and" operator <math>\and</math>.

Elements of the value set where the condition is false may be dropped using ] giving,
: <math> = V(\{-4 :: x_1, 4 :: x_2 \}) </math>

=== Application to Booleans ===

: <math> a \and b </math>

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

: <math> a \or b </math>

Allows multiple values for ''a'' and ''b''. If ''a'' is,,
: <math> a = V(\{\operatorname{false} :: a_1, \operatorname{true} :: a_2 \}) </math>

then for ''b''
: <math> 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> x = 2 \or x = -2 </math>

gives,
: <math> x = V(\{\_ :: a_1, 2 :: a_2 \}) </math>
and
: <math> x = V(\{-2 :: a_1, \_ :: a_2, -2 :: a_2 \}) </math>

unifying these two value sets gives,
: <math> x = V(\{-2 :: a_1, 2 :: a_2\}) </math>

The pair <math> -2 :: a_2 </math> was dropped because of the application of ]. Its value did not match with <math> 2 :: a_2 </math>.

''not'' is its own inverse function, and is a 1 to 1 mapping. But the negation of the ''and'' operator will introduce value sets, because of ], turning ''and'' into ''or''.

In ] Boolean values are given special treatment by the ]. Using value sets, this is unnecessary, as where inverses have multiple values, they may be contained within a value set. Relational evaluation treats all evaluation in the same manner and always attempts to evaluate unknown values from known values.

== Evaluation strategy ==

] occurs when value sets are combined. This must be minimized. The product of the sizes of the value sets in the relation, other than the unknown value, gives an estimate of the size of the value set created for the unknown value.

As evaluating any relation may contribute to reduce the size of other value sets by narrowing, the best strategy is to evaluate expressions with the smallest value set size first, as this may lead to narrowing that reduces the size of other vale sets.

The evaluation should proceed on a list of relations for which values have been requested, ordered by the predicted size of the value set to be created. This predicted size will change over time leading to the need for periodic re-ordering. For value sets with one value, this strategy is ]. For values sets with multiple values the strategy minimizes the combinatorial explosion.

Unlike ] there is no ] required for this algorithm. All possible values are contained in value sets, and are considered at the same time. The lack of backtracking may of benefit, or a disadvantage, depending on the problem. The use of value sets forces the consideration of all values, which allows the full benefits of narrowing in reducing the size of value sets. However it forces the solving of the whole problem at once, which if a problem may be naturally divided up, may be a disadvantage.

== Accessing the value set ==

Narrowing allows the elimination of values that do not satisfy a variables 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>E(x)</math> is an expression constraining a variable ''x'' then the set of values that the variable may take is,
:<math>\{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>\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 ] called ''math''. ''math'' takes an ] 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> \operatorname{xmath} = \forall M, \operatorname{let} T = \operatorname{math} \operatorname{in} T </math>

Using ''xmath'', ''gset'' may be defined by,
: <math> \forall x \#u, \exists N, \operatorname{gset}(x) = \operatorname{let} M = x \operatorname{in} \{z : z = N \and T\} </math>

Here ] the notation,
:<math>\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>x^2 = 4</math>. Then,
:<math>x^2 = 4</math>
:<math>\and s = \operatorname{gset}(x)</math>
:<math> \and (\forall x \#u, \exists N \operatorname{gset}(x) = \operatorname{let} M = x \operatorname{in} \{z : z = N \and T\}) </math>

Then the ''xmath'' expression is,
:<math>\forall M, \operatorname{let} T = </math>
::<math>\exists x, \exists s, (x^2 = 4</math>
::<math>\and s = \operatorname{gset}(x)</math>
::<math>\and (\forall x \#u, \exists N, \operatorname{gset}(x) = \operatorname{let} M = x \operatorname{in} \{z : z = N \and T\})</math>
:<math> \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>M = x \and s = \{z : z = N \and T\} </math>

Here <math>T</math> invokes ''T'' with M as N.
:<math>s = \{z : z = N \and x^2 = 4 \and x = N\}</math>
:<math>s = \{z : z^2 = 4\} </math>


== Probabilistic value sets == == Probabilistic value sets ==
Line 479: Line 564:
| Complete set || <math>\sum_{(v, l) \in K} P(l) = 1</math> | Complete set || <math>\sum_{(v, l) \in K} P(l) = 1</math>
|- |-
| Allowed values || <math>\sum_{(v, l) \in K \and v \in \operatorname{gset}(V(K))} P(l) = 1</math> | Allowed values || <math>\sum_{(v, l) \in K \land v \in \operatorname{gset}(V(K))} P(l) = 1</math>
|- |-
| Exclusion || <math>\forall v_1 \forall l_1 \forall v_2 \forall l_2 ((v_1, l_1) \in K \and (v_2, l_2) \in K \and (v_1, l_1) \ne (v_2, l_2)) \to P(C(l_1) \and C(l_2)) = 0 </math> | Exclusion || <math>\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>
|} |}


Line 506: Line 591:


The probability is given by the allowed values rule, The probability is given by the allowed values rule,
: <math>\sum_{(v, l) \in K \and v \in \operatorname{gset}(V(K))} P(l) = 1</math> : <math>\sum_{(v, l) \in K \land v \in \operatorname{gset}(V(K))} P(l) = 1</math>


which simplifies to, which simplifies to,
Line 530: Line 615:


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, 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>\forall v P(v = V(K)) = \sum_{(v, l) \in K \and v \in \operatorname{gset}(V(K))} ({\prod_{(r, z, u) \in l} P(z = u)})) </math> :<math>\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 ==
==Boolean inductive inference==


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.
Boolean induction<ref>
{{cite journal
|first1=Niki
|last1=Pfeifer
|first2=Gernot D.
|last2=Kleiter
|title=INFERENCE IN CONDITIONAL PROBABILITY LOGIC
|journal=KYBERNETIKA
|date=2006
|volume=42
|issue=4
|page=391– 404
|doi=10.1.1.85.7361
}}
</ref> starts with a target condition ''C'' which is a Boolean expression. ] is of the form,
:''A theory T implies the statement C. As the theory T is simpler than C, induction says that there is a probability that the theory T is implied by C''.


If <math>E(x)</math> is an expression constraining a variable ''x'' then the set of values that the variable may take is,
The method used is based on ].
:<math>\{z : E(z)\}</math>
<ref>Solomonoff, R., "", Report V-131, Zator Co., Cambridge, Ma. Feb 4, 1960, , Nov., 1960.
</ref>
<ref>
Solomonoff, R., "" ''Information and Control'', Vol 7, No. 1 pp 1–22, March 1964.
</ref>
<ref>
Solomonoff, R., "" ''Information and Control'', Vol 7, No. 2 pp 224–254, June 1964.
</ref>


Define the ''gset'' of ''x'' to be the set of values that satisfy the constraints on ''x''. Consider defining ''gset'' as,
See also ].
:<math>\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?
===Results===


=== Meta math definition ===
The expression obtained for the probability that the theory ''T'' is implied by the condion ''C'' is,


A meta-mathematical definition of ''gset'' may be possible. Imagine that what we know of as mathematics is actually implemented by a ] called ''math''. ''math'' takes an ] and gives meaning to the variables and mathematical structures and adds existential quantifiers for variables not explicitly quantified.
:<math>\forall t \in T(C), P(t \mid C) = \frac{\sum_{n: R(n) \equiv t} 2^{-L(n)}}{\sum_{j \in T(C)} \sum_{m: R(m) \equiv j} 2^{-L(m)}} </math>


''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.
A second version of the result derived from the first, by eliminating theories without predictive power is,
:<math>\forall t \in T(C), P(t \mid C) = \frac{P(F(t, c))}{P(F(C, c)) + \sum_{j : j \in T(C) \and P(F(j, c)) > P(F(C, c))} P(E(j, c))} </math>
:<math>P(\operatorname{random}(C) \mid C) = \frac{P(F(t, c))}{P(F(C, c)) + \sum_{j : j \in T(C) \and P(F(j, c)) > P(F(C, c))} P(F(j, c))} </math>


Now suppose there is an extended implementation of mathematics implemented by the ''xmath'' function, defined as,
where,
:<math> \forall t, P(F(t, c)) = \sum_{n: R(n) \equiv t \and L(n) < L(c)} 2^{-L(n)}</math> : <math> \operatorname{xmath} = \forall M, \operatorname{let} T = \operatorname{math} \operatorname{in} T </math>


Using ''xmath'', ''gset'' may be defined by,
=== Implication and condition probability ===
: <math> \forall x \#u, \exists N, \operatorname{gset}(x) = \operatorname{let} M = x \operatorname{in} \{z : z = N \land T\} </math>


Here ] the notation,
The following theorem will be required in the derivation of Boolean induction. Implication is related to conditional probability by the following law,
:<math>A \to B \iff P(B \mid A) = 1</math> :<math>\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.
Derivation,
:<math>A \to B</math>
:<math>\iff P(A \to B) = 1</math>
:<math>\iff P(A \and B \or \neg A) = 1</math>
:<math>\iff P(A \and B) + P(\neg A) = 1</math>
:<math>\iff P(A \and B) = P(A)</math>
:<math>\iff P(A) \cdot P(B \mid A) = P(A)</math>
:<math>\iff P(B \mid A) = 1</math>

=== Probability of a bit string ===

The ] is not valid in the real world. Dice may be loaded, and coins not ]. Knowledge of the physical world must be used to determine if the coin is fair.

However in the mathematical world indifference may be used. One bit of information has equal probability of being 1 or 0. Then each bit string has a probability of occurring,

:<math>P(a) = 2^{-L(a)}</math>

where L(a) is the length of the bit string ''a''.

===Parser for mathematics===

The parser for mathematics, represented by ''R'' is a function that takes a bit string and converts it into a logical condition.

The way the bit string is encoded will determine the probability of Boolean expressions. The encoding should be chosen to give the shortest representation of an expression. Consideration of other encodings is possible. For the purposes of Boolean induction, the encoding given here is considered the best, and no other encoding is necessary. Theoretically this is an approximation.

Each expression is the application of a function to its parameters. The number of bits used to describe a function call is,
* The size of the encoding of the ''function id''.
* The sum of the sizes of the expressions for each parameter.

A constant is encoded as a function with no parameters.

The ''function id'' is encoded with the ] based on the number of uses of the function id in the expression.

====Distribution of natural numbers====

No explicit representation of natural numbers is given. However natural numbers may be constructed by applying the successor function to 0, and then applying other arithmetic functions. A distribution of natural numbers is implied by this, based on the complexity of each number.

===Model for constructing worlds===

A model of how worlds are constructed is used in determining the probabilities of theories,
* A random bit string is selected.
* A condition is constructed from the bit string, using the ].
* A world is constructed that is consistent with the condition.

If ''w'' is the bit string then the world is created such that <math>R(w)</math> is true. An ] has some facts about the word, represented by the bit string ''c'', which gives the condition,
:<math>C = R(c)</math>

The set of bit strings consistent with any condition ''x'' is <math>E(x)</math>.
:<math>\forall x, E(x) = \{w : R(w) \equiv x \}</math>

A theory is a simpler condition that explains (or implies) ''C''. The set of all such theories is called ''T'',
:<math> T(C) = \{t : t \to C \}</math>

===Applying Bayes' theorem===

The next step is to apply the ]
:<math>P(A_i\mid B) = \frac{P(B\mid A_i)\,P(A_i)}{\sum\limits_j P(B\mid A_j)\,P(A_j)}\cdot</math>
where,
:<math>B = E(C)</math>
:<math>A_i = E(t)</math>

To apply Bayes' theorem the following must hold,
* <math>A_i</math> is a ] of the event space.

For <math>T(C)</math> to be a partition, no bit string ''n'' may belong to two theories. To prove this assume they can and derive a contradiction,
:<math>N \in T \and N \in M \and N \ne M \and n \in E(N) \and n \in E(M)</math>
:<math>\implies N \ne M \and R(n) \equiv N \and R(n) \equiv M</math>
:<math>\implies \operatorname{false}</math>

Secondly prove that ''T'' includes all outcomes consistent with the condition. As all theories consistent with ''C'' are included then <math>R(w)</math> must be in this set.

So Bayes theorem may be applied as specified giving,
:<math>\forall t \in T(C), P(E(t) \mid E(C)) = \frac{P(E(t)) \cdot P(E(C) \mid E(t))}{\sum_{j \in T(C)} P(E(j)) \cdot P(E(C) \mid E(j))} </math>

Using the ], the definition of <math>T(C)</math> implies,
:<math>\forall t \in T(C), P(E(C) \mid E(t)) = 1</math>

The probability of each theory in T is given by,
:<math> \forall t \in T(C), P(E(t)) = \sum_{n: R(n) \equiv t} 2^{-L(n)}</math>

so,
:<math>\forall t \in T(C), P(E(t) \mid E(C)) = \frac{\sum_{n: R(n) \equiv t} 2^{-L(n)}}{\sum_{j \in T(C)} \sum_{m: R(m) \equiv j} 2^{-L(m)})} </math>

Finally the probabilities of the events may be identified with the probabilities of the condition which the outcomes in the event satisfy,
:<math>\forall t \in T(C), P(E(t) \mid E(C)) = P(t \mid C)</math>

giving
:<math>\forall t \in T(C), P(t \mid C) = \frac{\sum_{n: R(n) \equiv t} 2^{-L(n)}}{\sum_{j \in T(C)} \sum_{m: R(m) \equiv j} 2^{-L(m)}} </math>

This is the probability of the theory ''t'' after observing that the condition ''C'' holds.

===Removing theories without predictive power===

Theories that are less probable than the condition ''C'' have no predictive power. Separate them out giving,
:<math>\forall t \in T(C), P(t \mid C) = \frac{P(E(t))}{(\sum_{j : j \in T(C) \and P(E(j)) > P(E(C))} P(E(j))) + (\sum_{j : j \in T(C) \and P(E(j)) \le P(E(C))} P(j))} </math>

The probability of the theories without predictive power on ''C'' is the same as the probability of ''C''. So,
:<math>P(E(C)) = \sum_{j : j \in T(C) \and P(E(j)) \le P(E(C))} P(j)</math>

So the probability
:<math>\forall t \in T(C), P(t \mid C) = \frac{P(E(t))}{P(E(C)) + \sum_{j : j \in T(C) \and P(E(j)) > P(E(C))} P(E(j))} </math>

and the probability of no prediction for C, written as <math>\operatorname{random}(C)</math>,
:<math>P(\operatorname{random}(C) \mid C) = \frac{P(E(C))}{P(E(C)) + \sum_{j : j \in T(C) \and P(E(j)) > P(E(C))} P(E(j))} </math>

The probability of a condition was given as,
:<math> \forall t, P(E(t)) = \sum_{n: R(n) \equiv t} 2^{-L(n)}</math>

Bit strings for theories that are more complex than the bit string given to the agent as input have no predictive power. There probabilities are better included in the ''random'' case. To implement this a new definition is given as ''F'' in,

:<math> \forall t, P(F(t, c)) = \sum_{n: R(n) \equiv t \and L(n) < L(c)} 2^{-L(n)}</math>

Using ''F'', an improved version of the inductive probabilities is,
:<math>\forall t \in T(C), P(t \mid C) = \frac{P(F(t, c))}{P(F(C, c)) + \sum_{j : j \in T(C) \and P(F(j, c)) > P(F(C, c))} P(E(j, c))} </math>
:<math>P(\operatorname{random}(C) \mid C) = \frac{P(F(C, c))}{P(F(C, c)) + \sum_{j : j \in T(C) \and P(F(j, c)) > P(F(C, c))} P(F(j, c))} </math>

== The relational model of state ==

] are characterized by having implicit ]. On the surface imperative programs are then very different from ]. However ] provide a way of introducing imperative commands into a functional language, by hiding the state in the monad object.

But monads do not give a completely natural way of representing imperative programming. They do not provide a general model for translating an imperative program into a functional language.

=== Transformations on imperative programs ===
Mathematical expressions may be transformed using mathematical laws to give equivalent expressions. The same ability is needed for imperative programs. A mathematical model for an imperative program would allow a change in the execution order of the program, without changing the overall effect of the program.

Other transformations of imperative programs are needed
* ]
* Transforming class functions from member functions to static functions.
* De-entanglement of objects so that may run efficiently across different machines (using a message protocol).
] is based on a "stateless" model. In this model, each response by the web server is based on the web pages the server is serving and the response from client. The "state" of the users interaction with the web page must be handled by the web page in the browser.

For efficiency the server software does not want to construct all the objects in the object model, as this would require sending too much data in the client response. This leads to a need for static functions, that may work without constructing the object.

This is an implementation strategy, required for scalability, and interaction with standard web security protocols. But it may not be the best way describing the program so that it is ] or understandable by the people. Also there are legacy programs and fat client applications that may need to be transformed into web applications.

These problems, and many more, could be addressed if there was a model for transforming imperative programs using mathematical methods.

=== State holder ===

Using the relational evaluation model, a simple model of state transfer may be given. A statement in an imperative program has,
* Input state
* Input parameters
* return value
* Output state

It is natural in a functional to consider the input state as another parameter. But using the relational evaluation model this is not necessary. the relation model allows the output to be used in determining the input. For example in,
:<math> x \cdot 3 = 9 </math>

''x'' is determined to be 3, when it is only input to the function.

Let the "state holder" be a triple consisting of,
* Input state
* return value
* Output state
Because a state holder takes its input from its output, it does not behave in the same way as other mathematical objects. But with its own set of laws it may be included in a mathematical framework.

The advantage of using a state holder is that state may be transferred through any parameter, providing a full model of imperative programming. The state transfer is completely hidden, and there is a direct translation between imperative programs and state holder programs. State only needs to be transferred where needed.

In comparison monads provide only a linear transfer through primary parameters, but not through every parameter.

A disadvantage is that translating an imperative program to a a state holder form does not make it obey the fundamental axioms of equality. Different equality axioms are followed by state holders. Separate transformations must be applied to put the code in a functional form.

=== Expressions ===

For the purposes of describing state, lower case letters will represent symbols and upper case letters will represent variables.

==== Assignment ====

An assignment statement, represented by :=, is defined by,
:<math> \forall X\#U, \forall I, \forall R, \forall O, (X := (I, R, O)) = (I, R, O]) </math>

where,
:''X'' is a left expression.
:''I'' and ''O'' are states.
:''R'' is an expression.
:<math> O]) </math>

Is the state ''O'' with the value identified by the symbol ''X'' replaced by the value ''R''.

The notation <math>\forall X\#U</math> gives access to the ], in ''U''. This identity is then used to look up the state.

==== State lookup ====

State lookup is represented by,
:<math> \forall X\#U, \forall I, =(I, I, I]) </math>

This definition uses the identity of the variable ''X'' (as ''U'') to lookup the state, and return the value for that identity.

In a typical imperative language, state lookup is implicit. But that would cause some problems in describing state in mathematics.

==== State transfer ====

The following definitions give a version of any function that manages state,
:<math> \forall I, \forall F, \forall X, \forall O, F\ (I, X, O) = (I, F\ X, O) </math>
:<math> \forall I, \forall F, \forall X, \forall O, (I, F, O)\ X = (I, F\ X, O) </math>
:<math> \forall I, \forall F, \forall X, \forall O, (I, F, M)\ (M, X, O) = (I, F\ X, O) </math>

To avoid contradiction the standard definitions of functions would not apply to state holders. That is,
:<math> ((I, X, M) = (M, X, O)) \ne (I = M \and M = O) </math>

instead it only is defined by,
:<math> ((I, X, M) = (M, X, O)) = (I, X = X, O) </math>

This may be achieved given a class hierarchy. Standard equality may be defined for standard objects, but not for state holders.

State holder objects do not obey the substitution rule,
:<math>A = B \to f(A) = f(B)</math>

This is a fundamental principle of mathematics. This rule must be suspended for state holders.

==== Example ====

Take for example,
<source lang='cpp'>
#include <stdio.h>
long x;

long f()
{
return (x = x + 5)+(x = x + 5);
}

void main()
{
x = 2;
long r = f();
printf("x = %ld, r = %ld\n", x, r);
}
</source>

The function ''f'' may be represented as,
:<math> f = (x := 5 + ) + (x := 5 + ) </math>
::<math> =(I_1, I_1, I_1]) </math>
::<math> =(I_2, I_2, I_2]) </math>
:<math> f = (x := 5 + (I_1, I_1, I_1])) + (x := 5 + (I_2, I_2, I_2])) </math>
::<math> F (I, X, O) = (I, F X, O) </math>
:<math> f = (x := (I_1, 5 + I_1, I_1])) + (x := (I_2, 5 + I_2, I_2])) </math>
::<math> (X := (I, R, O)) = (I, R, O]) </math>
:<math> f = ((I_1, 5 + I_1, I_1])) + (I_2, 5 + I_2, I_2]) </math>
::<math> (I, F, M)\ (M, X, O) = (I, F\ X, O) </math>
:<math> f = ((I_1, 5 + I_1 + 5 + I_2, I_2]) </math>
where,
:<math>I_2 = I_1]</math>

Suppose in the initial state <math>I_1 = 2</math>. Then,
:<math> f = ((I_1, 5 + 2 + 5 + I_1, I_2]) </math>
:<math> f = ((I_1, 5 + 2 + 5 + 5+2, I_2) </math>
:<math> f = ((I_1, 19, I_2) </math>

where,
<math> I_2 = I_1</math>

So the C++ program should return,
x = 12, r = 19

=== Control statements ===

==== Statement composition ====

Two statements are composed together, by feeding the output state from one statement into the input state of the next.
:<math>\forall I, \forall R_1, \forall M, \forall R_2, \forall O, (I, R_1, M); (M, R_2, O) \ = (I, R_2, O) </math>

==== If statement ====

An if statement may be regarded as a function, with 3 parameters. ] may be applied. The condition function may be state-full or stateless. Stateless is defined by,
:<math> \forall A, \forall B, (\operatorname{if} \operatorname{true} \operatorname{then} A \operatorname{else} B) = A </math>
:<math> \forall A, \forall B, (\operatorname{if} \operatorname{false} \operatorname{then} A \operatorname{else} B) = B </math>

where ''A'' and ''B'' may be state holders, or other types.
=== Example ===
State-full is defined by
:<math>\forall I, \forall M, \forall A, \forall B, \forall C, \operatorname{if} (I, C, M) \operatorname{then} A \operatorname{else} B = (I, C, M); \operatorname{if} C \operatorname{then} A \operatorname{else} B </math>


For example take the constraint expression <math>x^2 = 4</math>. Then,
For example,
:<math>x^2 = 4</math>
:<math>\land s = \operatorname{gset}(x)</math>
:<math> \land (\forall x \#u, \exists N \operatorname{gset}(x) = \operatorname{let} M = x \operatorname{in} \{z : z = N \land T\}) </math>


Then the ''xmath'' expression is,
{| class="wikitable mw-collapsible mw-collapsed"
:<math>\forall M, \operatorname{let} T = </math>
|-
::<math>\exists x, \exists s, (x^2 = 4</math>
! State-full if statement.
::<math>\land s = \operatorname{gset}(x)</math>
|-
| <math> x := 6; \operatorname{if} = 6 \operatorname{then} x := /2 \operatorname{else} x:=/3 </math> ::<math>\land (\forall x \#u, \exists N, \operatorname{gset}(x) = \operatorname{let} M = x \operatorname{in} \{z : z = N \land T\})</math>
:<math> \operatorname{in} T </math>
|-
| <math> (I_1, 6, I_1); \operatorname{if} (I_2, I_2 = 6, I_2) \operatorname{then} x := /2 \operatorname{else} x:=/3 </math>
|-
| <math> (I_1, 6, I_1); (I_2, I_2 = 6, I_2); \operatorname{if} I_2 = 6 \operatorname{then} x := /2 \operatorname{else} x:=/3 </math>
|-
| <math> (I_1, 6, I_1); (I_1, I_1 = 6, I_1) ; \operatorname{if} I_1 = 6 \operatorname{then} x := /2 \operatorname{else} x:=/3 </math>
|-
| <math> (I_1, 6 = 6, I_1) ; \operatorname{if} 6 = 6 \operatorname{then} x := /2 \operatorname{else} x:=/3 </math>
|-
| <math> (I_1, \operatorname{true}, I_1) ; x := /2 </math>
|-
| <math> (I_1, \operatorname{true}, I_1); (I_1, I_1/2, I_1/2]) </math>
|-
| <math> (I_1, I_1 = 6, I_1); (I_1, 6/2, I_1) </math>
|-
| <math> (I_1, I_1 = 6, I_1); (I_1, 3, I_1) </math>
|-
| <math> (I_1, 3, I_1) </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''),
==== While statement ====
:<math>M = x \land s = \{z : z = N \land T\} </math>


Here <math>T</math> invokes ''T'' with M as N.
The while statement is defined by,
:<math>s = \{z : z = N \land x^2 = 4 \land x = N\}</math>
:<math>\forall C, \forall B, \operatorname{while} C \operatorname{do} B = \operatorname{if} C \operatorname{then} (B; \operatorname{while} C \operatorname{do} B) </math>
:<math>s = \{z : z^2 = 4\} </math>

If ''C'' is not a state holder this statement either does nothing or expands recursively forever. If ''C'' is a state holder, the value represented by ''C'' does not need to be the same each time, even though the expression is the same.

=== Functions and return values ===

Many imperative languages use a fairly unnatural structure for defining functions. The natural structure is that the body of the function is an expression. The return value of the function is the value of the expression. The function call is then equal to the body of the function, with formal parameters replaced by actual parameters. The return value may be stateless, or it may be a state holder.

However imperative languages use statement composition which composes a state holder, which has no sensible return value. The return statement is then needed to capture a value from a state. An extra structure called the return frame is needed to get the value from a return statement.

==== Return frame ====

The return frame accepts the return value. The value may be stateless, or a state holder.
:<math> \forall X, \operatorname{returnframe}(\operatorname{return} X) = X </math>

==== Declaration frame ====

The declaration frame is required to insure the calling of destructors. It is defined by,
:<math> \forall I, \forall R, \forall O, \forall X, \forall Q, \operatorname{declareframe}(X, \operatorname{return} (I, R, O)) = (I, \_, O); destroy(X); (Q, R, Q) </math>

==== Return statement ====

The return statement is defined by,
:<math>\forall I, \forall D, \forall M, \forall R, \forall O, (I, D, M); \operatorname{return} (M, R, O) = \operatorname{return} (I, R, O)</math>
:<math>\forall X, \forall U, (\operatorname{return} X; U) = \operatorname{return} X</math>


== See also == == See also ==


* ]
** ]
** ]
* ] * ]
** ] ** ]
Line 921: Line 675:
** ] ** ]
** ] ** ]
* ]
** ]
** ]
* ] * ]
** ] ** ]
Line 930: Line 687:
** ] ** ]
** ] ** ]
* ]


== References == == References ==
Line 937: Line 695:
] ]
] ]
]

Latest revision as of 08:08, 27 February 2020

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,

x 2 = 4 {\displaystyle x^{2}=4}

which implies,

x = 2 x = 2 {\displaystyle x=2\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 = ± 2 {\displaystyle x=\pm 2}

Naively then,

x + x { 4 , 0 , 4 } {\displaystyle x+x\in \lbrace 4,0,-4\rbrace }

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,

V ( { 2 :: x 1 , 2 :: x 2 } ) {\displaystyle V(\{2::x_{1},-2::x_{2}\})}

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

  • 2 :: x 1 {\displaystyle 2::x_{1}}
  • 2 :: x 2 {\displaystyle -2::x_{2}}

The value 2 is associated with the possible world x 1 {\displaystyle x_{1}} . The value −2 is associated with the possible world x 2 {\displaystyle x_{2}} . This means that the value cannot be both 2 and −2 at the same time. In the world x 1 {\displaystyle x_{1}} the value of the value set must be 2. In the world x 2 {\displaystyle x_{2}} the value of the value set must be −2.

The solution of the equation,

x 2 = 4 {\displaystyle x^{2}=4}

is,

x = V ( { 2 :: x 1 , 2 :: x 2 } ) {\displaystyle x=V(\{2::x_{1},-2::x_{2}\})}

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 { x 1 , x 2 } {\displaystyle \{x_{1},x_{2}\}} is a world set as either x = 2 (in world x 1 {\displaystyle x_{1}} ) or x= −2 (in world x 2 {\displaystyle 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 {\displaystyle x_{1}} and x 2 {\displaystyle x_{2}} are true at the same time.

( x = 2 x = 2 ) = false {\displaystyle (x=2\land x=-2)={\text{false}}}

Application of functions

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

V ( M )   V ( N ) = V ( { ( m v   n v , m l n l ) : m v :: m l M n v :: n l N } ) {\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\})}

For example,

x + x = V ( { 2 :: x 1 , 2 :: x 2 } ) + V ( { 2 :: x 1 , 2 :: x 2 } ) {\displaystyle x+x=V(\{2::x_{1},-2::x_{2}\})+V(\{2::x_{1},-2::x_{2}\})}

is,

= V ( { 2 + 2 :: x 1 x 1 , 2 + 2 :: x 1 x 2 , 2 + 2 :: x 1 x 2 , 2 + 2 :: x 2 } ) {\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}\})}
= V ( { 4 :: x 1 x 1 , 0 :: x 1 x 2 , 0 :: x 2 x 1 , 2 + 2 :: x 2 x 1 } ) {\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}\})}

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

x 1 x 1 = x 1 {\displaystyle x_{1}\cap x_{1}=x_{1}}
x 2 x 2 = x 2 {\displaystyle x_{2}\cap x_{2}=x_{2}}

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

x 1 x 2 = { } {\displaystyle x_{1}\cap x_{2}=\{\}}
x 2 x 1 = { } {\displaystyle x_{2}\cap x_{1}=\{\}}

So,

= V ( { 4 :: x 1 , 0 :: { } , 0 :: { } , 4 :: x 2 } ) {\displaystyle =V(\{-4::x_{1},0::\{\},0::\{\},4::x_{2}\})}

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

V ( K ) = V ( { ( v , l ) : ( v , l ) K l { } } {\displaystyle V(K)=V(\{(v,l):(v,l)\in K\land l\neq \{\}\}}

giving,

= V ( { 4 :: x 1 , 4 :: x 2 } ) {\displaystyle =V(\{-4::x_{1},4::x_{2}\})}

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

Application to Booleans

a b {\displaystyle a\land b}

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

a b {\displaystyle a\lor b}

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

a = V ( { false :: a 1 , true :: a 2 } ) {\displaystyle a=V(\{\operatorname {false} ::a_{1},\operatorname {true} ::a_{2}\})}

then for b

b = V ( { true :: a 1 , false :: a 2 , true :: a 2 } ) {\displaystyle b=V(\{\operatorname {true} ::a_{1},\operatorname {false} ::a_{2},\operatorname {true} ::a_{2}\})}

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

Now consider,

x = 2 x = 2 {\displaystyle x=2\lor x=-2}

gives,

x = V ( { _ :: a 1 , 2 :: a 2 } ) {\displaystyle x=V(\{\_::a_{1},2::a_{2}\})}

and

x = V ( { 2 :: a 1 , _ :: a 2 , 2 :: a 2 } ) {\displaystyle x=V(\{-2::a_{1},\_::a_{2},-2::a_{2}\})}

unifying these two value sets gives,

x = V ( { 2 :: a 1 , 2 :: a 2 } ) {\displaystyle x=V(\{-2::a_{1},2::a_{2}\})}

The pair 2 :: a 2 {\displaystyle -2::a_{2}} is dropped because of the "assert equal" rule,

m v m l n v n l ( ( m v , m l ) M ( n v , n l ) N ) ( m v n v m l n l = { } ) {\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}\neq n_{v}\to m_{l}\cap n_{l}=\{\})}

Its value 2 :: a 2 {\displaystyle -2::a_{2}} did not match with 2 :: a 2 {\displaystyle 2::a_{2}} .

Dependent worlds

Consider the problem,

X = V ( { 1 :: x 1 , 3 :: x 2 , 4 :: x 3 } ) {\displaystyle X=V(\{1::x_{1},3::x_{2},4::x_{3}\})}
Y = V ( { 8 :: y 1 , 9 :: y 2 } ) {\displaystyle Y=V(\{8::y_{1},9::y_{2}\})}
X Y < 25 {\displaystyle X*Y<25}
X + Y > 10 {\displaystyle X+Y>10}

Firstly calculate the value set for X Y < 25 {\displaystyle X*Y<25} ,

V ( { 8 :: x 1 y 1 , 24 :: x 2 y 1 , 32 :: x 3 y 1 , 9 :: x 1 y 2 , 27 :: x 2 y 2 , 36 :: x 3 y 2 } ) < 25 {\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}\})<25}
V ( { 8 < 25 :: x 1 y 1 , 24 < 25 :: x 2 y 1 , 32 < 25 :: x 3 y 1 , 9 < 25 :: x 1 y 2 , 27 < 25 :: x 2 y 2 , 36 < 25 :: x 3 y 2 } ) < 25 {\displaystyle V(\{8<25::x_{1}\cap y_{1},24<25::x_{2}\cap y_{1},32<25::x_{3}\cap y_{1},9<25::x_{1}\cap y_{2},27<25::x_{2}\cap y_{2},36<25::x_{3}\cap y_{2}\})<25}
V ( { true :: x 1 y 1 , true :: x 2 y 1 , false :: x 3 y 1 , true :: x 1 y 2 , false :: x 2 y 2 , false :: x 3 y 2 } ) {\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}\})}

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

V ( { true :: x 1 y 1 , true :: x 2 y 2 , true :: x 1 y 2 } ) {\displaystyle V(\{{\text{true}}::x_{1}\cap y_{1},{\text{true}}::x_{2}\cap y_{2},{\text{true}}::x_{1}\cap y_{2}\})}

The worlds,

x 3 y 1 {\displaystyle x_{3}\cap y_{1}}
x 2 y 2 {\displaystyle x_{2}\cap y_{2}}
x 3 y 2 {\displaystyle x_{3}\cap y_{2}}

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 X 3 {\displaystyle X_{3}} is not represented in this value, and so must be empty. The value set for X {\displaystyle X} is now smaller,

X = V ( { 1 :: x 1 , 3 :: x 2 } ) {\displaystyle X=V(\{1::x_{1},3::x_{2}\})}

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

X + Y > 10 {\displaystyle X+Y>10}

Then the value sets are,

X = V ( { 1 :: x 1 , 3 :: x 2 } ) {\displaystyle X=V(\{1::x_{1},3::x_{2}\})}
Y = V ( { 8 :: y 1 , 9 :: y 2 } ) {\displaystyle Y=V(\{8::y_{1},9::y_{2}\})}

And the calculation is,

V ( { 1 + 8 :: x 1 y 1 , 3 + 8 :: x 2 y 1 , 2 + 9 :: x 1 y 2 , 1 + 9 :: x 2 y 2 } ) > 10 {\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}\})>10}

But x 2 y 2 {\displaystyle x_{2}\cap y_{2}} is empty. So,

V ( { 9 > 10 :: x 1 y 1 , 11 > 10 :: x 2 y 1 , 10 > 10 :: x 1 y 2 } ) {\displaystyle V(\{9>10::x_{1}\cap y_{1},11>10::x_{2}\cap y_{1},10>10::x_{1}\cap y_{2}\})}

So x 1 y 1 {\displaystyle x_{1}\cap y_{1}} and x 1 y 2 {\displaystyle x_{1}\cap y_{2}} are empty,

V ( { 11 > 10 :: x 2 y 1 } ) {\displaystyle V(\{11>10::x_{2}\cap y_{1}\})}

Now X 1 {\displaystyle X_{1}} and Y 2 {\displaystyle Y_{2}} are not represented, and are removed as dependent worlds. So,

X = V ( { 3 :: x 2 } ) = 3 {\displaystyle X=V(\{3::x_{2}\})=3}
Y = V ( { 8 :: y 1 } ) = 8 {\displaystyle Y=V(\{8::y_{1}\})=8}

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,

PizzaShop ( V ( { Carlton :: p 1 , Richmond :: p 2 , South Melbourne :: p 3 , Footscray :: p 4 , St Kilda :: p 5 , Toorak :: p 6 } ) ) {\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}\}))}

Beer you can get at,

BottleshopWithBeer ( V ( { South Melbourne :: b 1 , St Kilda :: b 2 , Carlton :: b 3 , Docklands :: b 4 } ) ) {\displaystyle {\text{BottleshopWithBeer}}(V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\}))}

Whiskey,

BottleshopWithWhiskey ( V ( { Essendon :: w 1 , South Melbourne :: w 2 } ) ) {\displaystyle {\text{BottleshopWithWhiskey}}(V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\}))}

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

WhereToGo ( x ) = PizzaShop ( x ) BottleshopWithBeer ( x ) BottleshopWithWhiskey ( x ) {\displaystyle {\text{WhereToGo}}(x)={\text{PizzaShop}}(x)\land {\text{BottleshopWithBeer}}(x)\land {\text{BottleshopWithWhiskey}}(x)}

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

x = V ( { Carlton :: p 1 , Richmond :: p 2 , South Melbourne :: p 3 , Footscray :: p 4 , St Kilda :: p 5 , Toorak :: p 6 } ) {\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}\})}

Then we need to unify this with,

x = V ( { South Melbourne :: b 1 , St Kilda :: b 2 , Carlton :: b 3 , Docklands :: b 4 } ) {\displaystyle x=V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\})}

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

x = V ( { South Melbourne :: b 1 p 3 , St Kilda :: b 2 p 5 , Carlton :: b 3 p 1 } ) {\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}\})}

Finally we need to unify with whiskey.

x = V ( { Essendon :: w 1 , South Melbourne :: w 2 } ) {\displaystyle x=V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\})}

Which gives 6 combinations. The matching one is,

x = V ( { South Melbourne :: b 1 p 3 w 2 } ) {\displaystyle x=V(\{{\text{South Melbourne}}::b_{1}\cap p_{3}\cap w_{2}\})}

A total of 30 combinations were generated.

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

x = V ( { Essendon :: w 1 , South Melbourne :: w 2 } ) {\displaystyle x=V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\})}

Then we need to unify this with,

x = V ( { South Melbourne :: b 1 , St Kilda :: b 2 , Carlton :: b 3 , Docklands :: b 4 } ) {\displaystyle x=V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\})}

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

x = V ( { South Melbourne :: b 1 w 2 } ) {\displaystyle x=V(\{{\text{South Melbourne}}::b_{1}\cap w_{2}\})}

Finally we need to unify with pizza.

x = { Carlton :: p 1 , Richmond :: p 2 , South Melbourne :: p 3 , Footscray :: p 4 , St Kilda :: p 5 , Toorak :: p 6 } {\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}\}}

Which gives 6 combinations. The matching one is,

x = V ( { South Melbourne :: b 1 w 2   p 3 } ) {\displaystyle x=V(\{{\text{South Melbourne}}::b_{1}\cap w_{2}\ \cap p_{3}\})}

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,

let x X in x {\displaystyle \operatorname {let} x\in X\operatorname {in} x}

In this expression x X {\displaystyle x\in X} 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,

( let x X in x )   ( let y Y in y ) {\displaystyle (\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)}
= let x X y Y in x   y {\displaystyle =\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y}
= let ( x , y ) X × Y in x   y {\displaystyle =\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y}

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.

( let x X in x )   ( let x X in x ) {\displaystyle (\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)}
= let x X in x   x {\displaystyle =\operatorname {let} x\in X\operatorname {in} x\ x}

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 ( v , l ) {\displaystyle (v,l)} means that the value of the value set V ( K ) {\displaystyle V(K)} is v if the condition function applied to the list, C ( l ) {\displaystyle C(l)} , 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 C ( l ) = ( ( r , z , u ) l z = u ) ) = ( r z u ( r , z , u ) l z = u ) {\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)}
Value condition v l ( ( v , l ) K C ( l ) v = V ( K ) {\displaystyle \forall v\forall l((v,l)\in K\land C(l)\to v=V(K)}
Complete set v l ( v , l ) K C ( l ) {\displaystyle \exists v\exists l(v,l)\in K\land C(l)}
Exclusion v 1 l 1 v 2 l 2 ( ( v 1 , l 1 ) K ( v 2 , l 2 ) K ( v 1 , l 1 ) ( v 2 , l 2 ) ) ¬ ( C ( l 1 ) C ( l 2 ) ) {\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})\neq (v_{2},l_{2}))\to \neg (C(l_{1})\land C(l_{2}))}

Value function

Using the value condition and complete set axioms,

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

As a let expression this becomes,

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

Single value

The value set to represent a single value is,

k = V ( { ( k , { } ) } ) {\displaystyle k=V(\{(k,\{\})\})}

The derivation is,

V ( { ( k , { } ) } ) {\displaystyle V(\{(k,\{\})\})}
= let ( v , l ) { ( k , { } ) } C ( l ) in v {\displaystyle =\operatorname {let} (v,l)\in \{(k,\{\})\}\land C(l)\operatorname {in} v}
= let v = k C ( { } ) in v {\displaystyle =\operatorname {let} v=k\land C(\{\})\operatorname {in} v}
= let v = k in v {\displaystyle =\operatorname {let} v=k\operatorname {in} v}
= k {\displaystyle =k}

Element of a set

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

x X ( let x X in x ) = let R = V ( { ( w , { ( R , x , w ) } ) : w X } ) in R {\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}

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

x = V ( R ) {\displaystyle x=V(R)} .

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,

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

The derivation is,

V ( { ( w , { ( r , x , w ) : w X } ) {\displaystyle V(\{(w,\{(r,x,w):w\in X\})}
= let ( v , l ) { ( w , { ( r , x , w ) } ) : w X } C ( l ) in v {\displaystyle =\operatorname {let} (v,l)\in \{(w,\{(r,x,w)\}):w\in X\}\land C(l)\operatorname {in} v}
= let v X ( ( r , z , u ) { ( _ , x , v ) } z = u ) in v {\displaystyle =\operatorname {let} v\in X\land ({\bigwedge _{(r,z,u)\in \{(\_,x,v)\}}z=u})\operatorname {in} v}
= let v X ( r z u ( r , z , u ) { ( _ , x , v ) } z = u ) in v {\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}
= let v X x = v in v {\displaystyle =\operatorname {let} v\in X\land x=v\operatorname {in} v}
= let x X in x {\displaystyle =\operatorname {let} x\in X\operatorname {in} x}

Application of functions

Function application of value sets is given by,

V ( M )   V ( N ) = V ( { ( m v   n v , m l n l ) : ( m v , m l ) M ( n v , n l ) N } ) {\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\})}

Derivation,

V ( M )   V ( N ) {\displaystyle V(M)\ V(N)}
= let ( m v , m l ) M C ( m l ) in m v )   ( let ( n v , n l ) N C ( n l ) in n v ) {\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})}
= let ( m v , m l ) M ( n v , n l ) N C ( n l ) C ( n l ) in m v   n v ) {\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})}

Then using,

C ( m l ) C ( n l ) {\displaystyle C(m_{l})\land C(n_{l})}
= ( ( z , u ) m l z = u ) ( ( z , u ) n l z = u ) {\displaystyle =({\bigwedge _{(z,u)\in m_{l}}z=u})\land ({\bigwedge _{(z,u)\in n_{l}}z=u})}
= ( ( z , u ) m l n l z = u ) {\displaystyle =({\bigwedge _{(z,u)\in m_{l}\cup n_{l}}z=u})}
= C ( m l n l ) {\displaystyle =C(m_{l}\cup n_{l})}

get,

= let ( m v , m l ) M ( n v , n l ) N C ( n l n l ) in m v   n v ) {\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})}
= let ( v , l ) { ( m v   n v , m l n l ) : ( m v , m l ) M ( n v , n l ) N } C ( l ) in v {\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}
= V ( { ( m v   n v , m l n l ) : ( m v , m l ) M ( n v , n l ) N } ) {\displaystyle =V(\{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\})}

Exclusion

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

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

This may be derived from,

V ( M ) s {\displaystyle V(M)\in s}
v l ( ( v , l ) M C ( l ) ) ( v = V [ M ] V ( M ) s ) {\displaystyle \to \forall v\forall l((v,l)\in M\land C(l))\to (v=V\land V(M)\in s)}
v l ( ( v , l ) M C ( l ) ) v S {\displaystyle \to \forall v\forall l((v,l)\in M\land C(l))\to v\in S}
v l ( ( v , l ) M v S ) ¬ C ( l ) {\displaystyle \to \forall v\forall l((v,l)\in M\land v\not \in S)\to \neg C(l)}

Simplification

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

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

Derivation

V ( { ( v , l ) : ( v , l ) K C ( l ) } ) {\displaystyle V(\{(v,l):(v,l)\in K\land C(l)\})}
= let ( v , l ) { ( v , l ) : ( v , l ) K C ( l ) } C ( l ) in v {\displaystyle =\operatorname {let} (v,l)\in \{(v,l):(v,l)\in K\land C(l)\}\land C(l)\operatorname {in} v}
= let ( v , l ) K C ( l ) C ( l ) in v {\displaystyle =\operatorname {let} (v,l)\in K\land C(l)\land C(l)\operatorname {in} v}
= let ( v , l ) K C ( l ) in v {\displaystyle =\operatorname {let} (v,l)\in K\land C(l)\operatorname {in} v}
= V ( K ) {\displaystyle =V(K)}

Summary of results

Name Rule
Value function V ( K ) = let ( v , l ) K C ( l ) in v {\displaystyle V(K)=\operatorname {let} (v,l)\in K\land C(l)\operatorname {in} v}
Single value k = V ( { ( k , { } ) } ) {\displaystyle k=V(\{(k,\{\})\})}
Set element x X ( let x X in x ) = let R = V ( { ( w , { ( R , x , w ) } ) : w X } ) in R {\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}
Function application V ( M )   V ( N ) = V ( { ( m v   n v , m l n l ) : ( m v , m l ) M ( n v , n l ) N } ) {\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\})}
Exclusion V ( M ) s ( v l ( ( v , l ) M v s ) ¬ C ( l ) ) {\displaystyle V(M)\in s\iff (\forall v\forall l((v,l)\in M\land v\not \in s)\to \neg C(l))}
Simplification V ( K ) = V ( { ( v , l ) : ( v , l ) K C ( l ) } ) {\displaystyle V(K)=V(\{(v,l):(v,l)\in K\land C(l)\})}
Assert equal V ( M ) = V ( N ) ( v l ( ( v , l ) N v S ( M ) ) ¬ C ( l ) ) {\displaystyle V(M)=V(N)\to (\forall v\forall l((v,l)\in N\land v\not \in S(M))\to \neg C(l))}

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,

x # u {\displaystyle \forall x\#u}

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,

x # u X ( let x X in x ) = let R = V ( ( u , { ( w , { ( R , x , w ) } ) : w X } ) ) in R {\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}

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,

m v m l n v n l ( ( m v , m l ) M ( n v , n l ) N ) ( m v n v ¬ ( C ( m l ) C ( n l ) ) ) {\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}\neq n_{v}\to \neg (C(m_{l})\land C(n_{l})))}

For the derivation, start with,

V ( M ) = V ( N ) {\displaystyle V(M)=V(N)}

The value condition gives,

( m v m l ( ( m v , m l ) M C ( m l ) v = V ( M ) ) ( n v n l ( ( n v , k ) N C ( n l ) ) n v = V ( N ) ) V ( M ) = V ( N ) {\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)}
m v m l n v n l ( ( ( m v , m l ) M C ( m l ) ) m v = V ( M ) ) ( ( ( n v , n l ) N C ( n l ) ) n v = V ( N ) ) V ( M ) = V ( N ) {\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)}
m v m l n v n l ( ( m v , m l ) M ( n v , n l ) N ) ( C ( j ) C ( k ) v = u ) {\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)}
m v m l n v n l ( ( m v , m l ) M ( n v , n l ) N ) ( m v n v ¬ ( C ( m l ) C ( n l ) ) ) {\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}\neq n_{v}\to \neg (C(m_{l})\land C(n_{l})))}

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,

C ( l ) = ( ( r , z , u ) l z = u ) ) {\displaystyle C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))}

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

C ( { ( r , z , u ) } = ( z = u ) {\displaystyle C(\{(r,z,u)\}=(z=u)}

So if this is false C ( l ) {\displaystyle C(l)} 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,

v 1 l 1 v 2 l 2 ( ( v 1 , l 1 ) K ( v 2 , l 2 ) K ( v 1 , l 1 ) ( v 2 , l 2 ) ) ¬ ( C ( l 1 ) C ( l 2 ) ) {\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})\neq (v_{2},l_{2}))\implies \neg (C(l_{1})\land C(l_{2}))}

Then for any set of dependent conditions l,

( ( K , x , v 1 ) l   ( K , x , v 2 ) l v 1 v 2 {\displaystyle ((K,x,v_{1})\in l\ \land (K,x,v_{2})\in l\land v_{1}\neq v_{2}}
( v 1 , { ( K , x , v 1 ) } ) K ( v 2 , { ( K , x , v 2 ) } ) K ( v 1 , l 1 ) ( v 2 , l 2 ) ) {\displaystyle \implies (v_{1},\{(K,x,v_{1})\})\in K\land (v_{2},\{(K,x,v_{2})\})\in K\land (v_{1},l_{1})\neq (v_{2},l_{2}))}
¬ ( C ( { ( K , x , v 1 ) } ) C ( { ( K , x , v 2 ) } ) ) {\displaystyle \implies \neg (C(\{(K,x,v_{1})\})\land C(\{(K,x,v_{2})\}))}
¬ C ( l ) {\displaystyle \implies \neg C(l)}

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,

v   l ( v , l ) K C ( l ) {\displaystyle \exists v\exists \ l(v,l)\in K\to C(l)}

The condition function is,

C ( l ) = ( ( r , z , u ) l z = u ) ) {\displaystyle C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))}

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

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

So

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

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

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

and so,

V ( L ) E ( K , L ) {\displaystyle V(L)\in E(K,L)}

Then using the exclusion rule,

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

gives,

( K L v l ( ( v , l ) L v E ( K , L ) ) ¬ C ( l ) ) {\displaystyle (\forall K\forall L\forall v\forall l((v,l)\in L\land v\not \in E(K,L))\to \neg C(l))}

This is the narrowing exclusion rule. E ( K , L ) {\displaystyle E(K,L)} 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,

C ( l ) = ( ( r , z , u ) l z = u ) ) {\displaystyle C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))}

The probability function is,

P ( l ) = ( ( r , z , u ) l P ( z = u ) ) ) {\displaystyle P(l)=({\prod _{(r,z,u)\in l}P(z=u)}))}

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 ( v , l ) {\displaystyle (v,l)} means that the probability of the value set V ( K ) {\displaystyle V(K)} is v is the probability function applied to the list, P ( l ) {\displaystyle P(l)} .
  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 P ( l ) = ( ( r , z , u ) l P ( z = u ) ) ) {\displaystyle P(l)=({\prod _{(r,z,u)\in l}P(z=u)}))}
Value condition v P ( v = V ( K ) ) = ( v , l ) K P ( l ) {\displaystyle \forall vP(v=V(K))=\sum _{(v,l)\in K}P(l)}
Complete set ( v , l ) K P ( l ) = 1 {\displaystyle \sum _{(v,l)\in K}P(l)=1}
Allowed values ( v , l ) K v gset ( V ( K ) ) P ( l ) = 1 {\displaystyle \sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}P(l)=1}
Exclusion v 1 l 1 v 2 l 2 ( ( v 1 , l 1 ) K ( v 2 , l 2 ) K ( v 1 , l 1 ) ( v 2 , l 2 ) ) P ( C ( l 1 ) C ( l 2 ) ) = 0 {\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})\neq (v_{2},l_{2}))\to P(C(l_{1})\land C(l_{2}))=0}

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,

k = V ( { ( k , { } ) } ) {\displaystyle k=V(\{(k,\{\})\})}

The complete set rule is,

( v , l ) K P ( l ) {\displaystyle \sum _{(v,l)\in K}P(l)}
= ( v , l ) { ( k , { } ) } P ( l ) {\displaystyle =\sum _{(v,l)\in \{(k,\{\})\}}P(l)}
= P ( { } ) {\displaystyle =P(\{\})}
= 1 {\displaystyle =1}

Which is consistent with the axiom.

Probabilities for multiple values

The value set to represent multiple values is,

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

The probability is given by the allowed values rule,

( v , l ) K v gset ( V ( K ) ) P ( l ) = 1 {\displaystyle \sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}P(l)=1}

which simplifies to,

v gset ( V ( K ) ) P ( x = v ) = 1 {\displaystyle \sum _{v\in \operatorname {gset} (V(K))}P(x=v)=1}

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.

v gset ( V ( K ) ) , P ( x = v ) = w P i ( x = v ) {\displaystyle \forall v\in \operatorname {gset} (V(K)),P(x=v)=w*P_{i}(x=v)}

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

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

So,

v gset ( V ( K ) ) w P i ( x = v ) = 1 {\displaystyle \sum _{v\in \operatorname {gset} (V(K))}w*P_{i}(x=v)=1}
w = 1 v gset ( V ( K ) ) P i ( x = v ) {\displaystyle w={\frac {1}{\sum _{v\in \operatorname {gset} (V(K))}P_{i}(x=v)}}}
v gset ( V ( K ) ) , P ( x = v ) = P i ( x = v ) v gset ( V ( K ) ) P i ( x = v ) {\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)}}}
v gset ( V ( K ) ) , P ( x = v ) = 0 {\displaystyle \forall v\not \in \operatorname {gset} (V(K)),P(x=v)=0}

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

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

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,

v P ( v = V ( K ) ) = ( v , l ) K v gset ( V ( K ) ) ( ( r , z , u ) l P ( z = u ) ) ) {\displaystyle \forall vP(v=V(K))=\sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}({\prod _{(r,z,u)\in l}P(z=u)}))}

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 E ( x ) {\displaystyle E(x)} is an expression constraining a variable x then the set of values that the variable may take is,

{ z : E ( z ) } {\displaystyle \{z:E(z)\}}

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

gset ( x ) = { z : E ( z ) } {\displaystyle \operatorname {gset} (x)=\{z:E(z)\}}

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,

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

Using xmath, gset may be defined by,

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

Here again the notation,

x # u {\displaystyle \forall x\#u}

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 x 2 = 4 {\displaystyle x^{2}=4} . Then,

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

Then the xmath expression is,

M , let T [ M ] = {\displaystyle \forall M,\operatorname {let} T=}
x , s , ( x 2 = 4 {\displaystyle \exists x,\exists s,(x^{2}=4}
s = gset ( x ) {\displaystyle \land s=\operatorname {gset} (x)}
( x # u , N , gset ( x ) = let M [ u ] = x in { z : z = N [ u ] T [ N ] } ) {\displaystyle \land (\forall x\#u,\exists N,\operatorname {gset} (x)=\operatorname {let} M=x\operatorname {in} \{z:z=N\land T\})}
in T [ _ ] {\displaystyle \operatorname {in} T}

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),

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

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

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

See also

References

  1. Kirchner, Hélène; Ringeissen, Christophe (1994). "Constraint Solving by Narrowing in Combined Algebraic Domains". Proc. 11th International Conference on Logic Programming. The MIT press. pp. 617–31.
  2. Arenas, Puri; Artalejo, Mario Rodríguez (1997). "A Lazy Narrowing Calculus for Functional Logic Programming with Algebraic Polymorphic Types.". Proc. of the International Symposium on Logic Programming (ILPS'97). The MIT Press. pp. 53–67.
  3. Marriott, Kim; Stuckey, Peter J. (1998). Programming with constraints: An introduction. MIT Press.
Categories:
Narrowing of algebraic value sets: Difference between revisions Add topic