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.

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)

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.

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.

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

We 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). (shrink)

The paper studies a simply typed term system Mω providing a primitive recursive concept of parallelism in the sense of Plotkin. The system aims at defining and computing partial continuous functionals. Some connections between denotational and operational semantics → for Mω are investigated. It is shown that → is correct with respect to the denotational semantics. Conversely, → is complete in the sense that if a program denotes some number k, then it is reducible to the numeral nk. Restricting to (...) the primitive recursive kernel Rω of Mω, it is shown that → is strongly normalising with uniquely determined normal forms. The twist is the design of fixed point style conversion rules for constants accounting for parallelly bounded parallel search such that correctness and strong normalisation hold. Thereupon, minor alternations to → bring about that every reduction sequence for a program of Rω terminates either in a numeral nk if the program denotes k, or in the term 0 if the program denotes the “undefined” object. Thus, Rω can be considered a primitive recursive version of Plotkin's PA+·. (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.

• Lisp was intended to be compiled at first. However, a universal Lisp function eval in 1959 to show that neater language for computability theory than Turing Steve Russell pointed out that the universal function taken as an interpreter for pure Lisp, and hand-compiled..

How to write a program in Haskell, and how to use the Haskell testing tools . . . QuickCheck is a tool written in the functional programming language Haskell that allows testing of specifications by means of randomly generated tests. QuickCheck is part of the standard Haskell library. Re-implementations of QuickCheck exist for many languages, including Ruby and Scheme. SmallCheck is a similar tool, different from QuickCheck in that it tests properties for all finitely many values of (...) a datatype up to some given depth, with progressive increase of depth. Haskell is a research language: many of the testing tools that were first developed for Haskell later find their way to other languages. These slides discuss QuickCheck (two versions), SmallCheck, and some work in progress. We end with some examples of Alloy specifications. (shrink)

The present study investigates linguistics and cognitive effects of bilingualism with a minority language acquired through school medium education. If bilingualism has an effect on cognition and language abilities, regardless of language prestige or opportunities of use, young adult Gaelic-English speakers attending Gaelic medium education (GME) could have an advantage on linguistic and cognitive tasks targeting executive functions. These will be reported, compared to monolingual speakers living in the same area. Furthermore, this study investigates whether there is a difference in (...) Home Speakers of Gaelic (speakers who had acquired the language at home) compared to New Speakers of this language, i.e. whether an immersive context -as the one offered in medium education- compensates for not being native. A group of 23 monolingual English young adult speakers was compared with a group of 25 bilingual speakers attending a GME school since five years old. Participants were tested on comprehension of a set of sentences with incremental complexity in English, on their capacity to inhibit a distractor using the Test of Everyday attention (TEA) and on their performance in a Digit Span task. A tendency for a better performance on more complex linguistics and cognitive tasks was reported in bilinguals compared to monolinguals with a further advantage for New Speakers compared to Home Speakers. The study supports the idea that being bilingual in a minority language is as beneficial as speaking any other combination of languages. An immersive context of acquisition can be a good ground for developing advantages on both linguistics and cognitive tasks, with a further advantage for New speakers of the language. (shrink)

Currently, there is an increasing number of older population groups, especially in developed countries. This demographic trend, however, may cause serious problems, such as an increase in aging diseases, one of which is dementia whose main symptom consists in the decline of cognitive functioning. Although there has been ongoing pharmacological research on this neurological disorder, it has not brought satisfying results as far as its treatment is concerned. Therefore, governments all over the world are trying to develop alternative, non-pharmacological strategies/activities, (...) which could help to prevent this cognitive decline while this aging population is still healthy in order to reduce future economic and social burden. One of the non-pharmacological approaches, which may enhance cognitive abilities and protect against the decline in healthy older population, seems to be the learning of a foreign language. The purpose of this mini-review is to discuss recent findings about the effect of foreign language learning on the enhancement of cognitive functions among healthy older individuals. The findings, divided into three research areas, show that the learning of a foreign language may generate a lot of benefits for older individuals, such as enhancement of cognitive functioning, their self-esteem, increased opportunities of socializing, or reduction of costs. However, as Ware et al. (2017) indicate, any intervention program on foreign language learning should be well thought of and tailored to the needs of older people in order to be effective and avoid accompanying factors, such as older people’s anxiety or low self-confidence. Nevertheless, more empirical studies should be done in this area. (shrink)

