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.
The assignment statement allows a variable to change its value.
Functional languages based on lambda calculus allow this mathematical approach to programming.
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.
Narrowing is a technique that allows logical deduction, with the flexibility of functional languages.
A variable may only take on a single value in each possible world.
Narrowing rules also detect situations where some combinations of worlds are shown to be impossible.
For example consider the equation, which implies, But this is a bit long winded, and it does not allow us to work with multiple values at the same time.
The solution of the equation, is, A possible world is used here as an informal term.
Formally a possible world is defined by a Boolean condition.
The term "possible world" is used to make the description of value sets easier to follow.
Consider the problem, Firstly calculate the value set for
, As this statement is asserted true, all the false values are dropped giving, The worlds, are impossible.
Then calculations should proceed first where the product of the sizes of the input value sets is smallest.
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, Beer you can get at, Whiskey, The cops are about and we are not getting any younger.
The matching one is, The result is the same but only 14 combinations were generated to arrive at the conclusion.
Also the set of conditions is used in narrowing by exclusion of dependent values.
If the addition of R to the dependent condition is ignored, the expression takes on a simpler and more understandable form, The derivation is, Function application of value sets is given by, Derivation, Then using, get, The exclusion is a rule that determines when conditions must be false, This may be derived from, The simplification rule allows values whose condition is false to be dropped.
This would make value sets distinct, unless they are based on the same variable.
For the sake of readability this extra level of structure has been omitted from the definition of value sets.
Considered as the basis for an algorithm for solving equations, this narrowing gives a set of values consistent with the constraints on a variable.
Consider defining gset as, This definition depends on knowing the expression E, which is the condition giving all the constraints on x.
So there is no mathematical function that may be applied to a variable to request the set of values.
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.
Now suppose there is an extended implementation of mathematics implemented by the xmath function, defined as, Using xmath, gset may be defined by, Here again the notation, is used to mean quantification over variables x where x refers to the value, and u refers to the unique identity of the variable.