Fundamenta Informaticae - Volume 65, issue 1-2

Authors: Hofmann, Martin | Urzyczyn, Paweł

Article Type: Other

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. v-v, 2005

Authors: Abbott, Michael | Altenkirch, Thorsten | McBride, Conor | Ghani, Neil

Article Type: Research Article

Abstract: 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. Show more

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 1-28, 2005

Authors: Amadio, Roberto M.

Article Type: Research Article

Abstract: 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. Show more

Keywords: Functional languages and term rewriting, Function algebras and implicit computational complexity, Static analysis, Polynomial interpretations and max-plus algebras

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 29-60, 2005

Authors: Blanqui, Frédéric

Article Type: Research Article

Abstract: 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. Show more

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 61-86, 2005

Authors: Coppola, Paolo | Ronchi della Rocca, Simona

Article Type: Research Article

Abstract: 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 λ-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 λ-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. Show more

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 87-112, 2005

Authors: Coquand, Thierry | Pollack, Randy | Takeyama, Makoto

Article Type: Research Article

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 113-134, 2005

Authors: Joly, Thierry

Article Type: Research Article

Abstract: The question whether a given functional of some full type structure (FTS for short) is λ-definable by a closed λ-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 -Pattern Matching Problem, recently established by R. Loader in [Loa03]. Show more

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 135-151, 2005

Authors: Kakutani, Yoshihiko | Hasegawa, Masahito

Article Type: Research Article

Abstract: The λμ-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 λμ-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. Show more

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 153-172, 2005

Authors: Laird, Jim

Article Type: Research Article

Abstract: 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 λ-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. Show more

Citation: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 173-191, 2005