Algorithmic debugging is a debugging technique that has been extended to practically all programming paradigms. It is based on the answers of the programmer to a series of questions generated automatically by the algo...
详细信息
ISBN:
(纸本)9783540714095
Algorithmic debugging is a debugging technique that has been extended to practically all programming paradigms. It is based on the answers of the programmer to a series of questions generated automatically by the algorithmic debugger. therefore, the performance of the technique is strongly dependent on the number and the complexity of these questions. In this work we overview and compare current strategies for algorithmic debugging and we introduce some new strategies and discuss their advantages over previous approaches.
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number ...
详细信息
ISBN:
(纸本)3540266550
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem term enumeration,. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a proof enumeration problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. this in turn yields a proof enumeration algorithm.
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logicprogramming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for t...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logicprogramming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of programtransformationthat allows to transform logicprograms in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.
We propose a new grouping operator for logicprograms based on the bag of predicate. the novelty of our proposal lies in the use of modes, which allows us to prove properties regarding groundness of computed answer su...
详细信息
ISBN:
(纸本)9783642125911
We propose a new grouping operator for logicprograms based on the bag of predicate. the novelty of our proposal lies in the use of modes, which allows us to prove properties regarding groundness of computed answer substitutions and termination. Moreover, modes allow us to define a somewhat declarative semantics for it and to relax some rather unpractical constraints on variable occurrences while retaining a straightforward semantics.
In this paper, we present an approach to non-termination of term rewriting systems inspired by a technique that was designed in the context of logic, programming. Our method is based on a classical unfolding operation...
详细信息
ISBN:
(纸本)9783540714095
In this paper, we present an approach to non-termination of term rewriting systems inspired by a technique that was designed in the context of logic, programming. Our method is based on a classical unfolding operation together with semi-unification and is independent of a particular reduction strategy. We also describe a technique to reduce the explosion of rules caused by the unfolding process. the analyser that we have implemented is able to solve most of the non-terminating examples in the Termination Problem Data Base.
this paper introduces a modular framework for termination analysis of logicprogramming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the log...
详细信息
ISBN:
(纸本)9783540787686
this paper introduces a modular framework for termination analysis of logicprogramming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the logicprogramming domain. the main idea of the approach is that termination conditions for a program are established based on the decomposition of its dependency graph into its strongly connected components. these conditions can then be analysed separately by possibly different well-founded orders. We propose a constraint-based approach for automating the framework. then, for example, termination techniques based on polynomial interpretations can be plugged in as a component to generate well-founded orders.
Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synthesis of a programthe type of which ...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synthesis of a programthe type of which is a given formula. We present a model of automata that can handle proof construction in full intuitionistic first-order logic. the automata are constructed in such a way that any successful run corresponds directly to a normal proof in the logic. this makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections withthe traditional logical connectives.
this book constitutes the thoroughly refereed post-conference proceedings of the 24thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2014, held in Canterbury, UK, in September 2014...
详细信息
ISBN:
(数字)9783319178226
ISBN:
(纸本)9783319178219
this book constitutes the thoroughly refereed post-conference proceedings of the 24thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2014, held in Canterbury, UK, in September 2014. the 18 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 34 submissions. the aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-basedprogram development. the papers are organized along a set of thematic tracks: program analysis and transformation, constraint handling rules, termination analysis, security, program testing and verification, programsynthesis, program derivation, semantic issues in logicprogramming and programtransformation and optimization.
Higher-order logicprogramming is an interesting extension of traditional logicprogramming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order charact...
详细信息
ISBN:
(纸本)9783030138387;9783030138370
Higher-order logicprogramming is an interesting extension of traditional logicprogramming that allows predicates to appear as arguments and variables to be used where predicates typically occur. Higher-order characteristics are indeed desirable but on the other hand they are also usually more expensive to support. In this paper we propose a program specialization technique based on partial evaluation that can be applied to a modest but useful class of higher-order logicprograms and can transform them into first-order programs without introducing additional data structures. the resulting first-order programs can be executed by conventional logicprogramming interpreters and benefit from other optimizations that might be available. We provide an implementation and experimental results that suggest the efficiency of the transformation.
We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum, count, findall, and min. this new feature significantly improves the conciseness and expressiveness of the language. In this pape...
详细信息
ISBN:
(纸本)9783540787686
We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum, count, findall, and min. this new feature significantly improves the conciseness and expressiveness of the language. In this paper, we describe an implementation based on source-to-source transformations to CHR (extended with some low-level compiler directives). We allow user-defined aggregates and nested aggregate expressions over arbitrary guarded conjunctions of constraints. Both an on-demand and an incremental aggregate computation strategy are supported.
暂无评论