scholarly journals Logic programming, functional programming, and inductive definitions

2006 ◽  
pp. 283-309 ◽  
Author(s):  
Lawrence C. Paulson ◽  
Andrew W. Smith
Keyword(s):  
Logic Programming ◽  
Functional Programming ◽  
Inductive Definitions

scholarly journals Expanding Transformation: A Basis for Correctness Verification of Rewriting Rules

2007 ◽  
Vol 11 (5) ◽  
pp. 478-490 ◽  
Author(s):  
Ekawit Nantajeewarawat ◽  
◽  
Kiyoshi Akama ◽  
Hidekatsu Koike ◽  
◽  
...  
Keyword(s):  
Logic Programming ◽  
Functional Programming ◽  
Program Transformation ◽  
Basic Class ◽  
Problem Description ◽  
Programming Paradigms ◽  
Rewriting Rules

Unfolding transformation has long been used for computation and program transformation both in functional programming and logic programming paradigms. In this paper, we clarify that an unfolding step can be regarded as the composition of two simpler operations, i.e., expanding transformation and unification, and show that expanding transformation, rather than unfolding transformation, is a suitable basis for verifying the correctness of rewriting rules by pattern manipulation, which in turn provides a basis for systematically generating rewriting rules from a given problem description. We verify the correctness of expanding transformation and demonstrate the correctness of a basic class of rewriting rules, called general rewriting rules, based on expanding transformation. Applying expanding transformation and its correctness result, we demonstrate correctness verification of a larger class of rewriting rules, called expanding-based rewriting rules, by transformation of clause patterns.

A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language

2011 ◽  
Vol 76 (2) ◽  
pp. 673-699 ◽  
Author(s):  
Michael Gabbay
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Functional Programming ◽  
Order Logic ◽  
First Order Logic ◽  
Cut Elimination ◽  
Logic Programming Language ◽  
First Order ◽  
Functional Programming Language ◽  
Sequent System

AbstractWe build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic.We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

scholarly journals Escape from Zurg: an exercise in logic programming

2004 ◽  
Vol 14 (3) ◽  
pp. 253-261 ◽  
Author(s):  
MARTIN ERWIG
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Functional Programming ◽  
Search Problems ◽  
Functional Programming Languages ◽  
Widespread Belief

In this Pearl we illustrate with an example that modern functional programming languages like Haskell can be used effectively for programming search problems, in contrast to the widespread belief that Prolog is much better suited for tasks like these.

scholarly journals Default rules for Curry

2016 ◽  
Vol 17 (2) ◽  
pp. 121-147 ◽  
Author(s):  
SERGIO ANTOY ◽  
MICHAEL HANUS
Keyword(s):  
Logic Programming ◽  
Basic Concept ◽  
Functional Programming ◽  
Functional Languages ◽  
Logic Programs ◽  
The Core ◽  
Functional Logic Programming ◽  
Functional Logic ◽  
Default Rules

AbstractIn functional logic programs, rules are applicable independently of textual order, i.e., any rule can potentially be used to evaluate an expression. This is similar to logic languages and contrary to functional languages, e.g., Haskell enforces a strict sequential interpretation of rules. However, in some situations it is convenient to express alternatives by means of compact default rules. Although default rules are often used in functional programs, the non-deterministic nature of functional logic programs does not allow to directly transfer this concept from functional to functional logic languages in a meaningful way. In this paper, we propose a new concept of default rules for Curry that supports a programming style similar to functional programming while preserving the core properties of functional logic programming, i.e., completeness, non-determinism, and logic-oriented use of functions. We discuss the basic concept and propose an implementation which exploits advanced features of functional logic languages.

Contextual equivalence for inductive definitions with binders in higher order typed functional programming

2013 ◽  
Vol 23 (6) ◽  
pp. 658-700
Author(s):  
MATTHEW R. LAKIN ◽  
ANDREW M. PITTS
Keyword(s):  
Functional Programming ◽  
Operational Semantics ◽  
Higher Order ◽  
European Symposium ◽  
Proof Search ◽  
Inductive Definitions ◽  
University Of Cambridge ◽  
Meta Programming ◽  
Contextual Equivalence ◽  
Phd Thesis

AbstractCorrect handling of names and binders is an important issue in meta-programming. This paper presents an embedding of constraint logic programming into the αML functional programming language, which provides a provably correct means of implementing proof search computations over inductive definitions involving names and binders modulo α-equivalence. We show that the execution of proof search in the αML operational semantics is sound and complete with regard to the model-theoretic semantics of formulae, and develop a theory of contextual equivalence for the subclass of αML expressions which correspond to inductive definitions and formulae. In particular, we prove that αML expressions, which denote inductive definitions, are contextually equivalent precisely when those inductive definitions have the same model-theoretic semantics. This paper is a revised and extended version of the conference paper (Lakin, M. R. & Pitts, A. M. (2009) Resolving inductive definitions with binders in higher-order typed functional programming. InProceedings of the 18th European Symposium on Programming (ESOP 2009), Castagna, G. (ed), Lecture Notes in Computer Science, vol. 5502. Berlin, Germany: Springer-Verlag, pp. 47–61) and draws on material from the first author's PhD thesis (Lakin, M. R. (2010)An Executable Meta-Language for Inductive Definitions with Binders. University of Cambridge, UK).

scholarly journals Preface for special section from FLOPS 2014

2016 ◽  
Vol 26 ◽  
Author(s):  
MICHAEL CODISH ◽  
EIJIRO SUMII
Keyword(s):  
International Symposium ◽  
Logic Programming ◽  
Functional Programming ◽  
Special Section ◽  
Declarative Programming ◽  
Cross Fertilization

The 12th International Symposium on Functional and Logic Programming was held in Kanazawa, Japan, June 4–6, 2014. The aim of the Functional and Logic Programming series of conferences is to bring together researchers interested in declarative programming including functional programming and logic programming. The series aims to promote cross-fertilization and integration between the two paradigms and it is traditionally organized and held in Japan.

Sign in / Sign up

Export Citation Format

Share Document