A key problem in implicit complexity is to analyse the impact on program run times of nesting control structures, such as recursion in all finite types in functional languages or for-do statements in imperative languages.Three types of programs are studied. One type of program can only use ground type recursion. Another is concerned with imperative programs: ordinary loop programs and stack programs. Programs of the third type can use higher type recursion on notation as in functional (...) programming languages.The present approach to analysing run time yields various characterisations of fptime and all Grzegorczyk classes at and above the flinspace level. Central to this approach is the distinction between “top recursion” and “side recursion”. Top recursions are the only form of recursion which can cause an increase in complexity. Counting the depth of nested top recursions leads to several versions of “the μ-measure”. In this way, various recent solutions of key problems in implicit complexity are integrated into a uniform approach. (shrink)

The SDML programming language which is optimized for modelling multi-agent interaction within articulated social structures such as organizations is described with several examples of its functionality. SDML is a strictly declarative modelling language which has object-oriented features and corresponds to a fragment of strongly grounded autoepistemic logic. The virtues of SDML include the ease of building complex models and the facility for representing agents flexibly as models of cognition as well as modularity and code reusability.

This volume contains finalized versions of papers presented at an international workshop on extensions of logic programming, held at the Seminar for Natural Language Systems at the University of Tübingen in December 1989. Several recent extensions of definite Horn clause programming, especially those with a proof-theoretic background, have much in common. One common thread is a new emphasis on hypothetical reasoning, which is typically inspired by Gentzen-style sequent or natural deduction systems. This is not only of theoretical significance, (...) but also bears upon computational issues. It was one purpose of the workshop to bring some of these recent developments together. The volume covers topics such as the languages Lambda-Prolog, N-Prolog, and GCLA, the relationship between logic programming and functional programming, and the relationship between extensions of logic programming and automated theorem proving. It contains the results of the first conference concentrating on proof-theoretic approaches to logic programming. (shrink)

