User loginNavigation 
Pure, Declarative, and Constructive Arithmetic Relations
Pure, Declarative, and Constructive Arithmetic Relations. Oleg Kiselyov, William E. Byrd, Daniel P. Friedman, and Chungchieh Shan. FLOPS 2008. (source code)
We present decidable logic programs for addition, multiplication, division with remainder, exponentiation, and logarithm with remainder over the unbounded domain of natural numbers. Our predicates represent relations without mode restrictions or annotations. They are fully decidable under the common, DFSlike, SLD resolution strategy of Prolog or under an interleaving refinement of DFS... So you've read The Reasoned Schemer and were excited about the fact that unlike the builtin operations in Prolog, arithmetic relations (over binary numbers) were fully implemented. For example, addition could also be used for subtraction and multiplication for factoring numbers and for generating all triples of numbers related by multiplication. Now comes this paper to explain the motivation behind some of the more arcane definitions needed to implement arithmetic in a fully relational style, and to prove their properties formally. The paper develops unary and binary arithmetic relations in pure Prolog (with no cuts, negation or introspection). LtU readers will also be interested in yet another embedding of pure Prolog into Haskell, that the authors offer. It is not meant to be the most optimal or convenient Prolog implementation (it wasn't even intended to be an implementation of a logic system). It was explicitly designed to be easier to reason about and so help prove certain properties of SLD or similar evaluation strategies. The main difference of DefinitionTree from other embeddings of Prolog in Haskell has to do with the generation of fresh names for logic variables. In DefinitionTree, name generation is not an effect, and the naming is fully decoupled from the evaluation. The evaluation no longer needs to carry a state for the generation of fresh names, hence the evaluator is easier to reason about equationally. 
Browse archivesActive forum topics

Recent comments
1 week 4 days ago
2 weeks 1 day ago
2 weeks 2 days ago
2 weeks 2 days ago
3 weeks 1 day ago
3 weeks 4 days ago
3 weeks 4 days ago
3 weeks 4 days ago
4 weeks 6 days ago
5 weeks 22 hours ago