Provides computer science students and researchers with a firm background in lambda-calculus and combinators.

Almost forty years ago Richard Montague proposed to analyse natural language with the same tools as formal languages. In particular, he gave formal semantic analyses of several interesting fragments of English in terms of typed logic. This led to the development of Montague grammar as a particular style of formal analysis of natural language.

We propose a rudimentary formal framework for reasoning about recursion equations over inductively generated data. Our formalism admits all equational programs , and yet singles out none. While being simple, this framework has numerous extensions and applications. Here we lay out the basic concepts and definitions; show that the deductive power of our formalism is similar to that of Peano's Arithmetic; prove a strong normalization theorem; and exhibit a mapping from natural deduction derivations to an applied λ -calculus, à la (...) Curry–Howard, which provides a transparent proof of Gödel's result that the provably recursive functions of PA are definable by primitive recursion in finite types. Also of interest is the extent, uncommon among similar constructions, to which our mapping is oblivious to first order terms, including first order quantification and equality. Additional applications and extensions of the method will be presented in sequel papers. In particular, the methodology introduced here lends itself to systematic links between natural sub-formalisms and computational complexity classes. Since these sub-formalisms are largely transparent, allowing one to reason formally in the full system while leaving to automatic software tools the task of verifying that restrictions are complied with, the framework is particularly attractive for the development of Feasible Mathematics. (shrink)

Epistemic logic is the logic of knowledge, and dynamic epistemic logic is the logic of effects of communicative actions on the knowledge states of a set of agents. Typical communicative actions are making public announcements, passing private messages, revealing secrets, telling lies. This paper takes its starting point from the version of dynamic epistemic logic of [3], and demonstrates a tool that can be used for showing what goes on during a series of epistemic updates: the dynamic epistemic modelling tool (...) DEMO [10]. DEMO allows modelling epistemic updates, graphical display of update results, graphical display of action models, formula evaluation in epistemic models, and translation of dynamic epistemic formulas to PDL [23] formulas. DEMO is written in Haskell. This paper intends to demonstrate its use for calculating and visualizing the model transformations that take place during epistemic updating. (shrink)

The Lisp programming language is often described as the first functional programming language and also as an important early AI language. In the history of functional programming, however, it occupies a rather anomalous position, as the circumstances of its development do not fit well with the widely accepted view that functional languages have been developed through a theoretically-inspired project of deriving practical programming languages from the lambda calculus. This paper examines the origins of (...) Lisp in the early AI programming work of the mid-to-late 1950s, and in particular in the work of Allen Newell, Cliff Shaw and Herbert Simon. Their 1956 program, the Logic Theory Machine, introduced new ideas about data and program structures that were articulated in response to perceived limitations in existing programming technique. Later writers, notably John Backus, have described these features as constituting a “programming language style” distinct from the traditional style that preceded it. The paper examines the origins of the earlier style in practices of manual computation, analyses the key technical differences between it and the style first manifested in the Logic Theory Machine, and concludes that programming practice and experience play a large and underappreciated role in the development of programming styles and languages. (shrink)

We show the adequacy of axioms and proof rules for strict and lazy functional programs. Our basic logic comprises a huge part of what is common to the two styles of functional programming. The logic for call-by-value is obtained by adding the axiom that says that all variables are defined, whereas the logic for call-by-name is obtained by adding the axiom that postulates the existence of an undefined object for each type. To show the correctness of the (...) axiomatization we do not use denotational semantics and the adequacy of the evaluation of programs with respect to the semantics. Instead we use the standard term models based on call-by-value and call-by-name evaluation. We introduce a new method to prove on the syntactical level the monotonicity of the evaluation of functional programs with unbounded recursion. The direct method yields results concerning the proof-theoretic strength of the axiomatization. As a side result we obtain a syntactical proof of the context lemma for simply typed lambda terms with recursion. (shrink)

An emerging standard for polymorphically typed, lazy, purely functional programming is Haskell, a language named after Haskell Curry. Haskell is based on (polymorphically typed) lambda calculus, which makes it an excellent tool for computational semantics.

This collection of current research on logic programming languages presents results from a three-year, ESPRIT-funded effort to explore the integration of the foundational issues of functional, logic, and object-oriented programming. It offers valuable insights into the fast-developing extensions of logic programming with functions, constraints, concurrency, and objects. Chapters are grouped according to the unifying themes of functional programming, constraint, logic programming, and object-oriented programming.

We study a hierarchy of Kalmàr elementary functions on integers based on a classification of LOOP programs of limited complexity, namely those in which the depth of nestings of LOOP commands does not exceed two. It is proved that -place functions in can be enumerated by a single function in , and that the resulting hierarchy of elementary predicates (i.e., functions with 0,1-values) is proper in that there are predicates that are not in . Along the way the rudimentary predicates (...) of Smullyan are classified as. (shrink)

