bagofN
!, var/1, or other non-logical operators. The purity and minimalism of our approach allows us to declare arithmetic in other logic systems, such as Haskell type classes.
To prove decidability, correctness and other properties of our predicates we have developed a new semantics of normal logic programs: solution sets. Unlike dominant model-theoretic semantics, ours is operational, proof-theoretic. It is more abstract than the partial-trace semantics.
We emphasize two premises of the paper. First, writing all-mode arithmetic relations is, in general, straightforward: with var/1 we determine which of the arguments of, say, the add predicate are instantiated, and so use addition, subtraction, or numeral generation as appropriate. We may chose to propagate the addition constraint or to residualize. There is a good reason however why the use of var/1 is discouraged. In our paper, we specifically disavowed var/1, negation or other such (reflective) facilities. We deliberately limited ourselves to Horn clauses, and nothing else. Theorem provers and constraint solvers certainly offer very sophisticated procedures for solving arithmetic constraints. In any such procedures, to my knowledge, we must know where all our variables are. But in our paper, we specifically do not. We have no idea which arguments of our goals are or contain variables, and we cannot tell. We disclaim any and all intensional analysis, just so we could see how much we can do without.
Our use of SLD resolution and its simple variants -- as widely implemented and quite efficient -- was another self-imposed restriction. One may quite rightfully say that we deliberately painted ourselves into the corner. On the other hand, purity and minimalism, however difficult to live with, often offer deep and general insights.
In contrast to Presburger arithmetic, which can decide arbitrary formulas within its domain, we can fully decide only base predicates -- addition, multiplication, etc. -- but not their conjunctions, or conjunctions with equality. Conjunctions of the base predicates let us express arbitrary Diofantine equations, which are not generally decidable. Technically, after a base goal succeeds, its arguments may share logic variables. Many of our termination theorems will not therefore apply to the second goal in a conjunction. It appears that some (if not many or all) cases of divergence due to the sharing of logic variables in the arguments of a goal could be prevented by tabling. Investigating the evaluation strategy of the XSB system is future work. Also part of the future work is the evaluation of principled ways of introducing negation, e.g., as done in lambda-Prolog.
The goal of this project was not to be useful but to be insightful. Quite surprisingly to us, a similar development for Curry proved to be practically useful and has become part of a Haskell Curry implementation.
Joint work with William E. Byrd, Daniel P. Friedman, and Chung-chieh Shan.
Chung-chieh Shan. Slides of the talk at FLOPS08, April 14, 2008.
< http://www.cs.rutgers.edu/~ccshan/arithm/talk.pdf >
unary.prl [9K]
Warm-up: a stepwise development of addition and multiplication of unary numbers
pure-bin-arithm.prl [41K]
Extensively commented source code, with termination proofs
DefinitionTree.hs [14K]
Definitional trees, a model for reasoning about evaluation of normal logic programs
That file is a full-fledged Prolog interpreter in Haskell. The salient feature is the absence of name-generation effects. The evaluation strategy is no longer concerned with fresh name generation, and so is easier to reason about.
(exists U. [U,U]), and `common subexpression elimination' in logical programs. We draw parallels with effects, of creating logical variables.The miniKanren implementation uses higher-order abstract syntax, to avoid copy_term, and an advanced evaluator that removes the need for the explicit iterative deepening. The result is an even leaner prover.
Bernhard Beckert and Joachim Posegga. leanTAP: Lean Tableau-based Deduction. Journal of Automated Reasoning, 15(3), 339-358 (1995).
< http://citeseer.ist.psu.edu/beckert95leantap.html >
We describe the real-world deployment of Soutei into a publish-subscribe web service with distributed and compartmentalized administration, emphasizing the often overlooked aspect of authorizing the creation of resources and the corresponding policies.
Soutei brings Binder from a research prototype into the real world. Supporting large, truly distributed policies required non-trivial changes to Binder, in particular mode-restriction and goal-directed top-down evaluation. To improve the robustness of our evaluator, we describe a fair and terminating backtracking algorithm.
This is a joint work with Andrew Pimlott.
Soutei: syntax, semantics, and use cases
< http://www.metnet.navy.mil/Metcast/Auth-use-cases.html >
soutei-1.tar.gz [61K]
The first implementation of Soutei, in Scheme. Its compiles Soutei assertions into Kanren code. The code relies on Bigloo-specific module system and the built-in parser and lexer. The code can be compiled with Bigloo v2.4. It includes many built-in tests.
This source code is given here for information only. It is no longer used; it served as a model for the current, version 2 implementation, which is written in Haskell.
nat = {zero} + nat with the operation plusbtree = {integer} + (btree * btree)We then demonstrate simple deep copying of a binary tree with optional modifications.
Since all edges have the same weight, an edge between two vertices is the shortest path between these vertices. Thus to find shortest paths from a given vertex to the others we merely need to do a breadth-first search.
This Prolog code takes advantage of Prolog's built-in ``database'' to maintain the queue of vertices for the breadth-first graph traversal.
NxN chess board and a knight standing at pos(Row,Col), we should print out a sequence of knight's moves that pass through every cell on the board exactly once. The last cell of the tour may or may not be the same as the starting cell: the tour does not have to be closed.
The predicate knight_tour(N,Pos) tries to solve the open tour problem for the NxN board. The necessary condition for a solution is N*N-1 being divisible by three. Here is a sample run:
knight_tour(4,pos(0,1)).
found solution
Board of 4 dim
3: 8 7 6 5
2: 9 10 11 4
1: 14 13 12 3
0: 15 0 1 2
The number in a cell tells that cell's position in a tour: the tour starts at the cell marked 0 and continues to the cells marked 1, 2, 3...15.
The code can be modified to print out all closed tours starting from a given position -- not necessarily complete tours of the board. The latter may exist only if N is divisible by 3 and is at least 6.
The code demonstrates an implementation of matrices in Prolog, as lists of lists. The code shows off ``updating'' of matrix elements and undoing the ``updates'' on back-tracking. These updates are all functional rather than destructive.
A web site dedicated to various Knight Tour problems and solutions
< http://www.borderschess.org/KnightTour.htm >
N queens on a N-by-N chessboard such that no queen beats the others. This introductory Prolog code produces all permutation of a given list and prints those that correspond to a safe position of the N queens.oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML