Theories with self-application and computational complexity

Applicative theories form the basis of Feferman’s systems of explicit mathematics, which have been introduced in the 1970s. In an applicative universe, all individuals may be thought of as operations, which can freely be applied to each other: self-application is meaningful, but not necessarily total. It has turned out that theories with self-application provide a natural setting for studying notions of abstract computability, especially from a proof-theoretic perspective. This paper is concerned with the study of (unramified) bounded applicative theories which have a strong relationship to classes of computational complexity. We propose new applicative systems whose provably total functions coincide with the functions computable in polynomial time, polynomial space, polynomial time and linear space, as well as linear space. Our theories can be regarded as applicative analogues of traditional systems of bounded arithmetic. We are also interested in higher-type features of our systems; in particular, it is shown that Cook and Urquhart’s system is directly contained in a natural applicative theory of polynomial strength.     

Using Annotations to Make Recursion Equations Behave

The use of annotated recursion equations as a programming technique is investigated by considering the "telegram problem." The annotations are used to select alternative strategies for evaluating the applicative expressions contained in the recursion equations, while the equations serve as an abstract specification of the desired results. This method has the advantage that the annotations explicitly display certain kinds of decision that would otherwise be implicit.     

Normalising the associative law: An experiment with Martin-Löf's type theory

Martin-Löf's type theory contains a logic, a specification language and a programming language, so it is a tool with different uses. Although it is traditionally used as anintegrated programming logic, it may well be used as anexternal logic, which is necessary if one wants to use the formalism of type theory to verify the correctness of an external program. Different tools, such as well founded recursion, measure functions, or the separation of correctness into termination and partial correctness, may be used to obtain a correct type theory program. Type theory is viewed as anopen system with respect toinductively defined types and predicates, which makes it easy to represent an external program as agraph. Formal proofs have been edited using Larry Paulson's ISABELLE.     

Recursion Hypothesis Considered as a Research Program for Cognitive Science

Humans grasp discrete infinities within several cognitive domains, such as in language, thought, social cognition and tool-making. It is sometimes suggested that any such generative ability is based on a computational system processing hierarchical and recursive mental representations. One view concerning such generativity has been that each of the mind’s modules defining a cognitive domain implements its own recursive computational system. In this paper recent evidence to the contrary is reviewed and it is proposed that there is only one supramodal computational system with recursion in the human mind. A recursion thesis is defined, according to which the hominin cognitive evolution is constituted by a recent punctuated genetic mutation that installed the general, supramodal capacity for recursion into the human nervous system on top of the existing, evolutionarily older cognitive structures, and it is argued on the basis of empirical evidence and theoretical considerations that the recursion thesis constitutes a plausible research program for cognitive science.     

Syntactic Structures and Recursive Devices: A Legacy of Imprecision

Taking Chomsky’s Syntactic Structures as a starting point, this paper explores the use of recursive techniques in contemporary linguistic theory. Specifically, it is shown that there were profound ambiguities surrounding the notion of recursion in the 1950s, and that this was partly due to the fact that influential texts such as Syntactic Structures neglected to define what exactly constituted a recursive device. As a result, uncertainties concerning the role of recursion in linguistic theory have prevailed until the present day, and some of the most common misunderstandings that have appeared in recent discussions are examined at some length. This article shows that debates about such topics are frequently undermined by fundamental misunderstandings concerning core terminology, and the full extent of the prevailing haziness is revealed. An attempt is made, for instance, to distinguish between such things as iterative constructional devices and self-similar syntactic embedding, despite the fact that these are usually both unhelpfully classified as examples of recursion. Consequently, this article effectively constitutes a plea for much greater accuracy and clarity when such important issues are addressed from a linguistic perspective.     

A symbolic algorithm for computing recursion operators of nonlinear partial differential equations

