Fundamenta Informaticae - Volume 103, issue 1-4

Authors: Gambin, Anna | NiwińSki, Damian | Urzyczyn, Paweł

Article Type: Other

DOI: 10.3233/FI-2010-315

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. i-ii, 2010

Authors: Barbuti, Roberto | Maggiolo-Schettini, Andrea | Troina, Angelo | Dezani-Ciancaglini, Mariangiola | Milazzo, Paolo

Article Type: Research Article

Abstract: The Calculus of Looping Sequences is a formalism for describing evolution of biological systems by means of term rewriting rules. We propose to enrich this calculus by labelling elements of sequences. Since two elements with the same label are considered to be linked, this allows us to represent protein interaction at the domain level. Well-formedness of terms are ensured by both a syntactic constraint and a type system: we discuss the differences between these approaches through the description of a biological system, namely the EGF pathway.

Keywords: Systems Biology, Predictive Modelling, Term Rewriting, Type Theories

DOI: 10.3233/FI-2010-316

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 1-29, 2010

Authors: Bergstra, J.A. | Middelburg, C.A.

Article Type: Research Article

Abstract: We study shedding in the setting of data linkage dynamics, a simple model of computation that bears on the use of dynamic data structures in programming. Shedding is complementary to garbage collection. With shedding, each time a link to a data object is updated by a program, it is determined whether or not the link will possibly be used once again by the program, and if not the link is automatically removed. Thus, everything is made garbage as soon as it can be viewed as garbage. By that, the effectiveness of garbage collection becomes maximal.

Keywords: data linkage dynamics, shedding, forecasting service

DOI: 10.3233/FI-2010-317

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 31-52, 2010

Authors: Dojer, Norbert

Article Type: Research Article

Abstract: We propose an algorithm for learning an optimal Bayesian network from data. Our method is addressed to biological applications, where usually datasets are small, and sets of random variables are large. Moreover, we assume that there is no need to examine the acyclicity of the graph. We provide polynomial bounds (with respect to the number of random variables) for time complexity of our algorithm for two generally used scoring criteria: Minimal Description Length and Bayesian-Dirichlet equivalence. Then we show how to adapt these criteria to work with continuous data and prove polynomial bounds for adapted scores. Finally, we briefly describe …applications of proposed algorithm in computational biology. Show more

DOI: 10.3233/FI-2010-318

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 53-67, 2010

Authors: Donnelly, Kevin | Kfoury, Assaf | Lapets, Andrei

Article Type: Research Article

Abstract: Interdomain routing on the Internet is performed using route preference policies specified independently and arbitrarily by each autonomous system (AS) in the network. These policies are used in the border gateway protocol (BGP) by each AS when selecting next-hop choices for routes to each destination. Conflicts between policies used by different ASs can lead to routing instabilities that, potentially, cannot be resolved regardless of how long BGP runs. The stable paths problem (SPP) is an abstract graph theoretic model of the problem of selecting next-hop routes for a destination. A solution to this problem is a set of next-hop choices, …one for each AS, that is compatible with the policies of each AS. In a stable solution each AS has selected its best next-hop if the next-hop choices of all neighbors are fixed. BGP can be viewed as a distributed algorithm for solving an SPP instance. In this report we consider a family of restricted variants of SPP, which we call f-SPP. We show that several natural variants of f-SPP are NP-complete. This includes a variant in which each AS is restricted to one of only two policies and each of these two policies is based on a monotonic weight aggregation function. Furthermore, we show that for networks with particular topologies and edge weight distributions, there exist efficient centralized algorithms for solving f-SPP. Show more

DOI: 10.3233/FI-2010-319

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 69-87, 2010

Authors: Gambin, Anna | Kluge, Bogusław

Article Type: Research Article

Abstract: In this paper we propose a mathematical model of the proteolysis process. Protein digestion is modelled with the use of chemical master equation (CME), i.e. the system of stochastic differential equations corresponding to the network of enzymatic reactions. We present an efficient approach to model parameters' estimation (i.e. enzyme activities) from time series of mass spectrometry data. These results extend previous results in three directions: by relaxing the stationarity of the proteolysis process assumption, by allowing cuts at arbitrary sites in the peptide sequence and by incorporating knowledge from biological databases.

