| Logical and Computational Aspects of Programming with Sets/Bags/Lists (1991) | |||||||||||||||||
Abstract | |||||||||||||||||
| . We study issues that arise in programming with primitive recursion over non-free datatypes such as lists, bags and sets. Programs written in this style can lack a meaning in the sense that their outputs may be sensitive to the choice of input expression. We are, thus, naturally lead to a set-theoretic denotational semantics with partial functions. We set up a logic for reasoning about the definedness of terms and a deterministic and terminating evaluator. The logic is shown to be sound in the model, and its recursion free fragment is shown to be complete for proving definedness of recursion free programs. The logic is then shown to be as strong as the evaluator, and this implies that the evaluator is compatible with the provable equivalence between different set (or bag, or list) expressions . Oftentimes, the same non-free datatype may have different presentations, and it is not clear a priori whether programming and reasoning with the two presentations are equivalent. We formulate t... | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||