A recursion operator is an integro-differential operator which maps a generalized symmetry of a nonlinear partial differential equation (PDE) to a new symmetry. Therefore, the existence of a recursion operator guarantees that the PDE has infinitely many higher-order symmetries, which is a key feature of complete integrability. Completely integrable nonlinear PDEs have a bi-Hamiltonian structure and a Lax pair; they can also be solved with the inverse scattering transform and admit soliton solutions of any order.

A straightforward method for the symbolic computation of polynomial recursion operators of nonlinear PDEs in (1+1) dimensions is presented. Based on conserved densities and generalized symmetries, a candidate recursion operator is built from a linear combination of scaling invariant terms with undetermined coefficients. The candidate recursion operator is substituted into its defining equation and the resulting linear system for the undetermined coefficients is solved.

The method is algorithmic and is implemented in Mathematica. The resulting symbolic package PDERecursionOperator.m can be used to test the complete integrability of polynomial PDEs that can be written as nonlinear evolution equations. With PDERecursionOperator.m, recursion operators were obtained for several well-known nonlinear PDEs from mathematical physics and soliton theory.     

Algebraic solutions to recursion schemes

The main problem in recursive scheme theory is determining how to solve a scheme and express its solution. Up to now this was always achieved by adding restrictive hypotheses either on the schemes themselves, or on the domains where they take their values, e.g., assuming the domains have a metric or an order structure and are complete with respect to this structure, or are iterative. Here we develop a strictly algebraic theory of recursion schemes with second-order substitutions. As it is strictly algebraic, the theory applies not only to all recursion schemes on trees, but also to recursion schemes on arbitrary algebras presented in the usual way by generators and relations. In particular, this gives a semantics for nondeterminism and for process algebras.     

A principled approach to programming with nested types in Haskell

Initial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold combinator which encapsulates structured recursion over data of that type, and a fold/build rule which optimises modular programs by eliminating from them data constructed using the buildcombinator, and immediately consumed using the foldcombinator, for that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types in Haskell. Specifically, the standard folds derived from initial algebra semantics have been considered too weak to capture commonly occurring patterns of recursion over data of nested types in Haskell, and no build combinators or fold/build rules have until now been defined for nested types. This paper shows that standard folds are, in fact, sufficiently expressive for programming with nested types in Haskell. It also defines buildcombinators and fold/build fusion rules for nested types. It thus shows how initial algebra semantics provides a principled, expressive, and elegant foundation for programming with nested types in Haskell.     

Set theory for verification. II: Induction and recursion

A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs, and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski theorem over a suitable set.Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion.Recursive data structures are expressed by applying the Knaster-Tarski theorem to a set, such asV , that is closed under Cartesian product and disjoint sum.Worked examples include the transitive closure of a relation, lists, variable-branching trees, and mutually recursive trees and forests. The Schröder-Bernstein theorem and the soundness of propositional logic are proved in Isabelle sessions.     

Extended recursion-based formalization of virus mutation

Computer viruses are programs that can replicate themselves by infecting other programs in a system. Bonfante, Kaczmarek and Marion have recently proposed a classification of viruses which relies on the recursion theory and its recursion theorems. We propose an extension of their formalism to consider in a more practical way the mutation of viruses. In particular, we are interested in modelling any depth of mutation, not just the first two levels. We show that this formalism still relies on recursion theorems, whatever the depth of mutation, even in the case of infinite depth. We also extend furthermore this formalism to model the viability of viral replication, which ensures that an infected program still can propagate the virus. An application of the proposed formalism to the class of combined viruses (multi-part viruses) is studied. Finally, given that metamorphic viruses can be modelled by grammars operating on grammars, we study a recursion-based approach of formal grammars and show that the recursion theorems of the recursion theory can be ported to the formal grammars theory.     

Nominal logic, a first order theory of names and binding