A number of general points behind the story of this paper may be worth setting out separately, now that we have come to the end.There is perhaps one obvious omission to be addressed right away. Although the word “information” has occurred throughout this paper, it must have struck the reader that we have had nothing to say on what information is. In this respect, our theories may be like those in physics: which do not explain what “energy” is (a notion (...) which seems quite similar to “information” in several ways), but only give some basic laws about its behaviour and transmission.The eventual recommendation made here has been to use a broad type-theoretic framework for studying various more classical and more dynamic notions of proposition in their interaction. This is not quite the viewpoint advocated by many current authors in the area, who argue for a whole-sale switch from a ‘static’ to a ‘dynamic’ perspective on propositions. This is not the place, however, to survey the conceptual arguments for and against such a more radical move.This still leaves many questions about possible reductions from one perspective to another. For instance, it would seem that classical systems ought to serve as a ‘limiting case’, which should still be valid after procedural details of some cognitive process have been forgotten. There are various ways of implementing the desired correspondence: e.g. by considering extreme cases with ⫅ equal to identity, or, in the pure relational algebra framework by considering only pairs (x, x). What we shall want then are reductions of dynamic logics, in those special cases, to classical logic. But perhaps also, more sophisticated views are possible. How do we take a piece of ‘dynamic’ prose, remove control instructions and the like, and obtain a piece of ‘classical’ text, suitable for inference ‘in the light of eternity’?There is also a more technical side to the matter of ‘reduction’. By now, Logic has reached such a state of ‘inter-translatability’ that almost all known variant logics can be embedded into each other, via suitable translations. In particular, once an adequate semantic has been given for a new system, this usually induces an embedding into standard logic: as we know, e.g., for the case of Modal Logic. Like-wise, all systems of dynamic interpretation or inference proposed so far admit of direct embedding into an ordinary ‘static’ predicate logic having explicit transition predicates (cf. van Benthem 1988b). Thus, our moral is this. The issue is not whether the new systems of information structure or processing are essentially beyond the expressive resources of traditional logical systems: for, they are not. The issue is rather which interesting phenomena and questions will be put into the right focus by them.The next broad issue concerns the specific use of the perspective proposed here, vis-à-vis concrete proposals for information-oriented or dynamic semantics. The general strategy advocated here is to locate some suitable base calculus and then consider which ‘extras’ are peculiar to the proposal. For instance, this is the spirit in which modal S4 would be a base logic of information models, and intuitionistic logicthe special theory devoting itself to upward persistent propositions. Or, with the examples in Section 4.1, the underlying base logic is our relational algebra, whereas, say, ordinary updates then impose special properties, such as ‘idempotence’: $$xRy \Rightarrow yRy$$ Does this kind of application presuppose the existence of one distinguished base logic, of which all others are extensions? This would be attractive-and some form of relational algebra or linear logic might be a reasonable candidate. Nevertheless, the enterprise does not rest on this outcome. What matters is an increased sensitivity to the ‘landscape’ of dynamic logics, just as with the ‘Categorial Hierarchy’ in Categorial Grammar (cf. van Benthem 1989a, 1991) where the family of logics with their interconnections seems more important than any specific patriarch.Finally, perhaps the most important issue in the new framework is the possibility of new kinds of questions arising precisely because of its differences from standard logic. Notably, given the option of regarding propositions as programs, it will be of interest to consider systematically which major questions about programming languages now make sense inside logic too.EXAMPLE. Correctness. When do we have $$\left[\kern-0.15em\left[ \pi \right]\kern-0.15em\right](\left[\kern-0.15em\left[ A \right]\kern-0.15em\right]) \subseteq \left[\kern-0.15em\left[ B \right]\kern-0.15em\right]$$ for (s, t) propositions A, B and a dynamic (s, (s, t)) proposition π?Program Synthesis. Which dynamic proposition will take us from an information state satisfying A to one satisfying B? (This question needs refinement, lest there be trivial answers.)Determinism. Which propositions as programs are deterministic, in the sense of defining single-valued functions from states to states?Querying. What does it mean to ask for information in the present setting? (Again, individual types referring to e will be crucial here.)This is not merely an agenda for wishful thinking. Within Logic, there are various ways of introducing such concerns into semantics, especially, using tools from Automata Theory. (See van Benthem 1989c for further discussion of such computational perspectives in ‘cognitive programming’.)At least if one believes that ‘dynamics’ is of the essence in cognition (rather than a mere interfacing problem between the halls of eternal truth and the noisy streets of reality), the true test for the present enterprise is the development of a significant new research program not merely copying the questions of old. (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)

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)

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)

Iterative characterizations of computable unary functions are useful patterns for the definition of programming languages based on iterative constructs. The features of such a characterization depend on the pairing producing it: this paper offers an infinite class of pairings involving very nice features.

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)

Formal pragmatics plays an important, though secondary, role in modern analytical philosophy of language: its aim is to explain how context can affect the meaning of certain special kinds of utterances. During recent years, the adequacy of formal tools has come under attack, often leading to one or another form of relativism or antirealism. Our aim will be to extend the critique to formal pragmatics while showing that sceptical conclusions can be avoided by developing a different approach to the issues. (...) In particular, we will show that formal pragmatics cannot provide a complete account of how context affects the meaning of utterances, both on its own terms and when faced with evidence of important aspects of natural languages. The focal issue is the relevant kind of context in which pragmatics should examine utterances. Our contention will be that the relevant context of an utterance is determined by the function of that utterance, this function being dependent upon the primary function of language – to convey information. We will argue that the functions of utterances and of language are too broad to be caught by the tools of formal pragmatics of the sort advocated by Montague (1968, 1974), which are an extension the methods of traditional model-theoretic semantics. The particular formal approach we will use as the main example is David Kaplan’s position (1979, 1989), an extension of Montague’s program. (shrink)

Natural language syntax yields an unbounded array of hierarchically structured expressions. We claim that these are used in the service of active inference in accord with the free-energy principle (FEP). While conceptual advances alongside modelling and simulation work have attempted to connect speech segmentation and linguistic communication with the FEP, we extend this program to the underlying computations responsible for generating syntactic objects. We argue that recently proposed principles of economy in language design—such as “minimal search” criteria from theoretical syntax—adhere (...) to the FEP. This affords a greater degree of explanatory power to the FEP—with respect to higher language functions—and offers linguistics a grounding in first principles with respect to computability. While we mostly focus on building new principled conceptual relations between syntax and the FEP, we also show through a sample of preliminary examples how both tree-geometric depth and a Kolmogorov complexity estimate (recruiting a Lempel–Ziv compression algorithm) can be used to accurately predict legal operations on syntactic workspaces, directly in line with formulations of variational free energy minimization. This is used to motivate a general principle of language design that we term Turing–Chomsky Compression (TCC). We use TCC to align concerns of linguists with the normative account of self-organization furnished by the FEP, by marshalling evidence from theoretical linguistics and psycholinguistics to ground core principles of efficient syntactic computation within active inference. (shrink)

Recently, connectionist models have been developed that seem to exhibit structuresensitive cognitive capacities without executing a program. This paper examines one such model and argues that it does execute a program. The argument proceeds by showing that what is essential to running a program is preserving the functional structure of the program. It has generally been assumed that this can only be done by systems possessing a certain temporalcausal organization. However, counterfactualpreserving functional architecture can be instantiated in other (...) ways, for example geometrically, which are realizable by connectionist networks. (shrink)

Formal pragmatics plays an important, though secondary, role in modern analytical philosophy of language: its aim is to explain how context can affect the meaning of certain special kinds of utterances. During recent years, the adequacy of formal tools has come under attack, often leading to one or another form of relativism or antirealism.1 Our aim will be to extend the critique to formal pragmatics while showing that sceptical conclusions can be avoided by developing a different approach to the issues. (...) In particular, we will show that formal pragmatics cannot provide a complete account of how context affects the meaning of utterances, both on its own terms and when faced with evidence of important aspects of natural languages. The focal issue is the relevant kind of context in which pragmatics should examine utterances. Our contention will be that the relevant context of an utterance is determined by the function of that utterance, this function being dependent upon the primary function of language – to convey information. We will argue that the functions of utterances and of language are too broad to be caught by the tools of formal pragmatics of the sort advocated by Montague (1968, 1974), which are an extension the methods of traditional model-theoretic semantics.2 The particular formal approach we will use as the main example is David Kaplan’s position (1979, 1989),3 an extension of Montague’s program. (shrink)

The computational program for theoretical neuroscience initiated by Marr and Poggio (1977) calls for a study of biological information processing on several distinct levels of abstraction. At each of these levels — computational (defining the problems and considering possible solutions), algorithmic (specifying the sequence of operations leading to a solution) and implementational — significant progress has been made in the understanding of cognition. In the past three decades, computational principles have been discovered that are common to a wide range of (...) functions in perception (vision, hearing, olfaction) and action (motor control). More recently, these principles have been applied to the analysis of cognitive tasks that require dealing with structured information, such as visual scene understanding and analogical reasoning. Insofar as language relies on cognition-general principles and mechanisms, it should be possible to capitalize on the recent advances in the computational study of cognition by extending its methods to linguistics. (shrink)

This book describes computability theory and provides an extensive treatment of data structures and program correctness. It makes accessible some of the author's work on generalized recursion theory, particularly the material on the logic programming language PROLOG, which is currently of great interest. Fitting considers the relation of PROLOG logic programming to the LISP type of language.

Nondeterministic programs occurring in recently developed programming languages define nondeterminate partial functions. Formulas (Boolean expressions) of such nondeterministic languages are interpreted by a nonempty subset of {T (true), F (false), U (undefined)}. As a semantic basis for the propositional part of a corresponding nondeterministic three-valued logic we study the notion of a truth-function over {T, F, U} which is computable by a nondeterministic evaluation procedure. The main result is that these truth-functions are precisely the functions satisfying four (...) basic properties, called -isotonic, –-isotonic, hereditarily guarded, and hereditarily guard-using, and that a function satisfies these properties iff it is explicitly definable (in a certain normal form) from if..then..else..fi, binary choice, and constants. (shrink)

This unique book presents a comprehensive and rigorous treatment of the theory of computability which is introductory yet self-contained. It takes a novel approach by looking at the subject using computation models rather than a limitation orientation, and is the first book of its kind to include software. Accompanying software simulations of almost all computational models are available for use in conjunction with the text, and numerous examples are provided on disk in a user-friendly format. Its applications to computer science (...) itself include interesting links to programming language theory, compiler design theory, and algorithm design. The software, numerous examples, and solutions make this book ideal for self-study by computer scientists and mathematicians alike. (shrink)

We show that to every recursive total continuous functional $\Phi$ there is a PCF-definable representative $\Psi$ of $\Phi$ in the hierarchy of partial continuous functionals, where PCF is Plotkin's programming language for computable functionals. PCF-definable is equivalent to Kleene's S1-S9-computable over the partial continuous functionals.

We introduce _Interleave-Disjunction-Lock parallel multiple context-free grammars_ (IDL-PMCFG), a novel grammar formalism designed to describe the syntax of free word order languages that allow for extensive interleaving of grammatical constituents. Though interleaved constituents, and especially the so-called hyperbaton, are common in several ancient (Classical Latin and Greek, Sanskrit...) and modern (Hungarian, Finnish...) languages, these syntactic structures are often difficult to express in existing formalisms. The IDL-PMCFG formalism combines Seki et al.’s parallel multiple context-free grammars (PMCFG) with Nederhof and (...) Satta’s IDL expressions. We define the semantics of IDL-PMCFGs and study their expressivity, proving that IDL-PMCFG extends both PMCFG and IDL-CFG (context-free grammars equipped with IDL expressions) and that IDL-PMCFG parsing is \(\mathrm {NP}\) -hard. We then introduce COMPĀ, a programming language extending Ranta’s Grammatical Framework (GF) and built as a high-level front-end formalism to IDL-PMCFG for practical grammar development. We present a parsing algorithm for IDL-PMCFG inspired by earlier Earley-style PMCFG parsing algorithms and Nederhof and Satta’s IDL graphs and give a worst-case estimate of its complexity as a function of several metrics on IDL expressions, the size of the input and a new notion of the _G_-density of a language. (shrink)

We prove that the observational equivalence of third-order finitary Idealized Algol is decidable using Game Semantics. By modelling the state explicitly in our games, we show that the denotation of a term M of this fragment of IA is a compactly innocent strategy-with-state, i.e. the strategy is generated by a finite view function fM. Given any such fM, we construct a real-time deterministic pushdown automaton that recognizes the complete plays of the knowing-strategy denotation of M. Since such plays characterize observational (...) equivalence, and there is an algorithm for deciding whether any two DPDAs recognize the same language, we obtain a procedure for deciding the observational equivalence of third-order finitary IA. Restricted to second-order terms, the DPDA representation cuts down to a deterministic finite automaton; thus our approach gives a new proof of Ghica and McCusker’s regular-expression characterization for this fragment. Our algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of IA and other cognate programming languages. Another result concerns second-order IA with full recursion: we show that observational equivalence for this fragment is undecidable. (shrink)

The prelims comprise: Introduction: Two Semantic Projects History The Uses of Semantics Conclusions.