Keywords: chemical master equation, peptidase activity, proteomics, stochastic modeling, mass spectrometry, Markov chain, non-linear optimization, matrix exponentiation

DOI: 10.3233/FI-2010-320

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 89-104, 2010

Authors: Górecki, Paweł

Article Type: Research Article

Abstract: In this paper, we present a model of evolution of genes in the context of evolution of species. The concept is based on reconciliation models. We assume that the gene evolution is modeled by macro-evolutionary events like gene duplications, losses and horizontal gene transfers (HGTs) while the evolution of species is shaped by speciation events. We define an evolutionary scenario (called an H-tree) which will represent the common evolution of genes and species. We propose a rewrite system for transforming the scenarios. We prove that the system is confluent, sound and strongly normalizing. We show that a scenario in a …normal form (that is, non-reducible) is unique and minimal in the sense of the cost computed as the total number of gene duplications, losses and HGTs (mutation cost). We present a classification of the scenarios and analyze their hierarchies. Show more

Keywords: Rewrite system, Molecular evolution, Phylogenetic tree, Duplication-loss model (DL-model), Horizontal gene transfer, Reconciled tree

DOI: 10.3233/FI-2010-321

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 105-128, 2010

Authors: Kozen, Dexter

Article Type: Research Article

Abstract: The Church–Rosser theorem states that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Löf. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the βη-calculus.

Keywords: lambda-calculus, confluence, Church–Rosser theorem

DOI: 10.3233/FI-2010-322

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 129-136, 2010

Authors: Kuśmierek, JarosłAw Dominik Mateusz | Bono, Viviana

Article Type: Research Article

Abstract: In this paper we present a novel approach to big-step operational semantics. This approach stems from the observation that the typical type soundness property formulated via a big-step operational semantics is weak, while the option of using a small-step operational semantics is not always an option, because it is less intuitive to build and understand. We support our claim by using a simple language called LM, for which we present a big-step semantics expressed with the new approach, allowing one to formulate a stronger type soundness property. We prove this property for LM and we present an example of an …error in the typing rules which does not violate the typical type soundness property, but does violate ours. Show more

DOI: 10.3233/FI-2010-323

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 137-172, 2010

Authors: Pagani, Michele | Rocca, Simona Ronchi Della

Article Type: Research Article

Abstract: We study the notion of solvability in the resource calculus, an extension of the λ-calculus modelling resource consumption. Since this calculus is non-deterministic, two different notions of solvability arise, one optimistic (angelical, may) and one pessimistic (demoniac, must). We give a syntactical, operational and logical characterization for the may-solvability and only a partial characterization of the must-solvability. Finally, we discuss the open problem of a complete characterization of the must-solvability.

DOI: 10.3233/FI-2010-324

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 173-202, 2010

Authors: Pratt, Vaughan

Article Type: Research Article

Abstract: We present the Yoneda Lemma in terms of categories without explicit reference to the notion of functor. From this perspective we then define a commune as a common generalization of Chu spaces and presheaves, and give some applications.

Keywords: commune, yoneda, chu space

DOI: 10.3233/FI-2010-325

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 203-218, 2010

Authors: Rudnicki, Ryszard | Wieczorek, Radosław

Article Type: Research Article

Abstract: We study a non-linear age-structured discrete-time population model and give necessary and sufficient conditions for stability of a positive stationary point. In the case of semelparous species we show that the population converges locally to a population consisted only of individuals at one age. It means that the long-time behaviour of the population depends only on an one-dimensional transformation g. If the reproduction age is an even number we prove that the positive stationary point is unstable and numerical simulations suggest that in this case almost all trajectories behave asymptotically as trajectories corresponding to g.

Keywords: age-structured discrete-time model, semelparous species, periodicity, chaos

DOI: 10.3233/FI-2010-326

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 219-233, 2010

Authors: Setty, Yaki | Cohen, Irun R. | Harel, David

Article Type: Research Article