This paper formalises within first-order logic some common practices in computer science to do with representing and reasoning about syntactical structures involving lexically scoped binding constructs. It introduces Nominal Logic, a version of first-order many-sorted logic with equality containing primitives for renaming via name-swapping, for freshness of names, and for name-binding. Its axioms express properties of these constructs satisfied by the FM-sets model of syntax involving binding, which was recently introduced by the author and M.J. Gabbay and makes use of the Fraenkel–Mostowski permutation model of set theory. Nominal Logic serves as a vehicle for making two general points. First, name-swapping has much nicer logical properties than more general, non-bijective forms of renaming while at the same time providing a sufficient foundation for a theory of structural induction/recursion for syntax modulo α-equivalence. Secondly, it is useful for the practice of operational semantics to make explicit the equivariance property of assertions about syntax – namely that their validity is invariant under name-swapping.     

The <Emphasis Type="Italic">λ</Emphasis>-Calculus and the Unity of Structural Proof Theory

In the context of intuitionistic implicational logic, we achieve a perfect correspondence (technically an isomorphism) between sequent calculus and natural deduction, based on perfect correspondences between left-introduction and elimination, cut and substitution, and cut-elimination and normalisation. This requires an enlarged system of natural deduction that refines von Plato’s calculus. It is a calculus with modus ponens and primitive substitution; it is also a “coercion calculus”, in the sense of Cervesato and Pfenning. Both sequent calculus and natural deduction are presented as typing systems for appropriate extensions of the λ-calculus. The whole difference between the two calculi is reduced to the associativity of applicative terms (sequent calculus = right associative, natural deduction = left associative), and in fact the achieved isomorphism may be described as the mere inversion of that associativity. The novel natural deduction system is a “multiary” calculus, because “applicative terms” may exhibit a list of several arguments. But the combination of “multiarity” and left-associativity seems simply wrong, leading necessarily to non-local reduction rules (reason: normalisation, like cut-elimination, acts at the head of applicative terms, but natural deduction focuses at the tail of such terms). A solution is to extend natural deduction even further to a calculus that unifies sequent calculus and natural deduction, based on the unification of cut and substitution. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions.     

程序设计中递归函数教学问题探究

递归问题是程序设计语言教学中的一个重点、难点内容,针对递归教学的教学特点,阐述递归函数的精髓和教学方法,提出将理论和实践结合起来,通过剖析学生在学习递归函数时产生的错误和误区,应用实例和类比策略帮助学生解决递归函数学习中存在的问题,取得了事半功倍的教学效果。     

Predicate μ-Calculus for Mobile Ambients

Ambient logics have been proposed to describe properties for mobile agents which may evolve over time as well as space. This paper takes a predicate-based approach to extending an ambient logic with recursion, yielding a predicate μ-calculus in which fixpoint formulas are formed using predicate variables. An algorithm is developed for model checking finite-control mobile ambients against formulas of the logic, providing the first decidability result for model checking a spatial logic with recursion.     

UnQL: a query language and algebra for semistructured data based on structural recursion

Abstract. This paper presents structural recursion as the basis of the syntax and semantics of query languages for semistructured data and XML. We describe a simple and powerful query language based on pattern matching and show that it can be expressed using structural recursion, which is introduced as a top-down, recursive function, similar to the way XSL is defined on XML trees. On cyclic data, structural recursion can be defined in two equivalent ways: as a recursive function which evaluates the data top-down and remembers all its calls to avoid infinite loops, or as a bulk evaluation which processes the entire data in parallel using only traditional relational algebra operators. The latter makes it possible for optimization techniques in relational queries to be applied to structural recursion. We show that the composition of two structural recursion queries can be expressed as a single such query, and this is used as the basis of an optimization method for mediator systems. Several other formal properties are established: structural recursion can be expressed in first-order logic extended with transitive closure; its data complexity is PTIME; and over relational data it is a conservative extension of the relational calculus. The underlying data model is based on value equality, formally defined with bisimulation. Structural recursion is shown to be invariant with respect to value equality. Received: July 9, 1999 / Accepted: December 24, 1999     