What is the meaning of language expressions and how to compute or calculate it? In this paper, we give an answer to this question by analysing the meanings of aspects and tenses in natural languages inside the formal model of an grammar of applicative, cognitive and enunciative operations , using the applicative formalism, functional types of categorial grammars and combinatory logic . In the enunciative theory and following , an utterance can be decomposed into two components: a modus (...) and a dictum . In GRACE, the modus is a complex operator applied to a proposition and is generated from more elementary operators of the categories of tense, aspect, and modality. The dictum is a proposition generated by a predicative relation. In this way, we can attribute a semantic meaning to different grammatical aspecto-temporal operators. The applicative expressions of CL can be easily translated into a functional programming language such as HASKELL or CAML. (shrink)

In this paper we systematically derive a predicate transformer semantics from a direct semantics for a simple probabilistic-nondeterministic programming language . This goal is achieved by exhibiting the direct semantics as isomorphic to a continuation semantics from which the predicate transformer semantics can be read off immediately. This isomorphism allows one to identify nonempty convex compact saturated sets of valuations on the set S of states with certain “good” functionals from to in a way similar to the one how (...) H. Minkowski in 1903 related nonempty convex compact subsets of to what is nowadays called Minkowski functionals. (shrink)

ABSTRACT A computational logic, PLPR (Predicate Logic using Polymorphism and Recursion) is presented. Actually this logic is the object language of an automated deduction system designed as a tool for proving mathematical theorems as well as specify and verify properties of functional programs. A useful denotationl semantics and two general deduction methods for PLPR are defined. The first one is a tableau algorithm proved to be complete and also used as a guideline for building complete calculi. The second is (...) a sound and complete natural deduction system. Moreover a fixed point induction rule is introduced for formulas called continuous. The strategies for mechanizing the proofs of the final automated system are based on the previous deduction methods. As the examples of the use of the system show, the implemented theorem prover outperforms humans to a certain extent, retaining logic and calculi generality. (shrink)

Inquiry into language evolution has been controversial, mainly because there is no consensus as to the nature of both ‘evolution’ and ‘language.’ Berwick and Chomsky make sense of the evolution of language by treating it as a biological phenomenon. In contrast to functional characterizations of language as ‘communication’ or ‘speech,’ the authors define it as, essentially, a mind-internal computational mechanism. Within their minimalist approach, hierarchical syntactic structure is achieved through the recursive application of a basic operation called ‘Merge.’ The (...) simplicity of the basic operation is consistent with archeological evidence suggesting an evolutionary recent origin of language. (shrink)

Identification of programs for computable functions from their graphs and identification of grammars for recursively enumerable languages from positive data are two extensively studied problems in the recursion theoretic framework of inductive inference.In the context of function identification, Freivalds et al. have shown that only those collections of functions, , are identifiable in the limit for which there exists a 1-1 computable numbering ψ and a discrimination function d such that1. for each , the number of indices i such (...) that ψi = ƒ is exactly one and2. for each , there are only finitely many indices i such that ƒ and ψi agree on the first d arguments.A similar characterization for language identification in the limit has turned out to be difficult. A partial answer is provided in this paper. Several new techniques are introduced which have found use in other investigations on language identification. (shrink)

