the proceedings contain 21 papers. the special focus in this conference is on logic, functional-logicprogramming, Applications, Program Analysis, Rewriting and Semantics. the topics include: A brief survey of quantum...
ISBN:
(纸本)354021402X
the proceedings contain 21 papers. the special focus in this conference is on logic, functional-logicprogramming, Applications, Program Analysis, Rewriting and Semantics. the topics include: A brief survey of quantum programming languages;analysis of synchronous and asynchronous cellular automata using abstraction by temporal logic;online justification for tabled logic programs;a declarative debugging tool for functionallogic languages;an effective self-applicable partial evaluator for prolog;multivariant non failure analysis via standard abstract interpretation;implementing natural rewriting and narrowing efficiently;complete axiomatization of an algebraic construction of graphs;semantics of linear continuation-passing in call-by-name;basic pattern matching calculi and derivation of deterministic inverse programs based on LR parsing.
In previous work we have presented lang-n-play, a functional language-oriented programming language with languages as first-class-citizens. Language definitions can be bound to variables, passed to and returned by fun...
详细信息
ISBN:
(纸本)9783030590246;9783030590253
In previous work we have presented lang-n-play, a functional language-oriented programming language with languages as first-class-citizens. Language definitions can be bound to variables, passed to and returned by functions, and can be modified at run-time before being used. lang-n-play programs are compiled and executed in the higher-order logicprogramming ***. In this paper, we describe our compilation methods, which highlight how the distinctive features of higher-order logicprogramming are a great fit in implementing a language-oriented programming language.
In this paper, we provide direct encodings into Horn sequents of Multiplicative Linear logic for two NP-complete problems, 3D MATCHING and PARTITION. their correctness proofs are given by using a characterization of m...
详细信息
ISBN:
(数字)9783319906867
ISBN:
(纸本)9783319906867;9783319906850
In this paper, we provide direct encodings into Horn sequents of Multiplicative Linear logic for two NP-complete problems, 3D MATCHING and PARTITION. their correctness proofs are given by using a characterization of multiplicative proof nets.
the question of what constraints must hold for a predicate to behave as a ( partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining...
详细信息
ISBN:
(纸本)9783642298226
the question of what constraints must hold for a predicate to behave as a ( partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. the latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. this paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logicprogramming, the method might well also find application in reasoning about type classes.
While there has been much cross-fertilization between functional and logicprogramming-e.g., leading to functional models of many Prolog features-this appears to be much less the case regarding probabilistic programmi...
详细信息
ISBN:
(数字)9783030994617
ISBN:
(纸本)9783030994600;9783030994617
While there has been much cross-fertilization between functional and logicprogramming-e.g., leading to functional models of many Prolog features-this appears to be much less the case regarding probabilistic programming, even though this is an area of mutual interest. Whereas functionalprogramming often focuses on modeling probabilistic processes, logicprogramming typically focuses on modeling possible worlds. these worlds are made up of facts that each carry a probability and together give rise to a distribution semantics. the latter approach appears to be little-known in the functionalprogramming community. this paper aims to remedy this situation by presenting a functional account of the distribution semantics of probabilistic logicprogrammingthat is based on possible worlds. We present a term monad for the monadic syntax of queries together with a natural interpretation in terms of boolean algebras. then we explain that, because probabilities do not form a boolean algebra, they-and other interpretations in terms of commutative semirings-can only be computed after query normalisation to deterministic, decomposable negation normal form (d-DNNF). While computing the possible worlds readily gives such a normal form, it suffers from exponential blow-up. Using heuristic algorithms yields much better results in practice.
Various program verification problems for functional programs can be reduced to the validity checking problem for formulas of a fixpoint logic. Recently, Kobayashi et al. have shown that the unfold/fold transformation...
详细信息
ISBN:
(数字)9783030994617
ISBN:
(纸本)9783030994600;9783030994617
Various program verification problems for functional programs can be reduced to the validity checking problem for formulas of a fixpoint logic. Recently, Kobayashi et al. have shown that the unfold/fold transformation originally developed for logicprogramming can be extended and applied to prove the validity of fixpoint logic formulas. In the present paper, we refine their unfold/fold transformation, so that each predicate can be unfolded a different number of times in an asynchronous manner. Inspired by the work of Lee et al. on size change termination, we use a variant of size change graphs to find an appropriate number of unfoldings of each predicate. We have implemented an unfold/fold transformation tool based on the proposed method, and evaluated its effectiveness.
the verification framework PPV (Probabilistic Program Verification) verifies functional probabilistic programs supporting higher-order functions, continuous distributions, and conditional inference. PPV is based on th...
详细信息
ISBN:
(数字)9783030994617
ISBN:
(纸本)9783030994600;9783030994617
the verification framework PPV (Probabilistic Program Verification) verifies functional probabilistic programs supporting higher-order functions, continuous distributions, and conditional inference. PPV is based on the theory of quasi-Borel spaces which is introduced to give a semantics of higher-order probabilistic programming languages with continuous distributions. In this paper, we formalize a theory of quasi-Borel spaces and a core part of PPV in Isabelle/HOL. We first construct a probability monad on quasi-Borel spaces based on the Giry monad in the Isabelle/HOL library. Our formalization of PPV is extended so that integrability of functions can be discussed formally. Finally, we prove integrability and convergence of the Monte Carlo approximation in our mechanized PPV.
the generation of comprehensible explanations is an essential feature of modern artificial intelligence systems. In this work, we consider probabilistic logicprogramming, an extension of logicprogramming which can b...
详细信息
ISBN:
(数字)9783030994617
ISBN:
(纸本)9783030994600;9783030994617
the generation of comprehensible explanations is an essential feature of modern artificial intelligence systems. In this work, we consider probabilistic logicprogramming, an extension of logicprogramming which can be useful to model domains with relational structure and uncertainty. Essentially, a program specifies a probability distribution over possible worlds (i.e., sets of facts). the notion of explanation is typically associated withthat of a world, so that one often looks for the most probable world as well as for the worlds where the query is true. Unfortunately, such explanations exhibit no causal structure. In particular, the chain of inferences required for a specific prediction (represented by a query) is not shown. In this paper, we propose a novel approach where explanations are represented as programs that are generated from a given query by a number of unfolding-like transformations. Here, the chain of inferences that proves a given query is made explicit. Furthermore, the generated explanations are minimal (i.e., contain no irrelevant information) and can be parameterized w.r.t. a specification of visible predicates, so that the user may hide uninteresting details from explanations.
A distinguishing feature of logic and functionallogic languages is their ability to perform computations with partial data and to search for solutions of a goal. Having a built-in search strategy is convenient but no...
详细信息
ISBN:
(纸本)354066677X
A distinguishing feature of logic and functionallogic languages is their ability to perform computations with partial data and to search for solutions of a goal. Having a built-in search strategy is convenient but not always sufficient. For many practical applications the built-in search strategy (usually depth-first search via global backtracking) is not well suited. Also the non-deterministic instantiation of unbound logic variables conflicts withthe monadic I/O concept, which requires a single-threaded use of the world. A solution to these problems is to encapsulate search via a primitive operator try, which returns all possible solutions to a search goal in a list. In the present paper we develop an abstract machine that aims at an efficient implementation of encapsulated search in a lazy functionallogic language.
暂无评论