Parallel Computing with the Sisal Applicative Language: Programmability and Performance Issues

The traditional argument for applicative languages has been programmability. Indeed, due to high-level abstractions and the implicit parallelism provided by applicative languages, programmers are free to concentrate on the implementation of the algorithm at hand without being burdened with low-level machine execution details. However, it has long been believed that the implementation and raw performance of applicative languages would be their downfall. We report here that it is easy to deliver both programmability and performance through applicative programming. To demonstrate the viability of applicative programming in the context of parallel computing, quantitative results from an experiment which consists of developing a multigrid elliptic Partial Differential Equation (PDE) solver are presented.     

Space-time tradeoffs for linear recursion

A linear recursive procedure is one each of whose executions activates at most one invocation of itself. When linear recursion cannot be replaced by iteration, it is usually implemented with a stack of size proportional to the depth of recursion. In this paper we analyze implementations of linear recursion which permit large reductions in storage space at the expense of a small increase in computation time. For example, if the depth of recursion isn, storage space can be reduced to \(\sqrt n \) at the cost of a constant factor increase in running time. The problem is treated by abstracting any implementation of linear recursion as the pebbling of a simple graph, and for this abstraction we exhibit the optimal space-time tradeoffs.     

On the observational theory of the CPS-calculus

We apply powerful proof-techniques of concurrency theory to study the observational theory of Thielecke’s CPS-calculus, a distillation of the target language of Continuation-Passing Style transforms. We define a labelled transition system from which we derive a (weak) labelled bisimilarity that completely characterises Morris’ context-equivalence. We prove a context lemma showing that Morris’ context-equivalence coincides with a simpler context-equivalence closed under a smaller class of contexts. Then we profit of the determinism of the CPS-calculus to give a simpler labelled characterisation of Morris’ equivalence, in the style of Abramsky’s applicative bisimilarity. We enhance our bisimulation proof-methods with up to bisimilarity and up to context proof techniques. We use our bisimulation proof techniques to investigate a few algebraic properties on diverging terms that cannot be proved using the original axiomatic semantics of the CPS-calculus.     

A survey of recursive analysis and Moore’s notion of real computation

The theory of analog computation aims at modeling computational systems that evolve in a continuous space. Unlike the situation with the discrete setting there is no unified theory of analog computation. There are several proposed theories, some of them seem quite orthogonal. Some theories can be considered as generalizations of the Turing machine theory and classical recursion theory. Among such are recursive analysis and Moore’s class of recursive real functions. Recursive analysis was introduced by Turing (Proc Lond Math Soc 2(42):230–265, 1936), Grzegorczyk (Fundam Math 42:168–202, 1955), and Lacombe (Compt Rend l’Acad Sci Paris 241:151–153, 1955). Real computation in this context is viewed as effective (in the sense of Turing machine theory) convergence of sequences of rational numbers. In 1996 Moore introduced a function algebra that captures his notion of real computation; it consists of some basic functions and their closure under composition, integration and zero-finding. Though this class is inherently unphysical, much work have been directed at stratifying, restricting, and comparing it with other theories of real computation such as recursive analysis and the GPAC. In this article we give a detailed exposition of recursive analysis and Moore’s class and the relationships between them.     

Backtracking in recursive computations

Summary A mathematical (denotational) semantics is constructed for a formalism of recursive equations with the Alternative operator. This formalism enables the combination of recursion and backtracking. The semantics is defined by applying fixpoint theory to set valued functions. We introduce the notion of strategy to produce subsets of the result. Two implementations are suggested using an auxiliary stack, that trade off recomputation time with space in the auxiliary stack. The concept of a sub-fixpoint is introduced, and the implementations are shown to be incomplete even w.r.t. sub-fixpoint values. One special strategy, the leftmost strategy, which stems from problems such as pattern matching or parsing, is discussed.