Semantic Determinism and Functional Logic Program Properties
| Autor: | José Miguel Cleva, Francisco Javier López-Fraguas |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
General Computer Science
Programming language Functional logic programming Computational logic functional-logic programming computer.software_genre Mathematical proof Determinism Theoretical Computer Science Logical framework program properties TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Philosophy of logic Computer Science::Logic in Computer Science Computer Science::Programming Languages Dynamic logic (modal logic) computer semantic determinism Logic programming Computer Science(all) Mathematics |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 174:3-15 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2006.10.018 |
| Popis: | In modern functional logic languages like Curry or Toy, programs are possibly non-confluent and non-terminating rewrite systems, defining possibly non-deterministic non-strict functions. Therefore, equational reasoning is not valid for deriving properties of such programs. In a previous work we showed how a mapping from CRWL –a well known logical framework for functional logic programming– into logic programming could be in principle used as logical conceptual tool for proving properties of functional logic programs. A severe problem faced in practice is that simple properties, even if they do not involve non-determinism, require difficult proofs when compared to those obtained using equational specifications and methods. In this work we improve our approach by taking into account determinism of (part of) the considered programs. This results in significant shortenings of proofs when we put in practice our methods using standard systems supporting equational reasoning like, e.g., Isabelle. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect