This paper and our conference paper (Abbott, Altenkirch, Ghani, and McBride, 2003b) explain and analyse the notion of the derivative of a data structure as the type of its one-hole contexts based on the central observation made by McBride (2001). To make the idea precise we need a generic notion of a data type, which leads to the notion of a container, introduced in (Abbott, Altenkirch and Ghani, 2003a) and investigated extensively in (Abbott, 2003). Using containers we can provide a notion of linear map which is the concept missing from McBride's first analysis. We verify the usual laws of differential calculus including the chain rule and establish laws for initial algebras and terminal coalgebras.
Quasi-interpretations are a tool to bound the size of the values computed by a first-order functional program (or a term rewriting system) and thus a mean to extract bounds on its computational complexity. We study the synthesis of quasi-interpretations selected in the space of polynomials over the max-plus algebra. We prove that the synthesis problem is NP-hard under various conditions and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. We provide a polynomial time algorithm to synthesize homogeneous quasi-interpretations of bounded degree and show how to extend the algorithm to synthesize (general) quasi-interpretations. The resulting algorithm generalizes certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity.
In a previous work, we proved that an important part of the Calculus of Inductive Constructions (CIC), the basis of the Coq proof assistant, can be seen as a Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In this paper, we prove that almost all CIC can be seen as a CAC, and that it can be further extended with non-strictly positive types and inductive-recursive types together with non-free constructors and pattern-matching on defined symbols.
Elementary Affine Logic (EAL) is a variant of Linear Logic characterizing the computational power of the elementary bounded Turing machines. The EAL Type Inference problem is the problem of automatically assigning to terms of l-calculus EAL formulas as types. This problem, restricted to the propositional fragment of EAL, is proved to be decidable, and an algorithm is shown, building, for every l-term, either a negative answer or a finite set of type schemata, from which all and only its typings can be derived, through suitable operations.
The question whether a given functional of some full type structure (FTS for short) is l-definable by a closed l-term, known as the Definability Problem, was proved to be undecidable by R. Loader in 1993 (cf [Loa01a]). Later on, R. Loader refined his first result by establishing that the problem is undecidable for every FTS over at least 3 ground elements (cf [Loa01b]).
We solve here the remaining non trivial case and show that the problem is undecidable whenever there are at least two ground elements. The proof is based on a direct encoding of the Halting Problem for register machines into the Definability Problem restricted to the functionals of the Monster type M=(((o®o)®o)®o)®(o®o). It follows that this new restriction of the Definability Problem, which is orthogonal to the ones considered so far, is also undecidable. The latter fact yields a particularly simple proof of the undecidability of the b-Pattern Matching Problem, recently established by R. Loader in [Loa03].
The lm-calculus features both variables and names together with their binding mechanisms. This means that constructions on open terms are necessarily parameterized in two different ways for both variables and names. Semantically, such a construction must be modeled by a biparameterized family of operators. In this paper, we study these biparameterized operators on Selinger's categorical models of the lm-calculus called control categories. The overall development is analogous to that of Lambek's functional completeness of cartesian closed categories via polynomial categories. As a particular and important application of such consideration, we study the parameterizations of uniform fixed-point operators on control categories. We show a bijective correspondence between biparameterized fixed-point operators and nonparameterized ones under the uniformity conditions.
We study a notion of bounded stable biorder, showing that the monotone and stable functions on such biorders are sequential. We construct bounded biorder models of a range of sequential, higher-order functional calculi, including unary PCF, (typed and untyped) call-by-value and lazy l-calculi, and non-deterministic SPCF. We prove universality and full abstraction results for these models by reduction to the case of unary PCF, for which we give a simple new argument to show that any order-extensional and sequential model is universal.
Simple least-significant-bit (LSB) substitution is the most straightforward way to embed the secret image in the host image. Based on the simple LSB substitution, the method using substitution table is proposed to improve the quality of the stego-image. In this paper, we shall bring up a new method that uses the un-embedded host pixel bits to partition the host pixel into different planes. This way, we can derive the optimal substitution table for each plane. By combining the optimal substitution tables, we can obtain the final result that we call the multi-bit-reference substitution table. After transforming the secret data according multi-bit-reference substitution table, we can embed the transformed secret data in the host image so that the host image will be degraded possibly less. The experimental results show that our method leads to good results.
In a previous paper connections between the congruence axioms WFCA, SFCA and the revealed preference axioms WAFRP, SAFRP for fuzzy choice functions whose domain contains the characteristic functions of pairs and of triples of alternatives have been studied.
The first objective of this paper is to establish such connections for the case of arbitrary fuzzy choice functions. We introduce the new revealed preference axioms WAFRP°, SAFRP°, HAFRP and we prove two main theorems:
1. The axioms WFCA and WAFRP° are equivalent;
2. The axioms SFCA and HAFRP are equivalent.
Our second objective is to define G-rational, M-rational, G-normal and M-normal fuzzy choice functions and to investigate some of their properties.
The notions and the results are formulated in terms of the residuum of the Gödel t-norm and the proofs use the residuated lattice structure of the interval [0, 1].
Region Connection Calculus (RCC) is the most widely studied formalism of Qualitative Spatial Reasoning. It has been known for some time that each connected regular topological space provides an RCC model. These `standard' models are inevitable uncountable and regions there cannot be represented finitely. This paper, however, draws researchers' attention to RCC models that can be constructed from finite models hierarchically. Compared with those `standard' models, these countable models have the nice property that regions where can be constructed in finite steps from basic ones. We first investigate properties of three countable models introduced by Düntsch, Stell, Li and Ying, resp. In particular, we show that (i) the contact relation algebra of our minimal model is not atomic complete; and (ii) these three models are non-isomorphic. Second, for each n > 0, we construct a countable RCC model that is a sub-model of the standard model over the Euclidean unit n-cube; and show that all these countable models are non-isomorphic. Third, we show that every finite model can be isomorphically embedded in any RCC model. This leads to a simple proof for the result that each consistent spatial network has a realization in any RCC model.
The vector quantization (VQ) compression scheme has been well accepted as an efficient image compression technique. However, the compression bit rate of the VQ scheme is limited. In order to improve its efficiency, in this paper, we shall propose a new lossless data compression scheme to further condense the VQ index table. The proposed scheme exploits the inter-block correlations in the index table to re-encode the indices. Unlike the well known existing re-encoding schemes such as SOC and STC, the proposed scheme uses a smaller number of compression codes to encode every index that coincides with another on the predefined path. Compared with VQ, SOC and STC, the proposed scheme performs better in terms of compression bit rate.
In the field of biological regulation, models extracted from experimental works are usually complex networks comprising intertwined feedback circuits. The overall behavior is difficult to grasp and the development of formal methods is needed in order to model and simulate biological regulatory networks. To model the behavior of such systems, R. Thomas and coworkers developed a qualitative approach in which the dynamics is described by a state transition system. Even if all steady states of the system can be detected in this formalism, some of them, the singular ones, are not formally included in the transition system. Consequently, temporal properties in which singular states have to be described, cannot be checked against the transition system. However, steady singular states play an essential role in the dynamics since they can induce homeostasis or multistationnarity and sometimes are associated to biological phenotypes.
These observations motivated our interest for developing an extension of Thomas formalism in which all singular states are represented, allowing us to check temporal properties concerning singular states. We easily demonstrate in our formalism the previously demonstrated theorems giving the conditions for the steadiness of singular states. We also prove that our formalism is coherent with the Thomas one since all paths of the Thomas transition system are preserved in our one, which in addition includes singular states.