In 2006, in a special issue of this journal, several authors explored what they called the dual nature of artefacts. The core idea is simple, but attractive: to make sense of an artefact, one needs to consider both its physical nature—its being a material object—and its intentional nature—its being an entity designed to further human ends and needs. The authors construe the intentional component quite narrowly, though: it just refers to the artefact’s function, its being a means to realize a (...) certain practical end. Although such strong focus on functions is quite natural , I argue in this paper that an artefact’s intentional nature is not exhausted by functional considerations. Many non-functional properties of artefacts—such as their marketability and ease of manufacture—testify to the intentions of their users/designers; and I show that if these sorts of considerations are included, one gets much more satisfactory explanations of artefacts, their design, and normativity.Keywords: Artefacts; Dual Nature program; Function; Intentionality; Normativity. (shrink)

Dynamic epistemic logic is the logic of the effects of epistemic actions like making public announcements, passing private messages, revealing secrets, telling lies. This paper takes its starting point from the version of dynamic epistemic logic of [2], and demonstrates a tool that can be used for showing what goes on during a series of epistemic updates: the dynamic epistemic modelling tool DEMO [7, 9]. DEMO allows modelling epistemic updates, graphical display of update results, graphical display of action models, formula (...) evaluation in epistemic models, and translation of dynamic epistemic formulas to PDL [22] formulas. DEMO is written in Haskell. This paper intends to demonstrate its usefulness for visualizing the model transformations that take place during epistemic updating. (shrink)

As a result of these restrictions, an implementation of L [subscript lambda] does not need to implement full higher-order unification. Instead, an extension to first-order unification that respects bound variable names and scopes is all that is required. Such unification problems are shown to be decidable and to possess most general unifiers when unifiers exist. A unification algorithm and logic programming interpreter are described and proved correct. Several examples of using L[subscript lambda] as a meta-programming language are presented.

The issue of proper functioning of operative computing and the utility of program verification, both in general and of specific methods, has been discussed a lot. In many of those discussions, attempts have been made to take mathematics as a model of knowledge and certitude achieving, and accordingly infer about the suitable ways to handle computing. I shortly review three approaches to the subject, and then take a stance by considering social factors which affect the epistemic status of both mathematics (...) and computing. I use the analogy between mathematics and computing in reverse—that is to say, I consider operative computing as a form of making mathematics, and so attempt to learn from computing to mathematics in general. I conclude that mathematics engineering is a field to be both developed for practical improvement of doing mathematics and taken into consideration while philosophizing about mathematics as well. (shrink)

Programmed cell death (PCD) in unicellular organisms is in some instances an altruistic trait. When the beneficiaries are clones or close kin, kin selection theory may be used to explain the evolution of the trait, and when the trait evolves in groups of distantly related individuals, group or multilevel selection theory is invoked. In mixed microbial communities, the benefits are also available to unrelated taxa. But the evolutionary ecology of PCD in communities is poorly understood. Few hypotheses have been offered (...) concerning the community role of PCD despite its far-reaching effects. The hypothesis we consider here is that PCD is a black queen. The Black Queen Hypothesis (BQH) outlines how public goods arising from a leaky function are exploited by other taxa in the community. Black Queen (BQ) traits are essential for community survival, but only some members bear the cost of possessing them, while others lose the trait In addition, BQ traits have been defined in terms of adaptive gene loss, and it is unknown whether this has occurred for PCD. Our conclusion is that PCD fulfils the two most important criteria of a BQ (leakiness and costliness), but that more empirical data are needed for assessing the remaining two criteria. In addition, we hold that for viewing PCD as a BQ, the original BQH needs to include social traits. Thus, despite some empirical and conceptual shortcomings, the BQH provides a helpful avenue for investigating PCD in microbial communities. (shrink)

This study focuses on the influence of the work of Carl Stumpf on the thought of Karl Bühler. Our working hypothesis is based on the philosophical program that Bühler attributes to Stumpf and to which several of his works are largely indebted. It is divided into five parts. The first is intended to establish a relationship between Bühler and the School of Brentano to which Stumpf belongs. In the second, I show that Bühler became aware of Brentano's ideas and of (...) Stumpf's program during a stay at the Institute of Psychology of Berlin during the winter semester 1904-1905, and I briefly comment, in the third part, Bühler's references to the work of Stumpf and two of his books in which he defends Stumpf's program against his critics. After having established the solid knowledge that Bühler had of Stumpf's work, I outline, in the fourth part, the main aspects of this program and evaluate, in the fifth, how Bühler uses it in the field of sensory phenomena (gestalt). I conclude this study with several remarks on Stumpf's positive evaluation of the work of Bühler. (shrink)

