Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism

We give extensional and intensional characterizations of functional programs with nondeterminism: as structure preserving functions between biorders, and as nondeterministic sequential algorithms on ordered concrete data structures which compute them. A fundamental result establishes that these extensional and intensional representations are equivalent, by showing how to construct the unique sequential algorithm which computes a given monotone and stable function, and describing the conditions on sequential algorithms which correspond to continuity with respect to each order. We illustrate by defining may-testing and must-testing denotational semantics for sequential functional languages with bounded and unbounded choice operators. We prove that these are computationally adequate, despite the non-continuity of the must-testing semantics of unbounded nondeterminism. In the bounded case, we prove that our continuous models are fully abstract with respect to may-testing and must-testing by identifying a simple universal type, which may also form the basis for models of the untyped {\lambda}-calculus. In the unbounded case we observe that our model contains computable functions which are not denoted by terms, by identifying a further "weak continuity" property of the definable elements, and use this to establish that it is not fully abstract.

Definitional schemes for primitive recursive and computable functions

The unary primitive recursive functions can be defined in terms of a finite set of initial functions together with a finite set of unary and binary operations that are primitive recursive in their inputs. We reduce arity considerations, by show that two fixed unary operations suffice, and a single initial function can be chosen arbitrarily. The method works for many other classes of functions, including the unary partial computable functions. For this class of partial functions we also show that a single unary operation (together with any finite set of initial functions) will never suffice.

Representing Continuous Functions between Greatest Fixed Points of Indexed Containers

We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.

The Limits of Computation

This article provides a survey of key papers that characterise computable functions, but also provides some novel insights as follows. It is argued that the power of algorithms is at least as strong as functions that can be proved to be totally computable in type-theoretic translations of subsystems of second-order Zermelo Fraenkel set theory. Moreover, it is claimed that typed systems of the lambda calculus give rise naturally to a functional interpretation of rich systems of types and to a hierarchy of ordinal recursive functionals of arbitrary type that can be reduced by substitution to natural number functions.

Compressible Multikey and Multi-Identity Fully Homomorphic Encryption

With the development of new computing models such as cloud computing, user’s data are at the risk of being leaked. Fully homomorphic encryption (FHE) provides a possible way to fundamentally solve the problem. It enables a third party who does not know anything about the secret key and plaintexts to homomorphically perform any computable functions on the corresponding ciphertexts. In 2009, Gentry proposed the first FHE scheme. After that, its inefficiency has always been a bottleneck of the development of practical schemes and applications. At TCC 2019, Gentry and Halevi proposed the first compressible FHE scheme that enables the ratio of plaintext size to the ciphertext size (i.e., the compression rate) to reach 1 − ε for any small ε > 0 under the standard learning with errors (LWE) assumption. However, it is only a single-key one, where the homomorphic evaluation can only be performed over ciphertexts encrypted under the same key. Compared with single-key FHE, multikey FHE is more practical. Multikey FHE enables ciphertexts encrypted under different public keys to be homomorphically computed without having to decrypt these ciphertexts using their own private keys. In addition, in a multi-identity FHE scheme, only identity information and public parameters are required when encrypting, which simplifies certificate-based key management in public key infrastructure. In this paper, a new compressible ciphertext expansion technique is proposed. Then, we use this technique to construct a compressible multikey FHE scheme and a compressible multi-identity FHE scheme to overcome the bottleneck of bandwidth inefficiency in the multikey and multi-identity settings. The two schemes proposed in this paper make it possible that the objects of homomorphic operation can be the ciphertexts encrypted under different keys or different identities before compression, thus solving the single-key defect of the work of Gentry and Halevi.

The Church–Turing Fallacy

The Church–Turing thesis (CT) says that, if a function is computable in the intuitive sense, then it is computable by Turing machines. CT has been employed in arguments for the Computational Theory of Cognition (CTC). One argument is that cognitive functions are Turing-computable because all physical processes are Turing-computable. A second argument is that cognitive functions are Turing-computable because cognitive processes are effective in the sense analyzed by Alan Turing. A third argument is that cognitive functions are Turing-computable because Turing-computable functions are the only type of function permitted by a mechanistic psychology. This chapter scrutinizes these arguments and argues that they are unsound. Although CT does not support CTC, it is not irrelevant to it. By eliminating misunderstandings about the relationship between CT and CTC, we deepen our appreciation of CTC as an empirical hypothesis.

Quines are the Fittest Programs - Large Nesting Algorithmic Probability Converges to Constructors

In this article we explore the limiting behavior of the universal prior distribution obtained when applied over multiple meta-level hierarchy of programs and output data of a computational automata model. We were motivated to alleviate the effect of Solomonoff's assumption that all computable functions or hypotheses of the same length are equally likely, by weighing each program in turn by the algorithmic probability of their description number encoding. In the limiting case, the set of all possible program strings of a fixed-length converges to a distribution of self-replicating quines and quine-relays - having the structure of a constructor. We discuss how experimental algorithmic information theory provides insights towards understanding the fundamental metrics proposed in this work and reflect on the significance of these result in digital physics and the constructor theory of life.

Quantum Turing Machines: Computations and Measurements

Contrary to the classical case, the relation between quantum programming languages and quantum Turing Machines (QTM) has not been fully investigated. In particular, there are features of QTMs that have not been exploited, a notable example being the intrinsic infinite nature of any quantum computation. In this paper, we propose a definition of QTM, which extends and unifies the notions of Deutsch and Bernstein & Vazirani. In particular, we allow both arbitrary quantum input, and meaningful superpositions of computations, where some of them are “terminated” with an “output”, while others are not. For some infinite computations an “output” is obtained as a limit of finite portions of the computation. We propose a natural and robust observation protocol for our QTMs, which does not modify the probability of the possible outcomes of the machines. Finally, we use QTMs to define a class of quantum computable functions—any such function is a mapping from a general quantum state to a probability distribution of natural numbers. We expect that our class of functions, when restricted to classical input-output, will not be different from the set of the recursive functions.

Spiking Neural P Systems with Polarizations and Rules on Synapses

Spiking neural P systems are a class of computation models inspired by the biological neural systems, where spikes and spiking rules are in neurons. In this work, we propose a variant of spiking neural P systems, called spiking neural P systems with polarizations and rules on synapses (PSNRS P systems), where spiking rules are placed on synapses and neurons are associated with polarizations used to control the application of such spiking rules. The computation power of PSNRS P systems is investigated. It is proven that PSNRS P systems are Turing universal, both as number generating and accepting devices. Furthermore, a universal PSNRS P system with 151 neurons for computing any Turing computable functions is given. Compared with the case of SN P systems with polarizations but without spiking rules in neurons, less number of neurons are used to construct a universal PSNRS P system.