Skip to content

chikamichi/amb

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

26 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

This gem is a compilation of several implementations of the ambiguous function/operator pattern, a computation tool useful for constraint programming and constraint satisfaction problems solving.

This little gem currently focuses on implementing backtracking, which is "a general algorithm for finding all (or some) solutions to some computational problem, that incrementally builds candidates to the solutions, and abandons each partial candidate c ("backtracks") as soon as it determines that c cannot possibly be completed to a valid solution." (:en)

Need some examples? Have you ever wanted to:

  • write a straightforward parser?
  • solve crosswords, sudokus or the n-queens problem?
  • design an equation-solver or a modelizer?
  • understand how logic programming languages (Prolog…) work?

Them amb may be of some interest to you.

Synopsis

You may want to jump straight to the Examples section if formal stuff annoys you.

Ambiguous functions were defined in John McCarty's 1963 paper A basis for a mathematical theory of computation. They allow for writing nondeterministic programs which contain various alternatives for the program flow.

Typically, the programmer would specify a limited number of alternatives (eg. different values for a variable), so that the program must later choose between them at runtime to find which one(s) are valid predicates to solve the issue at stake. The "issue" is often formalized as a constraint or a set of constraints referencing the variables some alternatives have been provided for. The evaluation may result in the discovery of dead ends, in which case it must "switch" to a previous branching point and start over with a different alternative.

To discover which alternatives groups are valid, a check/discard/switch strategy must be enforced by the program. Most often it will make use of a ambiguous operator, amb() which implements this strategy. Quoting Dorai Sitaram, "amb takes zero or more expressions, and makes a nondeterministic (or "ambiguous") choice among them, preferring those choices that cause the program to converge meaningfully". The most basic version of amb would be amb(x,y), which returns, in an unpredictible way, either x or y when both are defined; if only one is defined, whichever is defined; and terminate the program if none is defined. Using some recursivity, amb() may be used to define arbitrary, complex ambiguous functions. It is quite difficult to implement a good amb() operator matching that formal definition though (for unpredictability is not what computers enjoys doing). A simpler (yet functional) version has the operator return its first defined argument, then pass over the next defined one in case of a dead-end, in a depth-first selection algorithm. It is dumb yet it works as expected.

Thus the most common strategy used for implementing amb()'s logic (check/discard) is chronological backtracking. It is kind of a brute-force, linear approach, which always relies on some sort of continuations (call/cc). A continuation is like a savepoint, representing "what's left to run" at a given time. Recording as much continuations as alternatives enables amb to test "the rest of the program" multiple times until a valid solution is found. This rather dumb algorithm may be tweaked into a (not so) smarter backjumping algorithm for more efficiency, depending on the nature of the problem at stake. Another strategy is reinforcement learning (aka. constraint learning), as used in some AI systems. Most of the time it's really hard. This library implements simple backtracking only.

More details on all of this under the doc/ folder (pending).

Examples

# Amb is a module
A = Class.new { include Amb }.new

x = A.choose(1,2,3,4) # register each alternative as a backtrack point
y = A.choose(1,2,3,4) # same for y, so we have 16 backtracking branches

puts "examining x = #{x}, y = #{y}"

# assertions will backtrack if a dead-end is discovered
A.assert x + y == 5
A.assert x - y == 1
#A.assert x == 2    # if this line is uncommented, then no solution can be found
                    # and the program raises a Amb::ExhaustedError

puts "> solution: x = #{x}, y = #{y}"

will produce:

examining x = 1, y = 1
examining x = 1, y = 2
examining x = 1, y = 3
examining x = 1, y = 4
examining x = 2, y = 1
examining x = 2, y = 2
examining x = 2, y = 3
examining x = 2, y = 4
examining x = 3, y = 1
examining x = 3, y = 2
solution: x = 3, y = 2

This illustrates the incremental, backtracking pattern leading to the first valid solution.

Many more examples under the examples/ directory. You may run them with the -d flag to output information about the solving process.

Installation

gem install amb

Step by step

Here's a raw use-case, presenting the required steps. For concrete examples, see the examples/ directory.

First, require the lib:

require 'amb'

# one may either use the Amb module (Amb.choose…) or create a proxy class.
class Ambiguous
  include Amb
  # opportunity to log & the like here
end

amb = Ambiguous.new

Then, define your alternatives using #choose (aliased as #choices or #alternatives). It may take arbitrary code (values, proc…). Don't forget to assign it to a variable, otherwise it is just useless alternatives. Most of the time, several alternatives set will be defined.

x = amb.choose(1, 2, lambda { some code})
y = amb.choose(:some, :more, :alternatives)

Then, state at least one constraint which, hopefully, references your alternatives. If more than one constraint is expressed, all of them will be considered in the problem solving.

amb.assert(x != y)
amb.assert heavy_logical_computation_on(x, y)

And so on. Once again, for real use-cases, see the examples/ directory.

TODO

  • more examples!
  • more specs!
  • spec out choose depending on a previous choose
  • implements a version of amb matching the original definition (returns one of its argument at random) => keep track of backtracking paths
  • implements a trampoline version (continuation-passing style)
  • memoization/reset?
  • a different selection algo? (BFS, smarter one)

See also

  • doc/ and examples/ directories.
  • Continuations and fibers concepts.