Just as war can be viewed as continuation of diplomacy using other means, computational semantics is continuation of logical analysis of natural language by other means. For a long time, the tool of choice for this used to be Prolog. In our recent textbook we argue (and try to demonstrate by example) that lazy functional programming is a more appropriate tool. In the talk we will lay out a program for computational semantics, by linking computational semantics to the (...) general analysis of procedures for social interaction. The talk will give examples of how Haskell can be used to begin carrying out this program. (shrink)

The International Logic Programming Symposium is one of two major international conferences sponsored by the Association of Logic Programming. Both conferences are held annually. The theme for the 1995 conference was "Declarative Systems", particularly the integration of the logic programming, functional programming, and object-oriented programming paradigms.

This paper reinforces the current consensus against the applicability of the selected effect theory of function in ecology. It does so by presenting an argument which, in contrast with the usual argument invoked in support of this consensus, is not based on claims about whether ecosystems are customary units of natural selection. Instead, the argument developed here is based on observations about the use of the function concept in functional ecology, and more specifically, research into the relationship between biodiversity (...) and ecosystem functioning. It is argued that a selected effect account of ecological functions is made implausible by the fact that it would conflict with important aspects of the understanding of function and ecosystem functional organization which underpins functional ecology’s research program. Specifically, it would conflict with (1) Functional ecology’s adoption of a context-based understanding of function and its aim to study the functional equivalence between phylogenetically-divergent organisms; (2) Functional ecology’s attribution to ecosystems of a lower degree of part-whole integration than the one found in paradigm individual organisms; and (3) Functional ecology’s adoption of a physiological or metabolic perspective on ecosystems rather than an evolutionary one. (shrink)

Most models of computer programming explain the programmer's behaviour by a single design strategy. This article presents a cognitive architecture that uses cue‐based search to model multiple design strategies including procedural, functional, means‐end or focal, and opportunistic design. The model has been implemented in an artificial intelligence (AI) system that generates Pascal programs from English specifications.Knowledge is represented as nodes that reside in internal or external memory, where a node encodes an action that may range from a line (...) of code to a routine in size. A program is built by linking nodes through a search cue of the form. The cue is broadcast to memory, and any matching node is returned; the cue provides a question to ask, and the return provides the answer. A cue on the newly linked node is then selected as a new focus, and the search process repeated. Each design strategy defines a specific node visiting order that traverses the program structure through its links. (shrink)

This study examined the recall of car and food advertisements within either a car or food television program to investigate the relationship between recall, program content, and viewer involvement. The participants, 92 sixth-form students, aged between 16–17 years, were randomly assigned to one of four conditions. As predicted, advertisements placed within a program of dissimilar content were recalled significantly better than if placed within a program of similar content. A gender bias in recall was found with females recalling female-orientated products (...) significantly better than males. Viewer-involvement ratings factored onto three factor clusters: enjoyable, cheerful, and humorous. Negative correlations were shown between cheerfulness and recall in the car program, and positive correlations were shown between cheerfulness and recall in the food program. Finally, implications of the results were considered. (shrink)

The purpose of this randomized controlled study was to investigate the effects of a 12-week coordinative ability training program on adolescents’ cognitive functioning, using evaluation tests of visuospatial perception, attention, and working memory. We randomly assigned 60 public school students (14–15 years) to either an experimental coordinative abilities training (∼40 min twice/week) group (n= 30) or a control group (n= 30) who received general psycho-physical wellness training (∼40 min., twice a week). At baseline and after training we used two standardized (...) motor tests and a single cognitive measure (Corsi’s Block-tapping test) to assess students’ visuospatial perception, attention, and working memory. We found a significant Time x Group interaction for the Throwing and Catching Test and Corsi’s Block-Tapping test, reflecting a meaningful experimental group improvement (p< 0.001), and there were no significant pre-post changes found in the control group. Thus, a 12-week program of coordinative abilities was able to improve not only coordination skills but aspects of cognitive functioning relevant to academic achievement. (shrink)

