The Structure of the System
CFLP is a distributed software system for solving systems of equational goals in theories that can be represented as sets
of conditional rewrite rules over a term algebra whose signature is extended with external operators. The external operators
are used for expressing constraints over various domains.
The general architecture of the system is depicted below.
Figure 1. The architecture of CFLP.
The CFLP interpreter is designed to solve systems of equations between simply-typed -terms in theories axiomatized by finite sets of conditional rewrite rules of a certain kind, called pattern rewrite rules.
Roughly speaking, simply-typed -terms are analogous to the
2. Each such construct (which we will henceforth call a -term) should be well-typed, that is, a type can be inferred from the types of its base components (variables, constants, and function symbols).
The current version of CFLP recognizes the following base types:
and the following constructed types:
For lists, we have adopted both the Mathematica notation
The CFLP interpreter is based on a higher-order lazy narrowing calculus C for pattern rewrite systems  extended to handle also conditional pattern rewrite systems . The underlying calculus essentially consists of the unification rules of higher-order patterns  and the lazy narrowing rules. Since the search space of such a calculus is extremely large, we have implemented a couple of refinements with smaller search space for solutions, which are sound and complete for classes of functional logic programs and of practical interest.
We have extended these calculi in two main directions:1. the possibility to specify constraints, that is, equations that cannot be solved by narrowing, but for which specialized solvers are available; and
2. the possibility to specify explicit OR-parallelism.
The interpreter successively decomposes the goal toward an answer substitution by applying the inference steps of the underlying lazy narrowing calculus. The only equations that cannot be solved in this way are the constraints. The constraints generated upon derivations are collected and sent to be solved by specialized constraint solvers via the component called the scheduler (see Figure 1).
Note that the nondeterministic selection of a rewrite rule for a defined symbol and the explicit OR-formulas cause the initial goal to be reduced to disjoint sets of constraints that can be solved in parallel. Thus, in the last illustrative example, the reduction of the initial goal
involves the decomposition of the equation into simpler equations. The transformation step performed by our lazy narrowing calculus is
where X0, Y0 are new variables. In this step we have used the fresh variant
of the rewrite rule which defines f.
During step (2), an OR-subgoal is produced and as a result the initial goal is finally decomposed into two disjoint sets of constraints. These sets of constraints are sent to be solved to the scheduler.
The scheduler coordinates the process of solving the systems of constraints received from the interpreter. In order to solve these sets of constraints, the constraint scheduler maintains a dynamic data structure called a constraint tree. The nodes of the constraint tree are pairs of the form where is a substitution and cs is a set of constraints.
Whenever a set of constraints cs is received from the interpreter, the scheduler adds a new son to the root of the constraint tree. Here stands for the empty substitution. The scheduler expands this tree by applying constraint-solving methods in parallel to its leaf nodes.
A leaf node is expanded with respect to a method m as follows.1. cs is decomposed into a set of constraints to which method m can be applied, and a set of other constraints.
2. is sent to be solved to a constraint solver which implements method m. We call such a solver an m-solver.
3. If the m-solver detects inconsistent, then the node is marked as inconsistent. Otherwise the m-solver returns if it cannot reduce , or it computes a finite sequence of pairs with the property that is a solution of cs if and only if there exists a solution of some , such that .
4. If the sequence is computed by the m-solver, then the nodes are added to the constraint tree as sons of the node .
A node is final if it cannot be reduced by any m-solver which is available.
The implementation of the scheduling algorithm is inspired by the work of Hong . The scheduler can be regarded as a component parameterized with a list of constraint-solving methods. The scheduler implements a cooperation strategy S, which repeatedly applies the sequence of methods to the leaves of the constraint tree until they become either final or inconsistent. As soon as a final node is generated, it is made accessible to the interpreter.
The Constraint Solvers
The constraint solvers are implementations of the constraint-solving methods specified to the scheduler through the list M. The current implementation of CFLP provides constraint solvers, which implement the following methods for solving constraints over the domains of real and complex numbers.
These methods are tried in the order presented.
All solvers are implemented by separate Mathematica processes executing in parallel and communicating with the constraint scheduler via MathLink connections. There are two types of constraint solvers in CFLP.1. Local constraint solvers that run as subsidiary Mathematica processes of the CFLP constraint scheduler.
2. Shared constraint solvers are started from outside a CFLP session and can be connected later to more CFLP schedulers, which may run on a different machine.
The user can adjust the distributed constraint-solving component of the system by specifying the number of local constraint solvers that are started at system initialization, and the remote machines on which to look for shared constraint solvers.
The communication mechanism between scheduler and constraint solvers is implemented completely in MathLink . Therefore, CFLP is a platform-independent software system and can be used in heterogeneous networks.
Copyright © 2001 Wolfram Media, Inc. All rights reserved.