This is a thesis in formal semantics. It consists of two parts corresponding to the distinction, due to Richard Montague, between universal grammar and specific semantic theories. The first part concerns universal grammar and is intended to provide a precise and unified conceptual framework within which different theories of formal semantics can be represented and compared. ;The second part of the thesis is concerned with intensional logic, i.e., with the logical analysis of discourse involving so called oblique contexts. These contexts (...) are characterized by the apparent failure of certain classically valid principles of substitutivity. Two kinds of reactions among logicians to the appearance of oblique contexts in natural languages are distinguished: (1) the intensional point of view, according to which oblique contexts are seen as genuine counterexamples to classical logic and to the related semantical principle of extensionality: the principle that the denotation of an expression is a function of the denotations of its parts; and (2) the extensional point of view, according to which the conflict between oblique contexts and classical logic is only apparent. The extensional point of view therefore calls for analyses of oblique contexts that preserve the laws of classical logic and the principle of extensionality. In this thesis, we are concerned with the precise formulation of and comparison between different programs for the formal semantic representation of oblique contexts. In Chapter 5, we are concerned with Church's program of representing oblique contexts within a formal language whose semantics is fully extensional and based on Frege's distinction between sense and denotation. The ambiguity between the "direct" and "indirect" denotation of an expression A is avoided by letting A be replaced in oblique contexts by an expression which denotes A's ordinary sense. We provide a possible-worlds semantics for a version of Church's formal language with the following features: (i) Objectual quantification into oblique constructions is accounted for. The treatment of quantification requires for each entity x an essence of x, by which we mean a sense which determines x in those worlds in which x exists and is undefined in all other worlds. (ii) The variables range over actually existing entities only. It is allowed that entities of certain types are contingent, i.e., the same entity may exist in one world and fail to exist in other worlds. (iii) In order to combine a proper treatment of the cross-world identification of functions with varying domains, partial functions are allowed. (iv) Senses are allowed to be partially defined. For example, the sense of a proper name is undefined in a world in which the denotation of the name does not exist. (v) Senses of functions from objects of type a to objects of type b are identified with functions from senses of objects of type a to senses of objects of type b. In Chapters 6 and 7, we pursue the Russellian Alternative in intensional semantics, where a sense/denotation distinction is avoided. Apparent failures of substitutivity principles for singular terms are explained along the lines of Russell's theory of definite descriptions. Failures of substitutivity of coextensional sentences and predicates are explained by Russell's doctrine that sentences and predicate denote propositions and propositional functions , respectively. Russellian semantics is fully extensional in the sense that the Russellian denotation of a designator is a function of the Russellian denotations of its parts. In Chapter 6, a theory of Russellian propositions is developed within set theory. This theory is then applied in Chapter 7 to the task of providing a set-theoretic semantics for Russellian type theory. (shrink)

Patricia Smith Churchland's Neurophilosophy argues that a mind is the same thing as the complex patterns of neural activity in a human brain and, furthermore, that we will be able to find out interesting things about the mind by studying the brain. I basically agree with this stance and my comments are divided into four sections. First, comparisons between human and non?human primate brains are discussed in the context, roughly, of where one should locate higher functions. Second, I examine Churchland's (...) views on reduction and levels of organization, which I find mostly congenial. Third, a key point of disagreement about the relationship and importance of language to specifically human cognition is taken up. I like Churchland's critique of certain sentential paradigms, but I try to show using an analogy with cellular coding systems why we need to get a better theory of ?sentences?. Finally, I discuss how the models introduced in the last chapter might be extended to make better contact with neurobiology and language. (shrink)

Nonmonotonic causal logic is a knowledge representation language designed for describing domains that involve actions and change. The process of literal completion, similar to program completion familiar from the theory of logic programming, can be used to translate some nonmonotonic causal theories into classical logic. Its applicability is restricted, however, to theories that deal with truth-valued fluents, represented by predicate symbols. In this note we introduce functional completion—a more general process that can be applied to causal theories in (...) which fluents are treated as functions. (shrink)

Soames thinks the dependencies show up in the semantics if they are generated by variable binding. That will only partially overlap with Pinillos's ambitions for the notion of de jure codesignation. This chapter contributes towards 'domesticating' the kind of predicates that fans of de jure codesignation are friendly to, that is, making them seem less alien and somewhat less 'magical'. It surveys a novel kind of semantic structure that has been posited by Mark Richard, Kit Fine, Ángel Pinillos, and others. (...) It focuses on anaphora, especially cases that cannot be handled by a 'bound‐variable' analysis, and distinguishes our target view from other treatments of anaphora. The chapter discusses the semantics of attitude reports and discusses two kinds of complex anaphoric dependency. It explains a difference in how functions in a programming language can be sensitive to the identity of their operands. (shrink)

