The proceedings contain 10 papers. The special focus in this conference is on foundations of logic and functionalprogramming. The topics include: Typechecking dependent types and subtypes;reducing recursion to iterat...
ISBN:
(纸本)9783540191292
The proceedings contain 10 papers. The special focus in this conference is on foundations of logic and functionalprogramming. The topics include: Typechecking dependent types and subtypes;reducing recursion to iteration by means of pairs and N-tuples;unification revisited;rule rewriting methods for efficient implementations of horn logic;a completeness result for E-unification algorithms based on conditional narrowing;representing domain structure of many-sorted Prolog knowledge bases;horn: An inference engine prototype to implement intelligent systems;PAP: a logicprogramming system based on a constructive logic.
functional completeness of the combinatory logic means that every λ-expression may be translated into an equivalent combinator expression and this is the theoretical basis for the implementation of functional languag...
详细信息
functional completeness of the combinatory logic means that every λ-expression may be translated into an equivalent combinator expression and this is the theoretical basis for the implementation of functional languages on combinator-based abstract machines. To obtain efficient implementations it is important to distinguish between early and late binding times . i.e. to distinguish between compile-time and run-time computations. We therefore introduce a two-level version of the λ-calculus where this distinction is made in an explicit way. Turning to the combinatory logic we only wish to generate combinator-code for the run-timecomputations. The two-level version of the combinatory logic therefore will be a mixed λ-calculus and combinatory logic. A previous paper has shown that (a natural formulation of) the mixed λ-calculus and combinatory logic is not functionally complete but only corresponds to a strict subset of the two-level λ-calculus. In this paper we extend the mixed λ-calculus and combinatory logic with a new combinator, Ψ, and show that this suffices for the mixed λ-calculus and combinatory logic to be functionally complete. However, the new combinator may not always be implementable and we therefore discuss conditions under which it can be dispensed with.
Recent advances in the foundations and the implementations of functionallogicprogramming languages originate from far-reaching results on narrowing evaluation strategies. Narrowing is a computation similar to rewrit...
详细信息
Recent advances in the foundations and the implementations of functionallogicprogramming languages originate from far-reaching results on narrowing evaluation strategies. Narrowing is a computation similar to rewriting which yields substitutions in addition to normal forms. In functionallogicprogramming, the classes of rewrite systems to which narrowing is applied are, for the most part, subclasses of the constructor-based, possibly conditional, rewrite systems. Many interesting narrowing strategies, particularly for the smallest subclasses of the constructor-based rewrite systems, are generalizations of well-known rewrite strategies. However, some strategies for larger non-confluent subclasses have been developed just for functionallogic computations. This paper discusses the elements that play a relevant role in evaluation strategies for functionallogic computations, describes some important classes of rewrite systems that model functionallogic programs, shows examples of the differences in expressiveness provided by these classes, and reviews the characteristics of narrowing strategies proposed for each class of rewrite systems. (c) 2005 Elsevier Ltd. All rights reserved.
We study Girard's linear logic from the point of view of giving a concrete computational interpretation of the logic, based on the Curry-Howard isomorphism. In the case of Intuitionistic linear logic, this leads t...
详细信息
We study Girard's linear logic from the point of view of giving a concrete computational interpretation of the logic, based on the Curry-Howard isomorphism. In the case of Intuitionistic linear logic, this leads to a refinement of the lambda calculus, giving finer control over order of evaluation and storage allocation, while maintaining the logical content of programs as proofs, and computation as cut-elimination. In the classical case, it leads to a concurrent process paradigm with an operational semantics in the style of Berry and Boudol's chemical abstract machine. This opens up a promising new approach to the parallel implementation of functionalprogramming languages;and offers the prospect of typed concurrent programming in which correctness is guaranteed by the typing.
This volume consists of some of the papers that were delivered during the workshop on "foundations of logic and functionalprogramming" held in Trento, Italy, from December 15th to 19th, 1986. The meeting ce...
详细信息
ISBN:
(数字)9783540391265
ISBN:
(纸本)9783540191292
This volume consists of some of the papers that were delivered during the workshop on "foundations of logic and functionalprogramming" held in Trento, Italy, from December 15th to 19th, 1986. The meeting centered on themes and trends in functionalprogramming and in logicprogramming. This book contains five papers contributed by the invited speakers and five selected contributions.
This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functionalprogramming l...
详细信息
ISBN:
(纸本)9781450302555
This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functionalprogramming language Haskell, which (1) optimally plays sequential games, (2) implements a computational version of the Tychonoff Theorem from topology, and (3) realizes the Double-Negation Shift from logic and proof theory. The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad. In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here).
This volume contains papers presented at the secondinternational workshop on extensions of logicprogramming,which was held at the Swedish Institute of Computer Science,Stockhom, January 27-29, 1991.The 12 papers ...
详细信息
ISBN:
(数字)9783540471141
ISBN:
(纸本)9783540554981
This volume contains papers presented at the second
international workshop on extensions of logicprogramming,
which was held at the Swedish Institute of Computer Science,
Stockhom, January 27-29, 1991.
The 12 papers describe and discuss several approaches to
extensions of logicprogramming languages such as PROLOG, as
well as connections between logicprogramming and functionalprogramming, theoretical foundations of extensions,
applications, and programming methodologies.
The first workshop in this series was held in T}bingen in
1989 and its proceedings areavailable as LNCS 475. The
third workshop will be held in Bologna in 1992.
Recent advances in the foundations and the development of functionallogicprogramming languages originate from far-reaching results on narrowing evaluation strategies. Narrowing is a computation similar to rewriting ...
详细信息
This issue contains 9 conference papers. The topics covered are: algebras, polynomials, and programs;functional polymorphism;fixed points in Cartesian closed categories;guarded theories;categorical fixed point semanti...
详细信息
This issue contains 9 conference papers. The topics covered are: algebras, polynomials, and programs;functional polymorphism;fixed points in Cartesian closed categories;guarded theories;categorical fixed point semantics;functional completeness of mixed lambda-calculus and combinatory logic;recursive programs and denotational semantics in absolute logics of programs;Scott's thesis for domains of information and well-quasi-orderings;generalization of the concept of sketch. All papers are separately indexed and abstracted.
暂无评论