The Theory and Applications of Models of Computation (TAMC) conference series is both international and interdisciplinary in character, bringing together researchers working in computer science, mathematics (especially logic) and the physical sciences. It is this, together with its predominantly computational and computability theoretic focus, that gives the series its special character.

We show that, for any abstract complexity measure in the sense of Blum and for any computable function f (or computable operator F), the class of problems that are f-speedable (or F-speedable) does not have effective measure 0. On the other hand, for sufficiently fast growing f (or F), the class of non-speedable computable problems does not have effective measure 0. These results answer some questions raised by Calude and Zimand. We also give a quantitative analysis of Borodin and Trakhtenbrot's Gap Theorem, which corrects a claim by Calude and Zimand.

We consider a functional language that performs non-deterministic tests on real numbers and define a denotational semantics for that language based on Smyth powerdomains. The semantics is only an approximate one because the denotation of a program for a real number may not be precise enough to tell which real number the program computes. However, for many first-order total functions f : n → , there exists a program for f whose denotation is precise enough to show that the program indeed computes the function f. In practice, it is not difficult to find programs like this that possess a faithful denotation. We provide a few examples of such programs and the corresponding proofs of correctness.

We define and investigate a number of small inductively defined classes (idc's), à la Gregorczyk, that are based on argument-bounded initial functions and the bounded minimalisation and bounded counting schemata. We establish equivalences between these and other classes in the literature, with an emphasis on minimalism. We also obtain characterisations of the classes in terms of well-known fragments of first-order predicate logic.

We study the existence of bisimulations for Kleisli morphisms associated with the Giry monad of subprobabilities over Polish spaces. We first investigate these morphisms and show that the problem can be reduced to the existence of bisimulations for objects in the base category of stochastic relations using simulation equivalent congruences. This leads us to a criterion for two objects to be bisimilar.

We show that the diamond lattice can be embedded into the Σ02 enumeration degrees preserving 0 and 1, with atoms one high and Π01, and the other one low.

Wang tiles are unit-size squares with coloured edges. In this paper, we approach one aspect of the study of tiling computability: the quest for a universal tile set. Using a complex construction, based on Robinson's classical construction and its different modifications, we build a tile set (pronounced ayin) that almost always simulates any tile set. By way of Banach–Mazur games on tilings topological spaces, we prove that the set of -tilings that do not satisfy the universality condition is meagre in the set of -tilings.

Haplotypes are more useful in complex disease gene mapping than single-nucleotide polymorphisms (SNPs). However, haplotypes are difficult to obtain directly using biological experiments, which has prompted research into efficient computational methods for determining haplotypes. The individual haplotyping problem called Minimum Letter Flip (MLF) is a computational problem that, given a set of aligned DNA sequence fragment data of an individual, induces the corresponding haplotypes by flipping minimum SNPs. There has been no practical exact algorithm for solving the problem. Due to technical limits in DNA sequencing experiments, the maximum length of a fragment sequenced directly is about 1kb. In consequence, with a genome-average SNP density of 1.84 SNPs per 1 kb of DNA sequence, the maximum number k1 of SNP sites that a fragment covers is usually small. Moreover, in order to save time and money, the maximum number k2 of fragments that cover an SNP site is usually no more than 19. Building on these fragment data properties, the current paper introduces a new parameterised algorithm with running time O(nk22k2 + mlogm + mk1), where m is the number of fragments and n is the number of SNP sites. In practical biological applications, the algorithm solves the MLF problem efficiently even if m and n are large.

In this paper, we investigate the axiomatic semantics of the projection temporal logic programming language MSVL. To this end, we employ Propositional Projection Temporal Logic (PPTL) as an assertion language to specify the desired properties. We give a set of state axioms and state inference rules. In order to deduce a program over an interval, we also formalise a set of rules in terms of a Hoare logic-like triple. These rules enable us to deduce a program into its normal form and from the current state to the next one. They also enable us to verify properties over intervals. In this way, an axiom system for proving the correctness of MSVL programs is established. The axiom system is proved to be sound and relatively complete with respect to an operational model of MSVL, and give an example showing how the axiom system works. Finally, we employ a recently developed prototype verifier based on PVS as an example of semi-automatic verification using MSVL.

The logical and algebraic approaches are regarded as two of the dominant methodologies for the development of reactive and concurrent systems. It is well known that the logic approach is more abstract, but lacks compositionality; while the algebraic approach is inherently compositional, but lacks abstractness. However, connecting the two approaches is a major challenge in computer science, and many efforts have been directed to resolving the problem. Linking the algebraic approach to the logical approach has been satisfactorily resolved through the notion of characteristic formulae. But very limited success has been achieved so far in the other direction, as most of the established results have been developed only with respect to a simple semantics, which has usually been strong bisimulation. However, in practice, an observational semantics like weak bisimulation, which is much more complicated, is thought to be more useful. In this paper, we investigate how to connect the logical and algebraic approaches with respect to the observational preorder, which is a generalisation of weak bisimulation that takes divergence into account. We show the following results. First, we prove that the non-deterministic operator of process algebra can be defined in modal and temporal logics (such as the μ-calculus and the Fixpoint Logic with Chop) with respect to the observational preorder (in fact, the kernel of its precongruence). In this way, we can apply the logical approach to the design of a complex system in a compositional way. Second, we present two algorithms for constructing the characteristic formulae for a context-free process up to the preorder and its precongruence, respectively. The effect of this is that all the reductions for processes that are usually done in an algebraic setting can be handled in a logical setting.

Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal proof system based on an extension of Hofmann's SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. In particular, we define rules that directly justify the computational indistinguishability between programs, and then prove that these rules are sound with respect to the set-theoretic semantics, and thus the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micali's construction of a pseudorandom generator, and the equivalence between next-bit unpredictability and pseudorandomness.

The notion of divergence information of an ensemble of probability distributions was introduced by Jain, Radhakrishnan and Sen in Jain et al. (2002; 2009) in the context of the ‘substate theorem’. Since then, divergence has been recognised as a more natural measure of information in several situations in both quantum and classical communication.

We construct ensembles of probability distributions for which divergence information may be significantly smaller than the more standard Holevo information. As a result, we establish that bounds previously shown for Holevo information are weaker than similar ones shown for divergence information.