Concurrent Distinct Choices
August 2002
Introduction
An injective finite mapping is an abstraction common to
many programs.
This page shows the design of an injective finite mapping
and its implementation in
Curry,
a functional logic language.
Functional logic programming supports the
concurrent asynchronous execution of distinct portions
of a program---a condition that prevents passing from one
portion to another
the structure containing a partially constructed mapping to
ensure that a new choice does not violate the injectivity condition.
The following annotated links show programs using the
proposed implementation of an injective finite mapping.
Application
The example programs solve cryptarithms.
A cryptarithm is ``an arithmetic problem in which letters
have been substituted for numbers and which is solved by finding
all possible pairings of digits with letters that produce a
numerically correct answer.''
A convention of the problem is that different letters stand
for different digits.
This means that the mapping from letters to digits is injective.
A well-known example of cryptarithm and its solution are:
SEND + MORE = MONEY
9567 + 1085 = 10652 |
The following links include a program for this problem and three
variations for the following problem:
that has 130 distinct solutions.
Design
A mapping is a (total) function from a set
of indices to a set of values.
The type of both the indices and the values is arbitrary.
The mapping is represented as a list referred to as the store.
The store is indexed by the values of the problem.
In the particular case of cryptarithms,
this indexing is natural and straightforward since
the values are the digits 0,1,...9.
Initially, the elements of the store are free variables.
The elements in the store are referred to as tokens.
Putting a token into the store
represents the action of choosing a value that must be
different from the value of any other choice.
Often, it is convenient to represent
the tokens with the indices of the problem.
In the particular case of SEND+MORE=MONEY
we choose the characters S, E, N...
as the tokens.
Thus, the indexes and values of a problem
are used as values and indexes respectively, in the store,
i.e., the roles they have in the problem is reversed in the store.
The injectivity requirement is intended to prevent the condition
in which two distinct indices are mapped to the same value.
Every time an index of the problem
is mapped to a value, the program attempts to unify
the value with the variable of the store associated to the index.
If the variable is already bound to a different value,
the unification fails and the failure prevents the condition that
we want to prevent.
There are several options for the representation of the store.
In particular, the store can be initially represented with a list
of free variables, or with a single free variable, or with a tree-like
data structure. These variations are shown in the programs below.
Implementation
-
send-more.curry
This implementation initializes the store with a list of free variables.
-
too-much-1.curry
This implementation initializes the store with a list of free variables.
-
too-much-2.curry
This implementation initializes the store with a single free variable.
-
too-much-3.curry
This implementation initializes the store with a tree-like structure
containing pairs consisting of digits and free variables.
References
The following
paper, in PDF format, describes in detail the technique
addressed by this page.