Long ago, when Alexander the Great asked the mathematician Menaechmus for a crash course in geometry, he got the famous reply ``There is no royal road to mathematics.'' Where there was no shortcut for Alexander, there is no shortcut for us. Still, the fact that we have access to computers and mature programming languages means that there are avenues for us that were denied to the kings and emperors of yore. The purpose of this book is to teach logic (...) and mathematical reasoning in practice, and to connect logical reasoning with computer programming in Haskell. Haskell emerged in the 1990s as a standard for lazy functional programming, a programming style where arguments are evaluated only when the value is actually needed. Haskell is a marvelous demonstration tool for logic and maths because its functional character allows implementations to remain very close to the concepts that get implemented, while the laziness permits smooth handling of infinite data structures. This book does not assume the reader to have previous experience with either programming or construction of formal proofs, but acquaintance with mathematical notation, at the level of secondary school mathematics is presumed. Everything one needs to know about mathematical reasoning or programming is explained as we go along. After proper digestion of the material in this book, the reader will be able to write interesting programs, reason about their correctness, and document them in a clear fashion. The reader will also have learned how to set up mathematical proofs in a structured way, and how to read and digest mathematical proofs written by others. This is the updated, expanded, and corrected second edition of a much-acclaimed textbook. Praise for the first edition: 'Doets and van Eijck's ``The Haskell Road to Logic, Maths and Programming'' is an astonishingly extensive and accessible textbook on logic, maths, and Haskell.' Ralf Laemmel, Professor of Computer Science, University of Koblenz-Landau. (shrink)

Research regarding ethics programs represents an important segment of business ethics literature. In the last thirty years, scientific discourse on ethics programs has flourished. Numerous studies examined their functions, composition, application in organizational practice, and impact on employee ethical behavior and many other organizational variables. However, so far there has been no study that would comprehensively map this particular field. Given that, this paper aims to examine discourse on ethics programs in its complexity within business and management literature. Based on (...) a sophistically composed search protocol in the Scopus database, and after multiple rounds of checks, we extracted a final sample of 287 documents that matched the selection criteria. The sample was thoroughly analyzed by means of advanced bibliometric analytics tools. The results show the quantitative impact of ethics program literature via publication and citation metrics, a network of co-occurring themes and clusters of scientific inquiry, and the evolution of respective discourse over time. This detailed analysis results in a set of conclusions provided in the last part of the paper summarizing the quantitative performance and thematic scope of literature on ethics programs. (shrink)

Smooth function is the essence of the ε-smooth support vector regression (ε-SSVR) which is an unconstrained convex quadratic programming. In this paper, Bézier function as a new smooth function is proposed to replace the ε-insensitive loss function of ε-SSVR with tolerating a smaller error in fitting given data sets linearly and nonlinearly. The ε-Bézier function smooth support vector regression (ε-BSSVR) model is presented. Theoretical analyses show that the derived smooth function has improved approximation precision compared with other smooth approximate (...) functions. The Newton-Armijo algorithm is applied to solve the new model. Numerical results and comparisons demonstrate that the proposed method has the better regression performance and learning efficiency compared with other given models. (shrink)

The variety of semantical approaches that have been invented for logic programs is quite broad, drawing on classical and many-valued logic, lattice theory, game theory, and topology. One source of this richness is the inherent non-monotonicity of its negation, something that does not have close parallels with the machinery of other programming paradigms. Nonetheless, much of the work on logic programming semantics seems to exist side by side with similar work done for imperative and functional programming, (...) with relatively minimal contact between communities. In this paper we summarize one variety of approaches to the semantics of logic programs: that based on fixpoint theory. We do not attempt to cover much beyond this single area, which is already remarkably fruitful. We hope readers will see parallels with, and the divergences from the better known fixpoint treatments developed for other programming methodologies. (shrink)

It has been known since the seventies that the formulas of modal logic are invariant for bisimulations between possible worlds models — while conversely, all bisimulation-invariant first-order formulas are modally definable. In this paper, we extend this semantic style of analysis from modal formulas to dynamic program operations. We show that the usual regular operations are safe for bisimulation, in the sense that the transition relations of their values respect any given bisimulation for their arguments. Our main result is a (...) complete syntactic characterization of all first-order definable program operations that are safe for bisimulation. This is a semantic functional completeness result for programming, which may be contrasted with the more usual analysis in terms of computational power. The 'Safety Theorem' can be modulated in several ways. We conclude with a list of variants, extensions, and further developments. (shrink)

This volume contains papers presented at the second international workshop on extensions of logic programming, 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 logic programming languages such as PROLOG, as well as connections between logic programming and functional programming, 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. (shrink)

A free logic is one in which a singular term can fail to refer to an existent object, for example, `Vulcan' or `5/0'. This essay demonstrates the fruitfulness of a version of this non-classical logic of terms (negative free logic) by showing (1) how it can be used not only to repair a looming inconsistency in Quine's theory of predication, the most influential semantical theory in contemporary philosophical logic, but also (2) how Beeson, Farmer and Feferman, among others, use it (...) to provide a natural foundation for partial functions in programming languages. Vis à vis (2), the question is raised whether the Beeson-Farmer-Feferman approach is adequate to the treatment of partial functions in all programming languages. Gumb and the author say No, and suggest a way of handling the refractory cases by means of positive free logic. Finally, Antonelli's solution of a problem associated with the Gumb-Lambert proposal is mentioned. (shrink)