Abstract: Complex biological systems involve incorporated behaviors of numerous processes, mechanisms and objects. However, experimental analysis, by its nature, divides biological systems into static interactions with little dynamics. To bridge the gap between experimental data and the underlying behavior, our group has been formalizing biological findings into mathematically and algorithmically rigorous specifications, which are then compiled into reactive models. To realistically animate our models, we designed a generic architecture for the earlier idea of reactive animation, in a way that allows it to link up reactive models with animation tools. Here, we describe the reactive animation approach and some of the …benefits of employing it to simulate and analyze complex biological systems. We illustrate our approach with a model of pancreatic development, a highly complex system with a unique 3D structure, and also mention more recent work on adding animation to the generic cell project (GemCell). Show more

Keywords: Modeling, Computational Biology, Reactive Animation

DOI: 10.3233/FI-2010-327

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 235-246, 2010

Authors: Shivers, Olin | Wand, Mitchell

Article Type: Research Article

Abstract: If we represent a λ-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from β-reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement β-reduction in a bottom-up manner, thus avoiding combinatorial explosion in time required to search the term in a top-down fashion. We present an algorithm for performing β-reduction on λ-terms represented as uplinked DAGs; describe its proof of correctness; discuss its relation to alternate techniques such as Lamping graphs, explicit-substitution calculi and director strings; and present some timings of …an implementation. Besides being both fast and parsimonious of space, the algorithm is particularly suited to applications such as compilers, theorem provers, and type-manipulation systems that may need to examine terms in between reductions—i.e., the “readback” problem for our representation is trivial. Like Lamping graphs, and unlike director strings or the suspension λ calculus, the algorithm functions by side-effecting the term containing the redex; the representation is not a “persistent” one. The algorithm additionally has the charm of being quite simple; a complete implementation of the data structure and algorithm is 180 lines of SML. Show more

DOI: 10.3233/FI-2010-328

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 247-287, 2010

Authors: Tyszkiewicz, Jerzy

Article Type: Research Article

Abstract: This paper contains the English version of my Master's thesis [6] written about 22 years ago under supervision of Jerzy Tiuryn. Its main result is the proof of PTIME-completeness of the type reconstruction problem for simply typed lambda calculus. About the time I had the English paper ready, a much simpler proof [3] by John Mitchell (later published in [4]) was announced. Therefore my thesis remained an unpublished manuscript, but has been referenced to in a number of other papers. The TEX sources went lost in the meantime, so the present paper has been re-typed from scratch, but is almost …identical to the original one written many years ago. Show more

Keywords: typed lambda calculus, simple types, typability, complexity, PTIME

DOI: 10.3233/FI-2010-329

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 289-301, 2010

Authors: Urzyczyn, Paweł

Article Type: Research Article

Abstract: Is is shown that the inhabitation problem is decidable for intersection type assignment without the intersection elimination rule.

DOI: 10.3233/FI-2010-330

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 303-322, 2010

Authors: Wilczyński, Bartek | Hvidsten, Torgeir R.

Article Type: Research Article

Abstract: Recent years have seen a wealth of computational methods applied to problems stemming from molecular biology. In particular, with the completion of many new full genome sequences, great advances have been made in studying the role of non-protein-coding parts of the genome, reshaping our understanding of the role of DNA sequences. Recent breakthroughs in experimental technologies allowing us to inspect the innards of cells on a genomic scale has provided us with unprecedented amounts of data, posing new computational challenges for scientists working to uncover the secrets of life. Due to the binary-like nature of the DNA code and switch-like …behavior of many regulatory mechanisms, many of the questions that are currently in focus in biology are surprisingly related to problems that have been of long-term interest to computer scientists. In this review, we present a glimpse into the current state of research in computational methods applied to modeling the regulatory genome. Our aim is to cover current approaches to selected problems from molecular biology that we consider most interesting from the perspective of computer scientists as well as highlight new challenges that will most likely draw the attention of computational biologists in the coming years. Show more

Keywords: computational biology, gene regulation, DNA motifs, regulatory elements

DOI: 10.3233/FI-2010-331

Citation: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 323-332, 2010