User:Thepigdog/Constraint Logic Programming Theory

From Knowino
Jump to: navigation, search

Contents

[edit] Purpose of this Web Page

The purpose of this web page is to describe a formal theory of Constraint Logic Programming.

Constraint Logic Programming is an approach to evaluating the values of variables constrained by equations.

[edit] Summary

Variables have inital sets of values described by there type. Each equation or statement constrains or narrows the values that variables may hold. An equation or statement is an expression that evaluates to true.

The values that a variable may hold are held in value sets. Each value is tagged against a Possible World, which may be considered as an alternate possibility.

By arguing backwards from the final results sets of of values may be determined or narrowed.

The order of evaluation may be chosen so as to minimise the size of the value sets that are created. This approach gives an efficient method of evaluating the constrained variables.

[edit] Definitions

In this section I attempt to formally describe the general statements made above.

The ideas involved here are fairly simple. However generalising the description always makes it harder to understand.

[edit] Possible Worlds

A Possible World is a logically a set of bindings of variables to values. However we do not usually explicitly represent these bindings.

Possible worlds are sets and behave like sets,

The intersection of Possible Worlds M and N obeys the set laws,

M\cap M = M\!
If M \sub N then M\cap N = M
M\cap N \sub M\!
M\cap N \sub N\!

Each possible world is a sub-world (sub set) of the actual world which we refer to as α.

A possible world must have one and only value for each variable. If a contradiction is found then the possible world does not exist.

A possible world may have sub worlds grouped as Possible World Sets.

[edit] Possible World Set

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

if X\in S \and Y\in S then X\cap Y is empty.
P = {\bigcup_{s\in S} s}\!

[edit] Value Set

A Value Set is a set of tagged values. A tagged value is defined by the operator ::

a = a_v :: a_p\!

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

Value Sets arise naturally as the solutions of some kinds of equations,

x2 = 4

also types with a finite set of values may be treated as value sets. Having obtained value sets we need rules for combining the results of value sets.

[edit] Functions of a Value Set

Suppose f is a function on a type T. We want to extend this definition to apply to value sets of type T also.

If we allow polymorphic functions polymorphic then we can also define,

The following definition defines the function on a value set of a type using the function of the type.

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

[edit] Function of multiple Parameters

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

If currying is allowed,

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

The following defintion may then be used,

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

F(X) = \{f\in F, x\in X: f_v(x_v)::f_p\cap x_p\}\!
[edit] Function of two parameters
g(X, Y) = g_{curry}(X)(Y) = \{x\in X: g_{curry}(x_v)::x_p\}(y)\!

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

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

or,

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

The result can be extended to more parameters.

[edit] Meta Mathematics

We want to write a program that implements Constraint Logic Programming. Before we write such a program we would like to describe its behaviour in the language of mathematics. This is mathematics about mathematics, or Meta-Mathematics.

To do this we need to be able to treat the target mathematics as data to be described by the rules in the meta mathematics. But for clarity we would like this mathematical data to look like mathematics. We want the data describing the target mathematics to be represented syntactically like mathemematics.

[edit] Data

We add a special function data that takes a mathematical expression as a parameter. This construct means the data describing the mathematical expression. For example,

data(5 * 6)\!

Is the data descibing the application of the operator * to the values 5 and 6. It is not the same as the value returned by the function. So it is distinct from,

data(30)\!

"data" is a special function because is role is to change the meaning of text that appears for the parameter. The text within, although looking like mathematics, represents data structures describing the mathematics, not the results of the mathematical calculations.

[edit] Meta

We will be writing functions, in the meta mathematics that transform the data. In order to do this it helps to be able to use values from the meta mathematics within the data. This is achieved using the special function "meta".

For example we may want to describe the evaluation of x * y by an evaluation function,

\forall x, y \in \mathbb{R} : eval(data(meta(x) * meta(y)) = x * y

[edit] Meta Types

In writing meta programs it helps to have some standard types;

Note that although the use of infix operators and other syntactic devices is usefull to the human reader, to the computer it is just noise. So,

5 + 6 = + (5,6)

and more importantly,

\exists f \in function, x, y \in expression : data(meta(f)(meta(x), meta(y)) = data(5 + 6)\!

binds

[edit] Currying

Currying of functions may be performed which means that,

f(x,y) = fcurry(x)(y)

This means that,

\exists f \in call, v \in variable : data(meta(f)(meta(v))) = data(f(x, y))\!

binds,

This is useful because it allows us to write meta expressions that breakdown functions of multiple parameters into functions or one parameter. Each parameter can then have rules applied to it.

[edit] Transformations of Mathematics

We wish to transform target mathematics,

[edit] Breaking up Compound Expressions

The Expression Breakdown Structure (EBS) is a triple,

\forall y\in EBS : y = (y_v, y_c, y_s)\!

The CLP function breaks up compound function calls into individual function calls linked by variables.

\forall f \in function : CLP((v, f, s)) = (v, f, s) \!
\forall f \in function, x \in variable : CLP((v, data(meta(f)(meta(x))), s)) = (v, data(meta(f)(meta(x))), s) \!
\forall f \in call, c \in call: \exists y, z \in EBS : \!
CLP((v, data(meta(f)(meta(c))), s)) = (y_v.next(), data(meta(z_f)(meta(y_v.var()))), \{ data(meta(y_v.var()) = meta(y_c))\} \cap meta(y_s)) \!
\and \ y = CLP((z_v, c, z_s)) \!
\and \ z = CLP((v, f, s)) \!

[edit] Calculating Requested Unknown Variable

[edit] Evaluation Strategy

Retrieved from "http://knowino.org/wiki/User:Thepigdog/Constraint_Logic_Programming_Theory"
Personal tools
Namespaces
Variants
Actions
Navigation
Community
Toolbox