, which uses the intuitionistic propositional calculus, with the only connective →. It is very important, because the well known Curry-Howard correspondence between proofs and programs was originally discovered with it, and because it enjoys the normalization property: every typed term is strongly normalizable. It was extended to second order intuitionistic logic, in 1970, by J.-Y. Girard [4], under the name of system F, still with the normalization property.More recently, in 1990, the Curry-Howard correspondence was extended to classical logic, following (...) Felleisen and Griffin [6] who discovered that the law of Peirce corresponds to control instructions in functional programming languages. It is interesting to notice that, as early as 1972, Clint and Hoare [1] had made an analogous remark for the law of excluded middle and controlled jump instructions in imperative languages.There are now many type systems which are based on classical logic; among the best known are the system LC of J.-Y. Girard [5] and the λμ-calculus of M. Parigot [11]. We shall use below a system closely related to the latter, called the λ c -calculus [8, 9]. Both systems use classical second order logic and have the normalization property.In the sequel, we shall extend the λ c -calculus to the Zermelo-Frænkel set theory. The main problem is due to the axiom of extensionality. To overcome this difficulty, we first give the axioms of ZF in a suitable (equivalent) form, which we call ZF ɛ. (shrink)

This study employs fMRI to examine the neural substrates of response to cognitive training in healthy old adults. Twenty Japanese healthy elders participated in a 4-week program and practiced a verbal articulation task on a daily basis. Functional connectivity analysis revealed that in comparison to age- and education-matched controls, elders who received the cognitive training demonstrated increased connectivity in the frontotemporal regions related with language and memory functions and showed significant correlations between the behavioral change in a linguistic task (...) and connectivity in regions for goal-oriented persistence and lexical processing. The increased hippocampal connectivity was consistent with previous research showing efficacious memory improvement and change in hippocampal functioning. Moreover, the increased intra-network connectivity following cognitive training suggested an improved neural differentiation, in contrast to the inter-network activation pattern typical in the aging brain. This research not only validates the relationship of functional change in the frontal and temporal lobes to age-associated cognitive decline but also shows promise in turning neural change toward the right direction by cognitive training. (shrink)

We provide a full characterization of computational error states for information systems. The class of errors considered is general enough to include human rational processes, logical reasoning, scientific progress and data processing in some functional programming languages. The aim is to reach a full taxonomy of error states by analysing the recovery and processing of data. We conclude by presenting machine-readable checking and resolve algorithms.

The cornerstone of the radical program of positivism was the separation of science from metaphysics. In the good old days, the solution to this demarca tion problem was seen as a way of separating sheep from goats - ~ynthetic or analytic propositions, which were candidates for truth or falsity, either on empirical or formal grounds, on the one hand; and, on the other hand, those deceptive propositions which appeared to be truth claims, but were instead either meaningless, or nonsensical, or (...) poetical, or merely expressive - i.e. without proper cognitive content and hence not verifiable or falsifiable. In the last half century, analytic philosophy of science, linguistic analysis and logic have formulated and reformulated and reformulated again the distinction be tween science and metaphysics. The outcome was unexpected: metaphysics rather than retreating from the scene, shriveling up, dissolving, has instead re emerged as an acknowledged, even if problematic component of scientific theorizing. This has made some philosophers of science happy, others miserable. For Morris Lazerowitz, it should serve as evidence for his thesis that the sort of philosophical assertions which metaphysics makes about the nature of things are not simply radically undecidable, but persist because they express a deeper and unconscious function in the mental life of philosophers (and presumably, of those scientists who find it necessary to be philosophical in this way, whether self-consciously or tacitly). (shrink)

In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni–Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. In this paper we develop a semantics of SLR using BCK -algebras consisting of certain polynomial-time algorithms. It will follow from this semantics that safe recursion with arbitrary result type built up from (...) N and ⊸ as well as recursion over trees and other data structures remains within polynomial time. In its original formulation SLR supported only natural numbers and recursion on notation with first-order functional result type. (shrink)